--- 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\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Fract_of_int_quotient)
lemma "Abs_Rat (Rep_Rat a) = a"
-nitpick [card = 1\<midarrow>2, expect = unknown]
+nitpick [card = 1\<midarrow>2, expect = none]
by (rule Rep_Rat_inverse)
end
--- 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))
--- 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
--- 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 *)
--- 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)
--- 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