# HG changeset patch # User blanchet # Date 1256826292 -3600 # Node ID 3655e51f9958a683832036ba5c00e3e442c5a97a # Parent 14f2880e7ccf583a9f8f31aebf09acf94c6483ca minor cleanup in Nitpick diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Oct 29 15:24:52 2009 +0100 @@ -173,15 +173,15 @@ Ycoord :: int lemma "Abs_point_ext_type (Rep_point_ext_type a) = a" -nitpick [expect = unknown] +nitpick [expect = none] by (rule Rep_point_ext_type_inverse) lemma "Fract a b = of_int a / of_int b" -nitpick [card = 1\2, expect = unknown] +nitpick [card = 1\2, expect = none] by (rule Fract_of_int_quotient) lemma "Abs_Rat (Rep_Rat a) = a" -nitpick [card = 1\2, expect = unknown] +nitpick [card = 1\2, expect = none] by (rule Rep_Rat_inverse) end diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 29 15:24:52 2009 +0100 @@ -313,7 +313,7 @@ (@{const_name times_int_inst.times_int}, 0), (@{const_name div_int_inst.div_int}, 0), (@{const_name div_int_inst.mod_int}, 0), - (@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *) + (@{const_name uminus_int_inst.uminus_int}, 0), (@{const_name ord_int_inst.less_int}, 2), (@{const_name ord_int_inst.less_eq_int}, 2), (@{const_name Tha}, 1), @@ -966,6 +966,14 @@ (* indexname * typ -> term -> term *) fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) +(* theory -> string -> bool *) +fun is_funky_typedef_name thy s = + s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, + @{type_name int}] + orelse is_frac_type thy (Type (s, [])) +(* theory -> term -> bool *) +fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s + | is_funky_typedef _ _ = false (* term -> bool *) fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _) $ Const (@{const_name TYPE}, _)) = true @@ -976,9 +984,7 @@ | is_typedef_axiom thy boring (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = - boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}] - orelse is_frac_type thy (Type (s, []))) - andalso is_typedef thy s + boring <> is_funky_typedef_name thy s andalso is_typedef thy s | is_typedef_axiom _ _ _ = false (* Distinguishes between (1) constant definition axioms, (2) type arity and @@ -2543,7 +2549,6 @@ t else let - (* FIXME: strong enough in the face of user-defined axioms? *) val blacklist = if depth = 0 then [] else case term_under_def t of Const x => [x] | _ => [] (* term list -> typ list -> term -> term *) @@ -3009,14 +3014,16 @@ else if is_abs_fun thy x then accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> fold (add_def_axiom depth) - (nondef_props_for_const thy true + |> is_funky_typedef thy (range_type T) + ? fold (add_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) else if is_rep_fun thy x then accum |> fold (add_nondef_axiom depth) (nondef_props_for_const thy false nondef_table x) - |> fold (add_def_axiom depth) - (nondef_props_for_const thy true + |> is_funky_typedef thy (range_type T) + ? fold (add_def_axiom depth) + (nondef_props_for_const thy true (extra_table def_table s) x) |> add_axioms_for_term depth (Const (mate_of_rep_fun thy x)) diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Oct 29 15:24:52 2009 +0100 @@ -343,7 +343,6 @@ (* The type constraint below is a workaround for a Poly/ML bug. *) -(* FIXME: clean up *) (* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *) fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) R r = @@ -371,7 +370,6 @@ Kodkod.True end fun kk_n_ary_function kk R (r as Kodkod.Rel _) = - (* FIXME: weird test *) if not (is_opt_rep R) then if r = suc_rel then Kodkod.False diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Oct 29 15:24:52 2009 +0100 @@ -588,8 +588,7 @@ |> term_for_rep T T' (rep_of name) in Pretty.block (Pretty.breaks - [(setmp_CRITICAL show_question_marks false o setmp_show_all_types) - (Syntax.pretty_term ctxt) t1, + [setmp_show_all_types (Syntax.pretty_term ctxt) t1, Pretty.str oper, Syntax.pretty_term ctxt t2]) end (* dtype_spec -> Pretty.T *) diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Oct 29 15:24:52 2009 +0100 @@ -505,7 +505,7 @@ map prop_for_comp comps @ map prop_for_sign_expr sexps) in - case silence (SatSolver.invoke_solver "dpll") prop of + case SatSolver.invoke_solver "dpll" prop of SatSolver.SATISFIABLE asgns => SOME (literals_from_assignments max_var asgns lits |> tap print_solution) diff -r 14f2880e7ccf -r 3655e51f9958 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Oct 29 15:23:25 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Oct 29 15:24:52 2009 +0100 @@ -1059,11 +1059,12 @@ Op2 (And, bool_T, Any, case u2 of Op2 (Lambda, _, _, u21, u22) => - if num_occs_in_nut u21 u22 = 0 then (* FIXME: move to s_op2 *) + if num_occs_in_nut u21 u22 = 0 then u22 else Op2 (Apply, bool_T, Any, u2, x_u) | _ => Op2 (Apply, bool_T, Any, u2, x_u), + Op2 (Eq, bool_T, Any, y_u, Op2 (Apply, ran_T, Any, u1, x_u))))) |> sub