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