minor cleanup in Nitpick
authorblanchet
Thu Oct 29 15:24:52 2009 +0100 (2009-10-29)
changeset 335713655e51f9958
parent 33570 14f2880e7ccf
child 33572 d78f347515e0
minor cleanup in Nitpick
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Oct 29 15:23:25 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Oct 29 15:24:52 2009 +0100
     1.3 @@ -173,15 +173,15 @@
     1.4    Ycoord :: int
     1.5  
     1.6  lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
     1.7 -nitpick [expect = unknown]
     1.8 +nitpick [expect = none]
     1.9  by (rule Rep_point_ext_type_inverse)
    1.10  
    1.11  lemma "Fract a b = of_int a / of_int b"
    1.12 -nitpick [card = 1\<midarrow>2, expect = unknown]
    1.13 +nitpick [card = 1\<midarrow>2, expect = none]
    1.14  by (rule Fract_of_int_quotient)
    1.15  
    1.16  lemma "Abs_Rat (Rep_Rat a) = a"
    1.17 -nitpick [card = 1\<midarrow>2, expect = unknown]
    1.18 +nitpick [card = 1\<midarrow>2, expect = none]
    1.19  by (rule Rep_Rat_inverse)
    1.20  
    1.21  end
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 29 15:23:25 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Oct 29 15:24:52 2009 +0100
     2.3 @@ -313,7 +313,7 @@
     2.4     (@{const_name times_int_inst.times_int}, 0),
     2.5     (@{const_name div_int_inst.div_int}, 0),
     2.6     (@{const_name div_int_inst.mod_int}, 0),
     2.7 -   (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *)
     2.8 +   (@{const_name uminus_int_inst.uminus_int}, 0),
     2.9     (@{const_name ord_int_inst.less_int}, 2),
    2.10     (@{const_name ord_int_inst.less_eq_int}, 2),
    2.11     (@{const_name Tha}, 1),
    2.12 @@ -966,6 +966,14 @@
    2.13  (* indexname * typ -> term -> term *)
    2.14  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    2.15  
    2.16 +(* theory -> string -> bool *)
    2.17 +fun is_funky_typedef_name thy s =
    2.18 +  s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
    2.19 +         @{type_name int}]
    2.20 +  orelse is_frac_type thy (Type (s, []))
    2.21 +(* theory -> term -> bool *)
    2.22 +fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
    2.23 +  | is_funky_typedef _ _ = false
    2.24  (* term -> bool *)
    2.25  fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
    2.26                           $ Const (@{const_name TYPE}, _)) = true
    2.27 @@ -976,9 +984,7 @@
    2.28    | is_typedef_axiom thy boring
    2.29          (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
    2.30           $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
    2.31 -    boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
    2.32 -               orelse is_frac_type thy (Type (s, [])))
    2.33 -    andalso is_typedef thy s
    2.34 +    boring <> is_funky_typedef_name thy s andalso is_typedef thy s
    2.35    | is_typedef_axiom _ _ _ = false
    2.36  
    2.37  (* Distinguishes between (1) constant definition axioms, (2) type arity and
    2.38 @@ -2543,7 +2549,6 @@
    2.39      t
    2.40    else
    2.41      let
    2.42 -      (* FIXME: strong enough in the face of user-defined axioms? *)
    2.43        val blacklist = if depth = 0 then []
    2.44                        else case term_under_def t of Const x => [x] | _ => []
    2.45        (* term list -> typ list -> term -> term *)
    2.46 @@ -3009,14 +3014,16 @@
    2.47               else if is_abs_fun thy x then
    2.48                 accum |> fold (add_nondef_axiom depth)
    2.49                               (nondef_props_for_const thy false nondef_table x)
    2.50 -                     |> fold (add_def_axiom depth)
    2.51 -                             (nondef_props_for_const thy true
    2.52 +                     |> is_funky_typedef thy (range_type T)
    2.53 +                        ? fold (add_def_axiom depth)
    2.54 +                               (nondef_props_for_const thy true
    2.55                                                      (extra_table def_table s) x)
    2.56               else if is_rep_fun thy x then
    2.57                 accum |> fold (add_nondef_axiom depth)
    2.58                               (nondef_props_for_const thy false nondef_table x)
    2.59 -                     |> fold (add_def_axiom depth)
    2.60 -                             (nondef_props_for_const thy true
    2.61 +                     |> is_funky_typedef thy (range_type T)
    2.62 +                        ? fold (add_def_axiom depth)
    2.63 +                               (nondef_props_for_const thy true
    2.64                                                      (extra_table def_table s) x)
    2.65                       |> add_axioms_for_term depth
    2.66                                              (Const (mate_of_rep_fun thy x))
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Oct 29 15:23:25 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Oct 29 15:24:52 2009 +0100
     3.3 @@ -343,7 +343,6 @@
     3.4  
     3.5  (* The type constraint below is a workaround for a Poly/ML bug. *)
     3.6  
     3.7 -(* FIXME: clean up *)
     3.8  (* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *)
     3.9  fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
    3.10                       R r =
    3.11 @@ -371,7 +370,6 @@
    3.12        Kodkod.True
    3.13    end
    3.14  fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
    3.15 -    (* FIXME: weird test *)
    3.16      if not (is_opt_rep R) then
    3.17        if r = suc_rel then
    3.18          Kodkod.False
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 15:23:25 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 15:24:52 2009 +0100
     4.3 @@ -588,8 +588,7 @@
     4.4                     |> term_for_rep T T' (rep_of name)
     4.5        in
     4.6          Pretty.block (Pretty.breaks
     4.7 -            [(setmp_CRITICAL show_question_marks false o setmp_show_all_types)
     4.8 -                 (Syntax.pretty_term ctxt) t1,
     4.9 +            [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
    4.10               Pretty.str oper, Syntax.pretty_term ctxt t2])
    4.11        end
    4.12      (* dtype_spec -> Pretty.T *)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 15:23:25 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 15:24:52 2009 +0100
     5.3 @@ -505,7 +505,7 @@
     5.4                                  map prop_for_comp comps @
     5.5                                  map prop_for_sign_expr sexps)
     5.6      in
     5.7 -      case silence (SatSolver.invoke_solver "dpll") prop of
     5.8 +      case SatSolver.invoke_solver "dpll" prop of
     5.9          SatSolver.SATISFIABLE asgns =>
    5.10          SOME (literals_from_assignments max_var asgns lits
    5.11                |> tap print_solution)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Oct 29 15:23:25 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Oct 29 15:24:52 2009 +0100
     6.3 @@ -1059,11 +1059,12 @@
     6.4                                 Op2 (And, bool_T, Any,
     6.5                                      case u2 of
     6.6                                        Op2 (Lambda, _, _, u21, u22) =>
     6.7 -                                      if num_occs_in_nut u21 u22 = 0 then (* FIXME: move to s_op2 *)
     6.8 +                                      if num_occs_in_nut u21 u22 = 0 then
     6.9                                          u22
    6.10                                        else
    6.11                                          Op2 (Apply, bool_T, Any, u2, x_u)
    6.12                                      | _ => Op2 (Apply, bool_T, Any, u2, x_u),
    6.13 +
    6.14                                      Op2 (Eq, bool_T, Any, y_u,
    6.15                                           Op2 (Apply, ran_T, Any, u1, x_u)))))
    6.16                       |> sub