added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
--- a/doc-src/Nitpick/nitpick.tex Thu Feb 18 10:38:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Feb 18 18:48:07 2010 +0100
@@ -472,7 +472,7 @@
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
-\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
+\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
Nitpick found a potential counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
@@ -2083,7 +2083,6 @@
Specifies whether the given (recursive) datatype should be given standard
models. Nonstandard models are unsound but can help debug structural induction
proofs, as explained in \S\ref{inductive-properties}.
-%This option is not supported for the type \textit{nat}.
\optrue{std}{non\_std}
Specifies the default standardness to use. This can be overridden on a per-type
--- a/src/HOL/Nitpick.thy Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Nitpick.thy Thu Feb 18 18:48:07 2010 +0100
@@ -217,21 +217,6 @@
definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
"of_frac q \<equiv> of_int (num q) / of_int (denom q)"
-(* While Nitpick normally avoids to unfold definitions for locales, it
- unfortunately needs to unfold them when dealing with the following built-in
- constants. A cleaner approach would be to change "Nitpick_HOL" and
- "Nitpick_Nut" so that they handle the unexpanded overloaded constants
- directly, but this is slightly more tricky to implement. *)
-lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
- div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun
- minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
- one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
- ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
- ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
- times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
- semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int
- zero_nat_inst.zero_nat
-
use "Tools/Nitpick/kodkod.ML"
use "Tools/Nitpick/kodkod_sat.ML"
use "Tools/Nitpick/nitpick_util.ML"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 18 18:48:07 2010 +0100
@@ -265,7 +265,7 @@
orig_assm_ts
*)
val max_bisim_depth = fold Integer.max bisim_depths ~1
- val case_names = case_const_names thy
+ val case_names = case_const_names thy stds
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
val def_table = const_def_table ctxt defs
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
@@ -337,7 +337,7 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_type_always_monotonic T =
- (is_datatype thy T andalso not (is_quot_type thy T) andalso
+ (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_monotonic T =
@@ -347,8 +347,8 @@
| _ => is_type_always_monotonic T orelse
formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
fun is_deep_datatype T =
- is_datatype thy T andalso
- (not standard orelse is_word_type T orelse
+ is_datatype thy stds T andalso
+ (not standard orelse T = nat_T orelse is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names)
val all_Ts = ground_types_in_terms hol_ctxt binarize
(core_t :: def_ts @ nondef_ts)
@@ -519,8 +519,9 @@
declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
- val univ_card = univ_card nat_card int_card main_j0
- (plain_bounds @ sel_bounds) formula
+ val univ_card = Int.max (univ_card nat_card int_card main_j0
+ (plain_bounds @ sel_bounds) formula,
+ main_j0 |> bits > 0 ? Integer.add (bits + 1))
val built_in_bounds = bounds_for_built_in_rels_in_formula debug
univ_card nat_card int_card main_j0 formula
val bounds = built_in_bounds @ plain_bounds @ sel_bounds
@@ -837,8 +838,9 @@
forall (KK.is_problem_trivially_false o fst)
sound_problems then
print_m (fn () =>
- "Warning: The conjecture either trivially holds or (more \
- \likely) lies outside Nitpick's supported fragment." ^
+ "Warning: The conjecture either trivially holds for the \
+ \given scopes or (more likely) lies outside Nitpick's \
+ \supported fragment." ^
(if exists (not o KK.is_problem_trivially_false o fst)
unsound_problems then
" Only potential counterexamples may be found."
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 18 18:48:07 2010 +0100
@@ -85,6 +85,7 @@
val is_integer_type : typ -> bool
val is_bit_type : typ -> bool
val is_word_type : typ -> bool
+ val is_integer_like_type : typ -> bool
val is_record_type : typ -> bool
val is_number_type : theory -> typ -> bool
val const_for_iterator_type : typ -> styp
@@ -95,14 +96,13 @@
val curried_binder_types : typ -> typ list
val mk_flat_tuple : typ -> term list -> term
val dest_n_tuple : int -> term -> term list
- val instantiate_type : theory -> typ -> typ -> typ -> typ
val is_real_datatype : theory -> string -> bool
- val is_standard_datatype : hol_context -> typ -> bool
+ val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
val is_quot_type : theory -> typ -> bool
val is_codatatype : theory -> typ -> bool
val is_pure_typedef : theory -> typ -> bool
val is_univ_typedef : theory -> typ -> bool
- val is_datatype : theory -> typ -> bool
+ val is_datatype : theory -> (typ option * bool) list -> typ -> bool
val is_record_constr : styp -> bool
val is_record_get : theory -> styp -> bool
val is_record_update : theory -> styp -> bool
@@ -113,7 +113,7 @@
val mate_of_rep_fun : theory -> styp -> styp
val is_constr_like : theory -> styp -> bool
val is_stale_constr : theory -> styp -> bool
- val is_constr : theory -> styp -> bool
+ val is_constr : theory -> (typ option * bool) list -> styp -> bool
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
@@ -141,8 +141,10 @@
val constr_name_for_sel_like : string -> string
val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
val discriminate_value : hol_context -> styp -> term -> term
- val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
- val construct_value : theory -> styp -> term list -> term
+ val select_nth_constr_arg :
+ theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
+ val construct_value :
+ theory -> (typ option * bool) list -> styp -> term list -> term
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
val bounded_exact_card_of_type :
@@ -151,10 +153,13 @@
val special_bounds : term list -> (indexname * typ) list
val is_funky_typedef : theory -> typ -> bool
val all_axioms_of : theory -> term list * term list * term list
- val arity_of_built_in_const : bool -> styp -> int option
- val is_built_in_const : bool -> styp -> bool
+ val arity_of_built_in_const :
+ theory -> (typ option * bool) list -> bool -> styp -> int option
+ val is_built_in_const :
+ theory -> (typ option * bool) list -> bool -> styp -> bool
val term_under_def : term -> term
- val case_const_names : theory -> (string * int) list
+ val case_const_names :
+ theory -> (typ option * bool) list -> (string * int) list
val const_def_table : Proof.context -> term list -> const_table
val const_nondef_table : term list -> const_table
val const_simp_table : Proof.context -> const_table
@@ -165,7 +170,8 @@
val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
val inverse_axioms_for_rep_fun : theory -> styp -> term list
val optimized_typedef_axioms : theory -> string * typ list -> term list
- val optimized_quot_type_axioms : theory -> string * typ list -> term list
+ val optimized_quot_type_axioms :
+ theory -> (typ option * bool) list -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
val fixpoint_kind_of_const :
theory -> const_table -> string * typ -> fixpoint_kind
@@ -340,44 +346,45 @@
(@{const_name trancl}, 1),
(@{const_name rel_comp}, 2),
(@{const_name image}, 2),
- (@{const_name Suc}, 0),
(@{const_name finite}, 1),
- (@{const_name nat}, 0),
- (@{const_name zero_nat_inst.zero_nat}, 0),
- (@{const_name one_nat_inst.one_nat}, 0),
- (@{const_name plus_nat_inst.plus_nat}, 0),
- (@{const_name minus_nat_inst.minus_nat}, 0),
- (@{const_name times_nat_inst.times_nat}, 0),
- (@{const_name div_nat_inst.div_nat}, 0),
- (@{const_name ord_nat_inst.less_nat}, 2),
- (@{const_name ord_nat_inst.less_eq_nat}, 2),
- (@{const_name nat_gcd}, 0),
- (@{const_name nat_lcm}, 0),
- (@{const_name zero_int_inst.zero_int}, 0),
- (@{const_name one_int_inst.one_int}, 0),
- (@{const_name plus_int_inst.plus_int}, 0),
- (@{const_name minus_int_inst.minus_int}, 0),
- (@{const_name times_int_inst.times_int}, 0),
- (@{const_name div_int_inst.div_int}, 0),
- (@{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 unknown}, 0),
(@{const_name is_unknown}, 1),
(@{const_name Tha}, 1),
(@{const_name Frac}, 0),
(@{const_name norm_frac}, 0)]
+val built_in_nat_consts =
+ [(@{const_name Suc}, 0),
+ (@{const_name nat}, 0),
+ (@{const_name nat_gcd}, 0),
+ (@{const_name nat_lcm}, 0)]
val built_in_descr_consts =
[(@{const_name The}, 1),
(@{const_name Eps}, 1)]
val built_in_typed_consts =
- [((@{const_name of_nat}, nat_T --> int_T), 0),
- ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
+ [((@{const_name zero_class.zero}, int_T), 0),
+ ((@{const_name one_class.one}, int_T), 0),
+ ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
+ ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
+ ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
+ ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
+ ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
+ ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
+ ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
+val built_in_typed_nat_consts =
+ [((@{const_name zero_class.zero}, nat_T), 0),
+ ((@{const_name one_class.one}, nat_T), 0),
+ ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
+ ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
+ ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
+ ((@{const_name of_nat}, nat_T --> int_T), 0)]
val built_in_set_consts =
- [(@{const_name semilattice_inf_fun_inst.inf_fun}, 2),
- (@{const_name semilattice_sup_fun_inst.sup_fun}, 2),
- (@{const_name minus_fun_inst.minus_fun}, 2),
- (@{const_name ord_fun_inst.less_eq_fun}, 2)]
+ [(@{const_name semilattice_inf_class.inf}, 2),
+ (@{const_name semilattice_sup_class.sup}, 2),
+ (@{const_name minus_class.minus}, 2),
+ (@{const_name ord_class.less_eq}, 2)]
(* typ -> typ *)
fun unarize_type @{typ "unsigned_bit word"} = nat_T
@@ -449,17 +456,19 @@
| is_gfp_iterator_type _ = false
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
fun is_boolean_type T = (T = prop_T orelse T = bool_T)
-val is_integer_type =
- member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
+fun is_integer_type T = (T = nat_T orelse T = int_T)
fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
fun is_word_type (Type (@{type_name word}, _)) = true
| is_word_type _ = false
+fun is_integer_like_type T =
+ is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
+ T = @{typ bisim_iterator}
val is_record_type = not o null o Record.dest_recTs
(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
| is_frac_type _ _ = false
-fun is_number_type thy = is_integer_type orf is_frac_type thy
+fun is_number_type thy = is_integer_like_type orf is_frac_type thy
(* bool -> styp -> typ *)
fun iterator_type_for_const gfp (s, T) =
@@ -507,13 +516,41 @@
| dest_n_tuple_type _ T =
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
+type typedef_info =
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
+ set_def: thm option, prop_of_Rep: thm, set_name: string,
+ Abs_inverse: thm option, Rep_inverse: thm option}
+
+(* theory -> string -> typedef_info *)
+fun typedef_info thy s =
+ if is_frac_type thy (Type (s, [])) then
+ SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
+ Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
+ set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+ |> Logic.varify,
+ set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+ else case Typedef.get_info thy s of
+ SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+ Rep_inverse, ...} =>
+ SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+ Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+ set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+ Rep_inverse = SOME Rep_inverse}
+ | NONE => NONE
+
+(* theory -> string -> bool *)
+val is_typedef = is_some oo typedef_info
+val is_real_datatype = is_some oo Datatype.get_info
+(* theory -> (typ option * bool) list -> typ -> bool *)
+fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
+
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
-(* string -> bool *)
-val is_basic_datatype =
- member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
- @{type_name nat}, @{type_name int},
- "Code_Numeral.code_numeral"]
+(* theory -> (typ option * bool) list -> string -> bool *)
+fun is_basic_datatype thy stds s =
+ member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
+ @{type_name int}, "Code_Numeral.code_numeral"] s orelse
+ (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
@@ -544,7 +581,8 @@
val (co_s, co_Ts) = dest_Type co_T
val _ =
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
- co_s <> "fun" andalso not (is_basic_datatype co_s) then
+ co_s <> "fun" andalso
+ not (is_basic_datatype thy [(NONE, true)] co_s) then
()
else
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
@@ -554,35 +592,6 @@
(* typ -> theory -> theory *)
fun unregister_codatatype co_T = register_codatatype co_T "" []
-type typedef_info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- set_def: thm option, prop_of_Rep: thm, set_name: string,
- Abs_inverse: thm option, Rep_inverse: thm option}
-
-(* theory -> string -> typedef_info *)
-fun typedef_info thy s =
- if is_frac_type thy (Type (s, [])) then
- SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
- Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
- set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
- |> Logic.varify,
- set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
- else case Typedef.get_info thy s of
- SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
- Rep_inverse, ...} =>
- SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
- Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
- set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
- Rep_inverse = SOME Rep_inverse}
- | NONE => NONE
-
-(* theory -> string -> bool *)
-val is_typedef = is_some oo typedef_info
-val is_real_datatype = is_some oo Datatype.get_info
-(* hol_context -> typ -> bool *)
-fun is_standard_datatype ({thy, stds, ...} : hol_context) =
- the o triple_lookup (type_match thy) stds
-
(* theory -> typ -> bool *)
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
| is_quot_type _ (Type ("FSet.fset", _)) = true
@@ -594,7 +603,8 @@
fun is_pure_typedef thy (T as Type (s, _)) =
is_typedef thy s andalso
not (is_real_datatype thy s orelse is_quot_type thy T orelse
- is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
+ is_codatatype thy T orelse is_record_type T orelse
+ is_integer_like_type T)
| is_pure_typedef _ _ = false
fun is_univ_typedef thy (Type (s, _)) =
(case typedef_info thy s of
@@ -607,11 +617,11 @@
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
| NONE => false)
| is_univ_typedef _ _ = false
-fun is_datatype thy (T as Type (s, _)) =
+(* theory -> (typ option * bool) list -> typ -> bool *)
+fun is_datatype thy stds (T as Type (s, _)) =
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
- is_quot_type thy T) andalso
- not (is_basic_datatype s)
- | is_datatype _ _ = false
+ is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+ | is_datatype _ _ _ = false
(* theory -> typ -> (string * typ) list * (string * typ) *)
fun all_record_fields thy T =
@@ -699,15 +709,16 @@
let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
- x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
is_coconstr thy x
end
fun is_stale_constr thy (x as (_, T)) =
is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
not (is_coconstr thy x)
-fun is_constr thy (x as (_, T)) =
+(* theory -> (typ option * bool) list -> styp -> bool *)
+fun is_constr thy stds (x as (_, T)) =
is_constr_like thy x andalso
- not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
+ not (is_basic_datatype thy stds
+ (fst (dest_Type (unarize_type (body_type T))))) andalso
not (is_stale_constr thy x)
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -844,15 +855,16 @@
#> List.foldr (s_conj o swap) @{const True}
(* typ -> term *)
-fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
+fun zero_const T = Const (@{const_name zero_class.zero}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* theory -> typ -> styp list *)
-fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
+(* hol_context -> typ -> styp list *)
+fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
+ (T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
| _ =>
- if is_datatype thy T then
+ if is_datatype thy stds T then
case Datatype.get_info thy s of
SOME {index, descr, ...} =>
let
@@ -883,11 +895,11 @@
[])
| uncached_datatype_constrs _ _ = []
(* hol_context -> typ -> styp list *)
-fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
+fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
| NONE =>
- let val xs = uncached_datatype_constrs thy T in
+ let val xs = uncached_datatype_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
(* hol_context -> bool -> typ -> styp list *)
@@ -930,11 +942,11 @@
else betapply (discr_term_for_constr hol_ctxt x, t)
| _ => betapply (discr_term_for_constr hol_ctxt x, t)
-(* styp -> term -> term *)
-fun nth_arg_sel_term_for_constr (x as (s, T)) n =
+(* theory -> (typ option * bool) list -> styp -> term -> term *)
+fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
let val (arg_Ts, dataT) = strip_type T in
- if dataT = nat_T then
- @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
+ if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
+ @{term "%n::nat. n - 1"}
else if is_pair_type dataT then
Const (nth_sel_for_constr x n)
else
@@ -952,24 +964,26 @@
(List.take (arg_Ts, n)) 0
in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
end
-(* theory -> styp -> term -> int -> typ -> term *)
-fun select_nth_constr_arg thy x t n res_T =
- case strip_comb t of
- (Const x', args) =>
- if x = x' then nth args n
- else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
- else betapply (nth_arg_sel_term_for_constr x n, t)
- | _ => betapply (nth_arg_sel_term_for_constr x n, t)
+(* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
+fun select_nth_constr_arg thy stds x t n res_T =
+ (case strip_comb t of
+ (Const x', args) =>
+ if x = x' then nth args n
+ else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
+ else raise SAME ()
+ | _ => raise SAME())
+ handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
-(* theory -> styp -> term list -> term *)
-fun construct_value _ x [] = Const x
- | construct_value thy (x as (s, _)) args =
+(* theory -> (typ option * bool) list -> styp -> term list -> term *)
+fun construct_value _ _ x [] = Const x
+ | construct_value thy stds (x as (s, _)) args =
let val args = map Envir.eta_contract args in
case hd args of
Const (x' as (s', _)) $ t =>
if is_sel_like_and_no_discr s' andalso
constr_name_for_sel_like s' = s andalso
- forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
+ forall (fn (n, t') =>
+ select_nth_constr_arg thy stds x t n dummyT = t')
(index_seq 0 (length args) ~~ args) then
t
else
@@ -1167,24 +1181,31 @@
user_defs @ built_in_defs
in (defs, built_in_nondefs, user_nondefs) end
-(* bool -> styp -> int option *)
-fun arity_of_built_in_const fast_descrs (s, T) =
+(* theory -> (typ option * bool) list -> bool -> styp -> int option *)
+fun arity_of_built_in_const thy stds fast_descrs (s, T) =
if s = @{const_name If} then
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
- else case AList.lookup (op =)
- (built_in_consts
- |> fast_descrs ? append built_in_descr_consts) s of
- SOME n => SOME n
- | NONE =>
- case AList.lookup (op =) built_in_typed_consts (s, T) of
- SOME n => SOME n
- | NONE =>
- if is_fun_type T andalso is_set_type (domain_type T) then
- AList.lookup (op =) built_in_set_consts s
- else
- NONE
-(* bool -> styp -> bool *)
-val is_built_in_const = is_some oo arity_of_built_in_const
+ else
+ let val std_nats = is_standard_datatype thy stds nat_T in
+ case AList.lookup (op =)
+ (built_in_consts
+ |> std_nats ? append built_in_nat_consts
+ |> fast_descrs ? append built_in_descr_consts) s of
+ SOME n => SOME n
+ | NONE =>
+ case AList.lookup (op =)
+ (built_in_typed_consts
+ |> std_nats ? append built_in_typed_nat_consts)
+ (s, unarize_type T) of
+ SOME n => SOME n
+ | NONE =>
+ if is_fun_type T andalso is_set_type (domain_type T) then
+ AList.lookup (op =) built_in_set_consts s
+ else
+ NONE
+ end
+(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
+val is_built_in_const = is_some oooo arity_of_built_in_const
(* This function is designed to work for both real definition axioms and
simplification rules (equational specifications). *)
@@ -1202,9 +1223,10 @@
(* Here we crucially rely on "Refute.specialize_type" performing a preorder
traversal of the term, without which the wrong occurrence of a constant could
be matched in the face of overloading. *)
-(* theory -> bool -> const_table -> styp -> term list *)
-fun def_props_for_const thy fast_descrs table (x as (s, _)) =
- if is_built_in_const fast_descrs x then
+(* theory -> (typ option * bool) list -> bool -> const_table -> styp
+ -> term list *)
+fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
+ if is_built_in_const thy stds fast_descrs x then
[]
else
these (Symtab.lookup table s)
@@ -1229,10 +1251,11 @@
(* theory -> const_table -> styp -> term option *)
fun def_of_const thy table (x as (s, _)) =
- if is_built_in_const false x orelse original_name s <> s then
+ if is_built_in_const thy [(NONE, false)] false x orelse
+ original_name s <> s then
NONE
else
- x |> def_props_for_const thy false table |> List.last
+ x |> def_props_for_const thy [(NONE, false)] false table |> List.last
|> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
@@ -1282,10 +1305,10 @@
fun table_for get ctxt =
get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
-(* theory -> (string * int) list *)
-fun case_const_names thy =
+(* theory -> (typ option * bool) list -> (string * int) list *)
+fun case_const_names thy stds =
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
- if is_basic_datatype dtype_s then
+ if is_basic_datatype thy stds dtype_s then
I
else
cons (case_name, AList.lookup (op =) descr index
@@ -1366,7 +1389,7 @@
end
| NONE => []
end
-fun optimized_quot_type_axioms thy abs_z =
+fun optimized_quot_type_axioms thy stds abs_z =
let
val abs_T = Type abs_z
val rep_T = rep_type_for_quot_type thy abs_T
@@ -1375,7 +1398,7 @@
val x_var = Var (("x", 0), rep_T)
val y_var = Var (("y", 0), rep_T)
val x = (@{const_name Quot}, rep_T --> abs_T)
- val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
+ val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
val normal_x = normal_t $ x_var
val normal_y = normal_t $ y_var
@@ -1392,31 +1415,31 @@
$ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
end
-(* theory -> int * styp -> term *)
-fun constr_case_body thy (j, (x as (_, T))) =
+(* theory -> (typ option * bool) list -> int * styp -> term *)
+fun constr_case_body thy stds (j, (x as (_, T))) =
let val arg_Ts = binder_types T in
- list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
+ list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
(* hol_context -> typ -> int * styp -> term -> term *)
-fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
+fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
+ $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
$ res_t
(* hol_context -> typ -> typ -> term *)
-fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
+fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
let
val xs = datatype_constrs hol_ctxt dataT
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
val (xs', x) = split_last xs
in
- constr_case_body thy (1, x)
+ constr_case_body thy stds (1, x)
|> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
(* hol_context -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
@@ -1425,65 +1448,56 @@
val rec_T' = List.last Ts
val j = num_record_fields thy rec_T - 1
in
- select_nth_constr_arg thy constr_x t j res_T
+ select_nth_constr_arg thy stds constr_x t j res_T
|> optimized_record_get hol_ctxt s rec_T' res_T
end
| _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
[]))
- | j => select_nth_constr_arg thy constr_x t j res_T
+ | j => select_nth_constr_arg thy stds constr_x t j res_T
end
(* hol_context -> string -> typ -> term -> term -> term *)
-fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
+fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
let
val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
val Ts = binder_types constr_T
val n = length Ts
val special_j = no_of_record_field thy s rec_T
- val ts = map2 (fn j => fn T =>
- let
- val t = select_nth_constr_arg thy constr_x rec_t j T
- in
- if j = special_j then
- betapply (fun_t, t)
- else if j = n - 1 andalso special_j = ~1 then
- optimized_record_update hol_ctxt s
- (rec_T |> dest_Type |> snd |> List.last) fun_t t
- else
- t
- end) (index_seq 0 n) Ts
+ val ts =
+ map2 (fn j => fn T =>
+ let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
+ if j = special_j then
+ betapply (fun_t, t)
+ else if j = n - 1 andalso special_j = ~1 then
+ optimized_record_update hol_ctxt s
+ (rec_T |> dest_Type |> snd |> List.last) fun_t t
+ else
+ t
+ end) (index_seq 0 n) Ts
in list_comb (Const constr_x, ts) end
-(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
- constant, are said to be trivial. For those, we ignore the simplification
- rules and use the definition instead, to ensure that built-in symbols like
- "ord_nat_inst.less_eq_nat" are picked up correctly. *)
-(* theory -> const_table -> styp -> bool *)
-fun has_trivial_definition thy table x =
- case def_of_const thy table x of SOME (Const _) => true | _ => false
-
(* theory -> const_table -> string * typ -> fixpoint_kind *)
fun fixpoint_kind_of_const thy table x =
- if is_built_in_const false x then
+ if is_built_in_const thy [(NONE, false)] false x then
NoFp
else
fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
(* hol_context -> styp -> bool *)
-fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
- : hol_context) x =
- not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
- fixpoint_kind_of_const thy def_table x <> NoFp
-fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
- : hol_context) x =
- exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
+fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
+ ...} : hol_context) x =
+ fixpoint_kind_of_const thy def_table x <> NoFp andalso
+ not (null (def_props_for_const thy stds fast_descrs intro_table x))
+fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
+ ...} : hol_context) x =
+ exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
+ x)))
[!simp_table, psimp_table]
fun is_inductive_pred hol_ctxt =
is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
(is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
- andf (not o has_trivial_definition thy def_table)
(* term * term -> term *)
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1522,7 +1536,7 @@
val unfold_max_depth = 255
(* hol_context -> term -> term *)
-fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
+fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
case_names, def_table, ground_thm_table,
ersatz_table, ...}) =
let
@@ -1537,8 +1551,11 @@
|> ran_T = nat_T ? Integer.max 0
val s = numeral_prefix ^ signed_string_of_int j
in
- if is_integer_type ran_T then
- Const (s, ran_T)
+ if is_integer_like_type ran_T then
+ if is_standard_datatype thy stds ran_T then
+ Const (s, ran_T)
+ else
+ funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
else
do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
$ Const (s, int_T))
@@ -1577,9 +1594,9 @@
(* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
- select_nth_constr_arg thy x (Bound 0) n res_T), [])
+ select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
- (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
+ (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
(* int -> typ list -> term -> styp -> term list -> term *)
and do_const depth Ts t (x as (s, T)) ts =
case AList.lookup (op =) ersatz_table s of
@@ -1588,7 +1605,7 @@
| NONE =>
let
val (const, ts) =
- if is_built_in_const fast_descrs x then
+ if is_built_in_const thy stds fast_descrs x then
(Const x, ts)
else case AList.lookup (op =) case_names s of
SOME n =>
@@ -1600,7 +1617,7 @@
|> do_term (depth + 1) Ts, ts)
end
| _ =>
- if is_constr thy x then
+ if is_constr thy stds x then
(Const x, ts)
else if is_stale_constr thy x then
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
@@ -1635,7 +1652,7 @@
| n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
else if is_rep_fun thy x then
let val x' = mate_of_rep_fun thy x in
- if is_constr thy x' then
+ if is_constr thy stds x' then
select_nth_constr_arg_with_args depth Ts x' ts 0
(range_type T)
else
@@ -1659,7 +1676,7 @@
in do_term 0 [] end
(* hol_context -> typ -> term list *)
-fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
val set_T = T --> bool_T
@@ -1677,8 +1694,8 @@
fun nth_sub_bisim x n nth_T =
(if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
else HOLogic.eq_const nth_T)
- $ select_nth_constr_arg thy x x_var n nth_T
- $ select_nth_constr_arg thy x y_var n nth_T
+ $ select_nth_constr_arg thy stds x x_var n nth_T
+ $ select_nth_constr_arg thy stds x y_var n nth_T
(* styp -> term *)
fun case_func (x as (_, T)) =
let
@@ -1695,7 +1712,7 @@
map case_func xs @ [x_var]))),
HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
$ (Const (@{const_name insert}, T --> set_T --> set_T)
- $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
+ $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
|> map HOLogic.mk_Trueprop
end
@@ -1753,9 +1770,9 @@
(* hol_context -> const_table -> styp -> bool *)
fun uncached_is_well_founded_inductive_pred
- ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
+ ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
: hol_context) (x as (_, T)) =
- case def_props_for_const thy fast_descrs intro_table x of
+ case def_props_for_const thy stds fast_descrs intro_table x of
[] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
[Const x])
| intro_ts =>
@@ -1999,10 +2016,10 @@
raw_inductive_pred_axiom hol_ctxt x
(* hol_context -> styp -> term list *)
-fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
+fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
psimp_table, ...}) (x as (s, _)) =
- case def_props_for_const thy fast_descrs (!simp_table) x of
- [] => (case def_props_for_const thy fast_descrs psimp_table x of
+ case def_props_for_const thy stds fast_descrs (!simp_table) x of
+ [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
[] => [inductive_pred_axiom hol_ctxt x]
| psimps => psimps)
| simps => simps
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Feb 18 18:48:07 2010 +0100
@@ -131,8 +131,7 @@
let
(* int -> int -> int -> KK.int_bound list *)
fun aux 0 _ _ = []
- | aux 1 pow_of_two j =
- if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
+ | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
| aux iter pow_of_two j =
(SOME pow_of_two, [single_atom j]) ::
aux (iter - 1) (2 * pow_of_two) (j + 1)
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 18 18:48:07 2010 +0100
@@ -264,8 +264,8 @@
-> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
-> typ -> rep -> int list list -> term *)
fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
- ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
- ofs, ...} : scope) sel_names rel_table bounds =
+ ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
+ datatypes, ofs, ...} : scope) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
(* int list list -> int *)
@@ -388,7 +388,7 @@
if j = 0 then @{const False} else @{const True}
| term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
| term_for_atom seen T _ j k =
- if T = nat_T then
+ if T = nat_T andalso is_standard_datatype thy stds nat_T then
HOLogic.mk_number nat_T j
else if T = int_T then
HOLogic.mk_number int_T (int_for_atom (k, 0) j)
@@ -713,7 +713,9 @@
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
datatypes |> filter #deep |> List.partition #co
- ||> append (integer_datatype nat_T @ integer_datatype int_T)
+ ||> append (integer_datatype int_T
+ |> is_standard_datatype thy stds nat_T
+ ? append (integer_datatype nat_T))
val block_of_datatypes =
if show_datatypes andalso not (null datatypes) then
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 18 18:48:07 2010 +0100
@@ -130,7 +130,7 @@
fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
| could_exist_alpha_sub_ctype thy alpha_T T =
- (T = alpha_T orelse is_datatype thy T)
+ (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
(* ctype -> bool *)
fun exists_alpha_sub_ctype CAlpha = true
@@ -545,8 +545,9 @@
handle List.Empty => initial_gamma
(* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
- max_fresh, ...}) =
+fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
+ def_table, ...},
+ alpha_T, max_fresh, ...}) =
let
(* typ -> ctype *)
val ctype_for = fresh_ctype_for_type cdata
@@ -663,10 +664,6 @@
in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
| @{const_name trancl} => do_fragile_set_operation T accum
| @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
- | @{const_name semilattice_inf_fun_inst.inf_fun} =>
- do_robust_set_operation T accum
- | @{const_name semilattice_sup_fun_inst.sup_fun} =>
- do_robust_set_operation T accum
| @{const_name finite} =>
let val C1 = ctype_for (domain_type (domain_type T)) in
(CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
@@ -710,19 +707,6 @@
(CFun (a_set_C, S Minus,
CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
end
- | @{const_name minus_fun_inst.minus_fun} =>
- let
- val set_T = domain_type T
- val left_set_C = ctype_for set_T
- val right_set_C = ctype_for set_T
- in
- (CFun (left_set_C, S Minus,
- CFun (right_set_C, S Minus, left_set_C)),
- (gamma, cset |> add_ctype_is_right_unique right_set_C
- |> add_is_sub_ctype right_set_C left_set_C))
- end
- | @{const_name ord_fun_inst.less_eq_fun} =>
- do_fragile_set_operation T accum
| @{const_name Tha} =>
let
val a_C = ctype_for (domain_type (domain_type T))
@@ -732,24 +716,44 @@
let val dom_C = ctype_for (domain_type T) in
(CFun (dom_C, S Minus, dom_C), accum)
end
- | _ => if is_sel s then
- if constr_name_for_sel_like s = @{const_name FunBox} then
- let val dom_C = ctype_for (domain_type T) in
- (CFun (dom_C, S Minus, dom_C), accum)
- end
- else
- (ctype_for_sel cdata x, accum)
- else if is_constr thy x then
- (ctype_for_constr cdata x, accum)
- else if is_built_in_const true x then
- case def_of_const thy def_table x of
- SOME t' => do_term t' accum
- | NONE => (print_g ("*** built-in " ^ s); unsolvable)
- else
- let val C = ctype_for T in
- (C, ({bounds = bounds, frees = frees,
- consts = (x, C) :: consts}, cset))
- end)
+ | _ =>
+ if s = @{const_name minus_class.minus} andalso
+ is_set_type (domain_type T) then
+ let
+ val set_T = domain_type T
+ val left_set_C = ctype_for set_T
+ val right_set_C = ctype_for set_T
+ in
+ (CFun (left_set_C, S Minus,
+ CFun (right_set_C, S Minus, left_set_C)),
+ (gamma, cset |> add_ctype_is_right_unique right_set_C
+ |> add_is_sub_ctype right_set_C left_set_C))
+ end
+ else if s = @{const_name ord_class.less_eq} andalso
+ is_set_type (domain_type T) then
+ do_fragile_set_operation T accum
+ else if (s = @{const_name semilattice_inf_class.inf} orelse
+ s = @{const_name semilattice_sup_class.sup}) andalso
+ is_set_type (domain_type T) then
+ do_robust_set_operation T accum
+ else if is_sel s then
+ if constr_name_for_sel_like s = @{const_name FunBox} then
+ let val dom_C = ctype_for (domain_type T) in
+ (CFun (dom_C, S Minus, dom_C), accum)
+ end
+ else
+ (ctype_for_sel cdata x, accum)
+ else if is_constr thy stds x then
+ (ctype_for_constr cdata x, accum)
+ else if is_built_in_const thy stds fast_descrs x then
+ case def_of_const thy def_table x of
+ SOME t' => do_term t' accum
+ | NONE => (print_g ("*** built-in " ^ s); unsolvable)
+ else
+ let val C = ctype_for T in
+ (C, ({bounds = bounds, frees = frees,
+ consts = (x, C) :: consts}, cset))
+ end)
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
SOME C => (C, accum)
@@ -881,20 +885,21 @@
val bounteous_consts = [@{const_name bisim}]
(* term -> bool *)
-fun is_harmless_axiom t =
- Term.add_consts t [] |> filter_out (is_built_in_const true)
+fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
+ Term.add_consts t []
+ |> filter_out (is_built_in_const thy stds fast_descrs)
|> (forall (member (op =) harmless_consts o original_name o fst)
orf exists (member (op =) bounteous_consts o fst))
(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_nondefinitional_axiom cdata sn t =
- not (is_harmless_axiom t) ? consider_general_formula cdata sn t
+fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
+ not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
(* cdata -> term -> accumulator -> accumulator *)
fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
consider_nondefinitional_axiom cdata Plus t
- else if is_harmless_axiom t then
+ else if is_harmless_axiom hol_ctxt t then
I
else
let
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Feb 18 18:48:07 2010 +0100
@@ -467,7 +467,7 @@
| factorize z = [z]
(* hol_context -> op2 -> term -> nut *)
-fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
let
(* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
@@ -603,46 +603,62 @@
Const (@{const_name top}, _) => Cst (False, bool_T, Any)
| _ => Op1 (Finite, bool_T, Any, sub t1))
| (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
- | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
- Cst (Num 0, T, Any)
- | (Const (@{const_name one_nat_inst.one_nat}, T), []) =>
- Cst (Num 1, T, Any)
- | (Const (@{const_name plus_nat_inst.plus_nat}, T), []) =>
- Cst (Add, T, Any)
- | (Const (@{const_name minus_nat_inst.minus_nat}, T), []) =>
- Cst (Subtract, T, Any)
- | (Const (@{const_name times_nat_inst.times_nat}, T), []) =>
- Cst (Multiply, T, Any)
- | (Const (@{const_name div_nat_inst.div_nat}, T), []) =>
- Cst (Divide, T, Any)
- | (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) =>
- Op2 (Less, bool_T, Any, sub t1, sub t2)
- | (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) =>
- Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+ | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
+ if is_built_in_const thy stds false x then
+ Cst (Num 0, T, Any)
+ else if is_constr thy stds x then
+ let val (s', T') = discr_for_constr x in
+ Construct ([ConstName (s', T', Any)], T, Any, [])
+ end
+ else
+ ConstName (s, T, Any)
+ | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
+ else ConstName (s, T, Any)
+ | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Add, T, Any)
+ else ConstName (s, T, Any)
+ | (Const (@{const_name minus_class.minus},
+ Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ [t1, t2]) =>
+ Op2 (SetDifference, T1, Any, sub t1, sub t2)
+ | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
+ else ConstName (s, T, Any)
+ | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
+ else ConstName (s, T, Any)
+ | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
+ if is_built_in_const thy stds false x then Cst (Divide, T, Any)
+ else ConstName (s, T, Any)
+ | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
+ ts as [t1, t2]) =>
+ if is_built_in_const thy stds false x then
+ Op2 (Less, bool_T, Any, sub t1, sub t2)
+ else
+ do_apply t0 ts
+ | (Const (@{const_name ord_class.less_eq},
+ Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
+ [t1, t2]) =>
+ Op2 (Subset, bool_T, Any, sub t1, sub t2)
+ (* FIXME: find out if this case is necessary *)
+ | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
+ ts as [t1, t2]) =>
+ if is_built_in_const thy stds false x then
+ Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+ else
+ do_apply t0 ts
| (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
| (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
- | (Const (@{const_name zero_int_inst.zero_int}, T), []) =>
- Cst (Num 0, T, Any)
- | (Const (@{const_name one_int_inst.one_int}, T), []) =>
- Cst (Num 1, T, Any)
- | (Const (@{const_name plus_int_inst.plus_int}, T), []) =>
- Cst (Add, T, Any)
- | (Const (@{const_name minus_int_inst.minus_int}, T), []) =>
- Cst (Subtract, T, Any)
- | (Const (@{const_name times_int_inst.times_int}, T), []) =>
- Cst (Multiply, T, Any)
- | (Const (@{const_name div_int_inst.div_int}, T), []) =>
- Cst (Divide, T, Any)
- | (Const (@{const_name uminus_int_inst.uminus_int}, T), []) =>
- let val num_T = domain_type T in
- Op2 (Apply, num_T --> num_T, Any,
- Cst (Subtract, num_T --> num_T --> num_T, Any),
- Cst (Num 0, num_T, Any))
- end
- | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
- Op2 (Less, bool_T, Any, sub t1, sub t2)
- | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
- Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+ | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
+ if is_built_in_const thy stds false x then
+ let val num_T = domain_type T in
+ Op2 (Apply, num_T --> num_T, Any,
+ Cst (Subtract, num_T --> num_T --> num_T, Any),
+ Cst (Num 0, num_T, Any))
+ end
+ else
+ ConstName (s, T, Any)
| (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
| (Const (@{const_name is_unknown}, T), [t1]) =>
Op1 (IsUnknown, bool_T, Any, sub t1)
@@ -655,18 +671,16 @@
| (Const (@{const_name of_nat},
T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
Cst (NatToInt, T, Any)
- | (Const (@{const_name semilattice_inf_fun_inst.inf_fun}, T),
- [t1, t2]) =>
- Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2)
- | (Const (@{const_name semilattice_sup_fun_inst.sup_fun}, T),
- [t1, t2]) =>
- Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2)
- | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) =>
- Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2)
- | (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) =>
- Op2 (Subset, bool_T, Any, sub t1, sub t2)
+ | (Const (@{const_name semilattice_inf_class.inf},
+ Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ [t1, t2]) =>
+ Op2 (Intersect, T1, Any, sub t1, sub t2)
+ | (Const (@{const_name semilattice_sup_class.sup},
+ Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+ [t1, t2]) =>
+ Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
- if is_constr thy x then
+ if is_constr thy stds x then
case num_binder_types T - length ts of
0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
o nth_sel_for_constr x)
@@ -678,7 +692,7 @@
else if String.isPrefix numeral_prefix s then
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
else
- (case arity_of_built_in_const fast_descrs x of
+ (case arity_of_built_in_const thy stds fast_descrs x of
SOME n =>
(case n - length ts of
0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 18 18:48:07 2010 +0100
@@ -43,11 +43,9 @@
| may_use_binary_ints _ = true
fun should_use_binary_ints (t1 $ t2) =
should_use_binary_ints t1 orelse should_use_binary_ints t2
- | should_use_binary_ints (Const (s, _)) =
- member (op =) [@{const_name times_nat_inst.times_nat},
- @{const_name div_nat_inst.div_nat},
- @{const_name times_int_inst.times_int},
- @{const_name div_int_inst.div_int}] s orelse
+ | should_use_binary_ints (Const (s, T)) =
+ ((s = @{const_name times} orelse s = @{const_name div}) andalso
+ is_integer_type (body_type T)) orelse
(String.isPrefix numeral_prefix s andalso
let val n = the (Int.fromString (unprefix numeral_prefix s)) in
n < ~ binary_int_threshold orelse n > binary_int_threshold
@@ -65,7 +63,8 @@
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
| aux (t as Const (x as (s, _))) args table =
- if is_built_in_const true x orelse is_constr_like thy x orelse
+ if is_built_in_const thy [(NONE, true)] true x orelse
+ is_constr_like thy x orelse
is_sel s orelse s = @{const_name Sigma} then
table
else
@@ -119,7 +118,7 @@
(** Boxing **)
(* hol_context -> typ -> term -> term *)
-fun constr_expand (hol_ctxt as {thy, ...}) T t =
+fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
(case head_of t of
Const x => if is_constr_like thy x then t else raise SAME ()
| _ => raise SAME ())
@@ -134,12 +133,13 @@
datatype_constrs hol_ctxt T |> hd
val arg_Ts = binder_types T'
in
- list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
+ list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
(index_seq 0 (length arg_Ts)) arg_Ts)
end
(* hol_context -> bool -> term -> term *)
-fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
+ orig_t =
let
(* typ -> typ *)
fun box_relational_operator_type (Type ("fun", Ts)) =
@@ -172,8 +172,9 @@
|> coerce_term (new_T1 :: Ts) new_T2 old_T2)
|> Envir.eta_contract
|> new_s <> "fun"
- ? construct_value thy (@{const_name FunBox},
- Type ("fun", new_Ts) --> new_T) o single
+ ? construct_value thy stds
+ (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+ o single
| t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
\coerce_term", [t']))
| (Type (new_s, new_Ts as [new_T1, new_T2]),
@@ -185,12 +186,12 @@
if new_s = "fun" then
coerce_term Ts new_T (Type ("fun", old_Ts)) t1
else
- construct_value thy
+ construct_value thy stds
(@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- [coerce_term Ts (Type ("fun", new_Ts))
- (Type ("fun", old_Ts)) t1]
+ [coerce_term Ts (Type ("fun", new_Ts))
+ (Type ("fun", old_Ts)) t1]
| Const _ $ t1 $ t2 =>
- construct_value thy
+ construct_value thy stds
(if new_s = "*" then @{const_name Pair}
else @{const_name PairBox}, new_Ts ---> new_T)
[coerce_term Ts new_T1 old_T1 t1,
@@ -302,7 +303,7 @@
Const (s, if s = @{const_name converse} orelse
s = @{const_name trancl} then
box_relational_operator_type T
- else if is_built_in_const fast_descrs x orelse
+ else if is_built_in_const thy stds fast_descrs x orelse
s = @{const_name Sigma} then
T
else if is_constr_like thy x then
@@ -325,7 +326,7 @@
betapply (if s1 = "fun" then
t1
else
- select_nth_constr_arg thy
+ select_nth_constr_arg thy stds
(@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
(Type ("fun", Ts1)), t2)
end
@@ -341,7 +342,7 @@
betapply (if s1 = "fun" then
t1
else
- select_nth_constr_arg thy
+ select_nth_constr_arg thy stds
(@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
(Type ("fun", Ts1)), t2)
end
@@ -371,13 +372,14 @@
| aux _ = true
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
- -> term * term list *)
-fun pull_out_constr_comb thy Ts relax k level t args seen =
+(* hol_context -> typ list -> bool -> int -> int -> term -> term list
+ -> term list -> term * term list *)
+fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
+ args seen =
let val t_comb = list_comb (t, args) in
case t of
Const x =>
- if not relax andalso is_constr thy x andalso
+ if not relax andalso is_constr thy stds x andalso
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
has_heavy_bounds_or_vars Ts level t_comb andalso
not (loose_bvar (t_comb, level)) then
@@ -398,8 +400,8 @@
(index_seq 0 n) seen
end
-(* theory -> bool -> term -> term *)
-fun pull_out_universal_constrs thy def t =
+(* hol_context -> bool -> term -> term *)
+fun pull_out_universal_constrs hol_ctxt def t =
let
val k = maxidx_of_term t + 1
(* typ list -> bool -> term -> term list -> term list -> term * term list *)
@@ -421,7 +423,7 @@
let val (t2, seen) = do_term Ts def t2 [] seen in
do_term Ts def t1 (t2 :: args) seen
end
- | _ => pull_out_constr_comb thy Ts def k 0 t args seen
+ | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
(* typ list -> bool -> bool -> term -> term -> term -> term list
-> term * term list *)
and do_eq_or_imp Ts eq def t0 t1 t2 seen =
@@ -440,8 +442,8 @@
fun mk_exists v t =
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
-(* theory -> term -> term *)
-fun pull_out_existential_constrs thy t =
+(* hol_context -> term -> term *)
+fun pull_out_existential_constrs hol_ctxt t =
let
val k = maxidx_of_term t + 1
(* typ list -> int -> term -> term list -> term list -> term * term list *)
@@ -468,13 +470,13 @@
in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
| _ =>
if num_exists > 0 then
- pull_out_constr_comb thy Ts false k num_exists t args seen
+ pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen
else
(list_comb (t, args), seen)
in aux [] 0 t [] [] |> fst end
(* hol_context -> bool -> term -> term *)
-fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
let
(* styp -> int *)
val num_occs_of_var =
@@ -509,7 +511,7 @@
| (Const (x as (s, T)), args) =>
let val arg_Ts = binder_types T in
if length arg_Ts = length args andalso
- (is_constr thy x orelse s = @{const_name Pair}) andalso
+ (is_constr thy stds x orelse s = @{const_name Pair}) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
discriminate_value hol_ctxt x t1 ::
@@ -524,7 +526,8 @@
else t0 $ aux false t2 $ aux false t1
(* styp -> term -> int -> typ -> term -> term *)
and sel_eq x t n nth_T nth_t =
- HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
+ HOLogic.eq_const nth_T $ nth_t
+ $ select_nth_constr_arg thy stds x t n nth_T
|> aux false
in aux axiom t end
@@ -565,34 +568,40 @@
aux (t1 :: prems) (Term.add_vars t1 zs) t2
in aux [] [] end
-(* theory -> int -> term list -> term list -> (term * term list) option *)
-fun find_bound_assign _ _ _ [] = NONE
- | find_bound_assign thy j seen (t :: ts) =
- let
- (* bool -> term -> term -> (term * term list) option *)
- fun aux pass1 t1 t2 =
- (if loose_bvar1 (t2, j) then
- if pass1 then aux false t2 t1 else raise SAME ()
- else case t1 of
- Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
- | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
- if j' = j andalso
- s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
- SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
- ts @ seen)
- else
- raise SAME ()
- | _ => raise SAME ())
- handle SAME () => find_bound_assign thy j (t :: seen) ts
- in
- case t of
- Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
- | _ => find_bound_assign thy j (t :: seen) ts
- end
+(* theory -> (typ option * bool) list -> int -> term list -> term list
+ -> (term * term list) option *)
+fun find_bound_assign thy stds j =
+ let
+ (* term list -> term list -> (term * term list) option *)
+ fun do_term _ [] = NONE
+ | do_term seen (t :: ts) =
+ let
+ (* bool -> term -> term -> (term * term list) option *)
+ fun do_eq pass1 t1 t2 =
+ (if loose_bvar1 (t2, j) then
+ if pass1 then do_eq false t2 t1 else raise SAME ()
+ else case t1 of
+ Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
+ | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+ if j' = j andalso
+ s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
+ SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
+ [t2], ts @ seen)
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () => do_term (t :: seen) ts
+ in
+ case t of
+ Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+ | _ => do_term (t :: seen) ts
+ end
+ in do_term end
(* int -> term -> term -> term *)
fun subst_one_bound j arg t =
let
+ (* term * int -> term *)
fun aux (Bound i, lev) =
if i < lev then raise SAME ()
else if i = lev then incr_boundvars (lev - j) arg
@@ -604,13 +613,13 @@
| aux _ = raise SAME ()
in aux (t, j) handle SAME () => t end
-(* theory -> term -> term *)
-fun destroy_existential_equalities thy =
+(* hol_context -> term -> term *)
+fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
let
(* string list -> typ list -> term list -> term *)
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
- (case find_bound_assign thy (length ss) [] ts of
+ (case find_bound_assign thy stds (length ss) [] ts of
SOME (_, []) => @{const True}
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
@@ -704,13 +713,11 @@
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
val (pref, connective, set_oper) =
if gfp then
- (lbfp_prefix,
- @{const "op |"},
- @{const_name semilattice_sup_fun_inst.sup_fun})
+ (lbfp_prefix, @{const "op |"},
+ @{const_name semilattice_sup_class.sup})
else
- (ubfp_prefix,
- @{const "op &"},
- @{const_name semilattice_inf_fun_inst.inf_fun})
+ (ubfp_prefix, @{const "op &"},
+ @{const_name semilattice_inf_class.inf})
(* unit -> term *)
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js depth polar
@@ -854,7 +861,7 @@
(index_seq 0 (length args) ~~ args)
val _ = not (null eligible_args) orelse raise SAME ()
val old_axs = equational_fun_axioms hol_ctxt x
- |> map (destroy_existential_equalities thy)
+ |> map (destroy_existential_equalities hol_ctxt)
val static_params = static_args_in_terms hol_ctxt x old_axs
val fixed_js = overlapping_indices static_params eligible_args
val _ = not (null fixed_js) orelse raise SAME ()
@@ -1016,8 +1023,8 @@
(* hol_context -> term -> (term list * term list) * (bool * bool) *)
fun axioms_for_term
- (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
- def_table, nondef_table, user_nondefs, ...}) t =
+ (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
+ evals, def_table, nondef_table, user_nondefs, ...}) t =
let
type accumulator = styp list * (term list * term list)
(* (term list * term list -> term list)
@@ -1051,7 +1058,8 @@
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if member (op =) xs x orelse is_built_in_const fast_descrs x then
+ (if member (op =) xs x orelse
+ is_built_in_const thy stds fast_descrs x then
accum
else
let val accum as (xs, _) = (x :: xs, axs) in
@@ -1072,7 +1080,7 @@
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
accum
end
- else if is_constr thy x then
+ else if is_constr thy stds x then
accum
else if is_equational_fun hol_ctxt x then
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
@@ -1127,7 +1135,7 @@
#> (if is_pure_typedef thy T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
else if is_quot_type thy T then
- fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
+ fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
else if max_bisim_depth >= 0 andalso is_codatatype thy T then
fold (add_maybe_def_axiom depth)
(codatatype_bisim_axioms hol_ctxt T)
@@ -1377,8 +1385,8 @@
(* hol_context -> term
-> ((term list * term list) * (bool * bool)) * term * bool *)
-fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
- skolemize, uncurry, ...}) t =
+fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
+ boxes, skolemize, uncurry, ...}) t =
let
val skolem_depth = if skolemize then 4 else ~1
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
@@ -1388,12 +1396,12 @@
|> specialize_consts_in_term hol_ctxt 0
|> `(axioms_for_term hol_ctxt)
val binarize =
+ is_standard_datatype thy stds nat_T andalso
case binary_ints of
SOME false => false
- | _ =>
- forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
- (binary_ints = SOME true orelse
- exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ (binary_ints = SOME true orelse
+ exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
val box = exists (not_equal (SOME false) o snd) boxes
val table =
Termtab.empty |> uncurry
@@ -1403,12 +1411,12 @@
binarize ? binarize_nat_and_int_in_term
#> uncurry ? uncurry_term table
#> box ? box_fun_and_pair_in_term hol_ctxt def
- #> destroy_constrs ? (pull_out_universal_constrs thy def
- #> pull_out_existential_constrs thy
+ #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
+ #> pull_out_existential_constrs hol_ctxt
#> destroy_pulled_out_constrs hol_ctxt def)
#> curry_assms
#> destroy_universal_equalities
- #> destroy_existential_equalities thy
+ #> destroy_existential_equalities hol_ctxt
#> simplify_constrs_and_sels thy
#> distribute_quantifiers
#> push_quantifiers_inward thy
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 18 18:48:07 2010 +0100
@@ -111,7 +111,7 @@
| is_complete_type dtypes (Type ("*", Ts)) =
forall (is_complete_type dtypes) Ts
| is_complete_type dtypes T =
- not (is_integer_type T) andalso not (is_bit_type T) andalso
+ not (is_integer_like_type T) andalso not (is_bit_type T) andalso
#complete (the (datatype_spec dtypes T))
handle Option.Option => true
and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
@@ -135,8 +135,9 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
-fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
- bits, bisim_depth, datatypes, ...} : scope) =
+fun quintuple_for_scope quote
+ ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+ datatypes, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@{typ bisim_iterator}]
@@ -144,7 +145,7 @@
card_assigns |> filter_out (member (op =) boring_Ts o fst)
|> List.partition (is_fp_iterator_type o fst)
val (secondary_card_assigns, primary_card_assigns) =
- card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
+ card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
o fst)
val cards =
map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
@@ -400,7 +401,8 @@
-> int Typtab.table *)
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
- if k = 1 orelse is_integer_type T orelse is_bit_type T then
+ if k = 1 orelse is_fp_iterator_type T orelse is_integer_type T
+ orelse T = @{typ bisim_iterator} orelse is_bit_type T then
aux next reusable assigns
else if length (these (Option.map #constrs (datatype_spec dtypes T)))
> 1 then
@@ -468,19 +470,20 @@
end
(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
deep_dataTs (desc as (card_assigns, _)) (T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
- val standard = is_standard_datatype hol_ctxt T
+ val standard = is_standard_datatype thy stds T
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
val complete = has_exact_card hol_ctxt card_assigns T
- val concrete = xs |> maps (binder_types o snd) |> maps binder_types
- |> forall (has_exact_card hol_ctxt card_assigns)
+ val concrete = is_word_type T orelse
+ (xs |> maps (binder_types o snd) |> maps binder_types
+ |> forall (has_exact_card hol_ctxt card_assigns))
(* int -> int *)
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
@@ -502,12 +505,12 @@
(map snd card_assigns @ map snd max_assigns) 0)
(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
+fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
deep_dataTs (desc as (card_assigns, _)) =
let
val datatypes =
map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
- desc) (filter (is_datatype thy o fst) card_assigns)
+ desc) (filter (is_datatype thy stds o fst) card_assigns)
val bits = card_of_type card_assigns @{typ signed_bit} - 1
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
card_of_type card_assigns @{typ unsigned_bit}
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Feb 18 18:48:07 2010 +0100
@@ -215,10 +215,11 @@
SOME z => SOME z
| NONE => ps |> find_first (is_none o fst) |> Option.map snd
(* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
-fun triple_lookup eq ps key =
- case AList.lookup (op =) ps (SOME key) of
- SOME z => SOME z
- | NONE => double_lookup eq ps key
+fun triple_lookup _ [(NONE, z)] _ = SOME z
+ | triple_lookup eq ps key =
+ case AList.lookup (op =) ps (SOME key) of
+ SOME z => SOME z
+ | NONE => double_lookup eq ps key
(* string -> string -> bool *)
fun is_substring_of needle stack =