make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 20:46:50 2010 +0100
@@ -293,7 +293,7 @@
val _ = null (Term.add_tvars assms_t []) orelse
raise NOT_SUPPORTED "schematic type variables"
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = preprocess_term hol_ctxt assms_t
+ core_t, binarize) = preprocess_term hol_ctxt assms_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -345,12 +345,13 @@
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
| _ => is_type_always_monotonic T orelse
- formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
+ formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
fun is_deep_datatype T =
is_datatype thy T andalso
- (is_word_type T orelse
+ (not standard 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 (core_t :: def_ts @ nondef_ts)
+ val all_Ts = ground_types_in_terms hol_ctxt binarize
+ (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
exists (member (op =) [nat_T, int_T]) all_Ts then
@@ -514,8 +515,9 @@
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
- val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
- rel_table datatypes
+ val dtype_axioms =
+ 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
@@ -545,9 +547,10 @@
if loc = "Nitpick_Kodkod.check_arity" andalso
not (Typtab.is_empty ofs) then
problem_for_scope unsound
- {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
- bits = bits, bisim_depth = bisim_depth,
- datatypes = datatypes, ofs = Typtab.empty}
+ {hol_ctxt = hol_ctxt, binarize = binarize,
+ card_assigns = card_assigns, bits = bits,
+ bisim_depth = bisim_depth, datatypes = datatypes,
+ ofs = Typtab.empty}
else if loc = "Nitpick.pick_them_nits_in_term.\
\problem_for_scope" then
NONE
@@ -905,8 +908,8 @@
end
val (skipped, the_scopes) =
- all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
- bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
+ all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
+ iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
val _ = if skipped > 0 then
print_m (fn () => "Too many scopes. Skipping " ^
string_of_int skipped ^ " scope" ^
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 20:46:50 2010 +0100
@@ -64,7 +64,7 @@
val strip_any_connective : term -> term list * term
val conjuncts_of : term -> term list
val disjuncts_of : term -> term list
- val unbit_and_unbox_type : typ -> typ
+ val unarize_and_unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
val shortest_name : string -> string
@@ -117,11 +117,14 @@
val is_sel : string -> bool
val is_sel_like_and_no_discr : string -> bool
val box_type : hol_context -> boxability -> typ -> typ
+ val binarize_nat_and_int_in_type : typ -> typ
+ val binarize_nat_and_int_in_term : term -> term
val discr_for_constr : styp -> styp
val num_sels_for_constr_type : typ -> int
val nth_sel_name_for_constr_name : string -> int -> string
val nth_sel_for_constr : styp -> int -> styp
- val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
+ val binarized_and_boxed_nth_sel_for_constr :
+ hol_context -> bool -> styp -> int -> styp
val sel_no_from_name : string -> int
val close_form : term -> term
val eta_expand : typ list -> term -> int -> term
@@ -132,10 +135,11 @@
val register_codatatype : typ -> string -> styp list -> theory -> theory
val unregister_codatatype : typ -> theory -> theory
val datatype_constrs : hol_context -> typ -> styp list
- val boxed_datatype_constrs : hol_context -> typ -> styp list
+ val binarized_and_boxed_datatype_constrs :
+ hol_context -> bool -> typ -> styp list
val num_datatype_constrs : hol_context -> typ -> int
val constr_name_for_sel_like : string -> string
- val boxed_constr_for_sel : hol_context -> styp -> styp
+ 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
@@ -176,8 +180,8 @@
val equational_fun_axioms : hol_context -> styp -> term list
val is_equational_fun_surely_complete : hol_context -> styp -> bool
val merge_type_vars_in_terms : term list -> term list
- val ground_types_in_type : hol_context -> typ -> typ list
- val ground_types_in_terms : hol_context -> term list -> typ list
+ val ground_types_in_type : hol_context -> bool -> typ -> typ list
+ val ground_types_in_terms : hol_context -> bool -> term list -> typ list
val format_type : int list -> int list -> typ -> typ
val format_term_type :
theory -> const_table -> (term option * int list) list -> term -> typ
@@ -376,23 +380,23 @@
(@{const_name ord_fun_inst.less_eq_fun}, 2)]
(* typ -> typ *)
-fun unbit_type @{typ "unsigned_bit word"} = nat_T
- | unbit_type @{typ "signed_bit word"} = int_T
- | unbit_type @{typ bisim_iterator} = nat_T
- | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
- | unbit_type T = T
-fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
- unbit_and_unbox_type (Type ("fun", Ts))
- | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
- Type ("*", map unbit_and_unbox_type Ts)
- | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
- | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
- | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
- | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
- Type (s, map unbit_and_unbox_type Ts)
- | unbit_and_unbox_type T = T
+fun unarize_type @{typ "unsigned_bit word"} = nat_T
+ | unarize_type @{typ "signed_bit word"} = int_T
+ | unarize_type @{typ bisim_iterator} = nat_T
+ | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
+ | unarize_type T = T
+fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
+ unarize_and_unbox_type (Type ("fun", Ts))
+ | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
+ Type ("*", map unarize_and_unbox_type Ts)
+ | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
+ | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
+ | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
+ | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
+ Type (s, map unarize_and_unbox_type Ts)
+ | unarize_and_unbox_type T = T
(* Proof.context -> typ -> string *)
-fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
+fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
@@ -692,7 +696,7 @@
member (op =) [@{const_name FunBox}, @{const_name PairBox},
@{const_name Quot}, @{const_name Zero_Rep},
@{const_name Suc_Rep}] s orelse
- let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
+ 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
@@ -703,7 +707,7 @@
not (is_coconstr thy x)
fun is_constr thy (x as (_, T)) =
is_constr_like thy x andalso
- not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
+ not (is_basic_datatype (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
@@ -757,6 +761,15 @@
else InPair)) Ts)
| _ => T
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+ | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+ | binarize_nat_and_int_in_type (Type (s, Ts)) =
+ Type (s, map binarize_nat_and_int_in_type Ts)
+ | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
(* styp -> styp *)
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
@@ -773,9 +786,10 @@
| nth_sel_for_constr (s, T) n =
(nth_sel_name_for_constr_name s n,
body_type T --> nth (maybe_curried_binder_types T) n)
-(* hol_context -> styp -> int -> styp *)
-fun boxed_nth_sel_for_constr hol_ctxt =
- apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
+(* hol_context -> bool -> styp -> int -> styp *)
+fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
+ apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
+ oo nth_sel_for_constr
(* string -> int *)
fun sel_no_from_name s =
@@ -876,8 +890,10 @@
let val xs = uncached_datatype_constrs thy T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
-fun boxed_datatype_constrs hol_ctxt =
- map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
+(* hol_context -> bool -> typ -> styp list *)
+fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
+ map (apsnd ((binarize ? binarize_nat_and_int_in_type)
+ o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
(* hol_context -> typ -> int *)
val num_datatype_constrs = length oo datatype_constrs
@@ -885,10 +901,12 @@
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
| constr_name_for_sel_like s' = original_name s'
-(* hol_context -> styp -> styp *)
-fun boxed_constr_for_sel hol_ctxt (s', T') =
+(* hol_context -> bool -> styp -> styp *)
+fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
let val s = constr_name_for_sel_like s' in
- AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
+ AList.lookup (op =)
+ (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
+ s
|> the |> pair s
end
@@ -2013,28 +2031,33 @@
| coalesce T = T
in map (map_types (map_atyps coalesce)) ts end
-(* hol_context -> typ -> typ list -> typ list *)
-fun add_ground_types hol_ctxt T accum =
- case T of
- Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
- | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
- | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
- | Type (_, Ts) =>
- if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
- accum
- else
- T :: accum
- |> fold (add_ground_types hol_ctxt)
- (case boxed_datatype_constrs hol_ctxt T of
- [] => Ts
- | xs => map snd xs)
- | _ => insert (op =) T accum
+(* hol_context -> bool -> typ -> typ list -> typ list *)
+fun add_ground_types hol_ctxt binarize =
+ let
+ fun aux T accum =
+ case T of
+ Type ("fun", Ts) => fold aux Ts accum
+ | Type ("*", Ts) => fold aux Ts accum
+ | Type (@{type_name itself}, [T1]) => aux T1 accum
+ | Type (_, Ts) =>
+ if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
+ T then
+ accum
+ else
+ T :: accum
+ |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
+ binarize T of
+ [] => Ts
+ | xs => map snd xs)
+ | _ => insert (op =) T accum
+ in aux end
-(* hol_context -> typ -> typ list *)
-fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
+(* hol_context -> bool -> typ -> typ list *)
+fun ground_types_in_type hol_ctxt binarize T =
+ add_ground_types hol_ctxt binarize T []
(* hol_context -> term list -> typ list *)
-fun ground_types_in_terms hol_ctxt ts =
- fold (fold_types (add_ground_types hol_ctxt)) ts []
+fun ground_types_in_terms hol_ctxt binarize ts =
+ fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
(* theory -> const_table -> styp -> int list *)
fun const_format thy def_table (x as (s, T)) =
@@ -2082,7 +2105,7 @@
(* int list -> int list -> typ -> typ *)
fun format_type default_format format T =
let
- val T = unbit_and_unbox_type T
+ val T = unarize_and_unbox_type T
val format = format |> filter (curry (op <) 0)
in
if forall (curry (op =) 1) format then
@@ -2121,7 +2144,7 @@
(* term -> term *)
val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
val (x' as (_, T'), js, ts) =
- AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
+ AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
|> the_single
val max_j = List.last js
val Ts = List.take (binder_types T', max_j + 1)
@@ -2211,7 +2234,7 @@
let val t = Const (original_name s, T) in
(t, format_term_type thy def_table formats t)
end)
- |>> map_types unbit_and_unbox_type
+ |>> map_types unarize_and_unbox_type
|>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 20:46:50 2010 +0100
@@ -33,7 +33,7 @@
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- hol_context -> int -> int Typtab.table -> kodkod_constrs
+ hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
@@ -742,12 +742,14 @@
(* nut NameTable.table -> styp -> KK.rel_expr *)
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> styp -> int -> nfa_transition list *)
-fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
- rel_table (dtypes : dtype_spec list) constr_x n =
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> styp -> int -> nfa_transition list *)
+fun nfa_transitions_for_sel hol_ctxt binarize
+ ({kk_project, ...} : kodkod_constrs) rel_table
+ (dtypes : dtype_spec list) constr_x n =
let
- val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
+ val x as (_, T) =
+ binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
val (r, R, arity) = const_triple rel_table x
val type_schema = type_schema_of_rep T R
in
@@ -756,19 +758,21 @@
else SOME (kk_project r (map KK.Num [0, j]), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> styp -> nfa_transition list *)
-fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
- maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> styp -> nfa_transition list *)
+fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
+ (x as (_, T)) =
+ maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> dtype_spec -> nfa_entry option *)
-fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
- | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
- SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
- o #const) constrs)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> dtype_spec -> nfa_entry option *)
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
+ | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
+ {typ, constrs, ...} =
+ SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
+ dtypes o #const) constrs)
val empty_rel = KK.Product (KK.None, KK.None)
@@ -825,23 +829,25 @@
fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> KK.formula list *)
-fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
- map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> KK.formula list *)
+fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
+ map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
+ dtypes
|> strongly_connected_sub_nfas
|> maps (fn nfa =>
map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
-(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
- -> constr_spec -> int -> KK.formula *)
-fun sel_axiom_for_sel hol_ctxt j0
+(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
+ -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
+fun sel_axiom_for_sel hol_ctxt binarize j0
(kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
kk_join, ...}) rel_table dom_r
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
n =
let
- val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
+ val x as (_, T) =
+ binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
val (r, R, arity) = const_triple rel_table x
val R2 = dest_Func R |> snd
val z = (epsilon - delta, delta + j0)
@@ -855,9 +861,9 @@
(kk_n_ary_function kk R2 r') (kk_no r'))
end
end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
-> constr_spec -> KK.formula list *)
-fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
val honors_explicit_max =
@@ -879,19 +885,19 @@
" too small for \"max\"")
in
max_axiom ::
- map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
+ map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> KK.formula list *)
-fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
- maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
+ maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
-> KK.formula list *)
-fun uniqueness_axiom_for_constr hol_ctxt
+fun uniqueness_axiom_for_constr hol_ctxt binarize
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
: kodkod_constrs) rel_table ({const, ...} : constr_spec) =
let
@@ -899,9 +905,10 @@
fun conjunct_for_sel r =
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
val num_sels = num_sels_for_constr_type (snd const)
- val triples = map (const_triple rel_table
- o boxed_nth_sel_for_constr hol_ctxt const)
- (~1 upto num_sels - 1)
+ val triples =
+ map (const_triple rel_table
+ o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
+ (~1 upto num_sels - 1)
val j0 = case triples |> hd |> #2 of
Func (Atom (_, j0), _) => j0
| R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
@@ -916,11 +923,11 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
-> KK.formula list *)
-fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
({constrs, ...} : dtype_spec) =
- map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
+ map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
(* constr_spec -> int *)
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
@@ -937,22 +944,24 @@
kk_disjoint_sets kk rs]
end
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec -> KK.formula list *)
-fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
+fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
+ | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
(dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
+ sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> KK.formula list *)
-fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
- acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
- maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
+fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
+ dtypes =
+ acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
+ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+ dtypes
(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut bits ofs
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 20:46:50 2010 +0100
@@ -110,23 +110,23 @@
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
(* term -> term *)
-fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
- unbit_and_unbox_term t1
- | unbit_and_unbox_term (Const (@{const_name PairBox},
- Type ("fun", [T1, Type ("fun", [T2, T3])]))
- $ t1 $ t2) =
- let val Ts = map unbit_and_unbox_type [T1, T2] in
+fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
+ unarize_and_unbox_term t1
+ | unarize_and_unbox_term (Const (@{const_name PairBox},
+ Type ("fun", [T1, Type ("fun", [T2, T3])]))
+ $ t1 $ t2) =
+ let val Ts = map unarize_and_unbox_type [T1, T2] in
Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
- $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
+ $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
end
- | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
- | unbit_and_unbox_term (t1 $ t2) =
- unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
- | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
- | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
- | unbit_and_unbox_term (Bound j) = Bound j
- | unbit_and_unbox_term (Abs (s, T, t')) =
- Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
+ | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
+ | unarize_and_unbox_term (t1 $ t2) =
+ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
+ | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
+ | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
+ | unarize_and_unbox_term (Bound j) = Bound j
+ | unarize_and_unbox_term (Abs (s, T, t')) =
+ Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
(* typ -> typ -> (typ * typ) * (typ * typ) *)
fun factor_out_types (T1 as Type ("*", [T11, T12]))
@@ -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, ...}, card_assigns, bits, datatypes, ofs, ...}
- : scope) sel_names rel_table bounds =
+ ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
+ ofs, ...} : scope) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
(* int list list -> int *)
@@ -356,10 +356,10 @@
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
|> make_plain_fun maybe_opt T1 T2
- |> unbit_and_unbox_term
- |> typecast_fun (unbit_and_unbox_type T')
- (unbit_and_unbox_type T1)
- (unbit_and_unbox_type T2)
+ |> unarize_and_unbox_term
+ |> typecast_fun (unarize_and_unbox_type T')
+ (unarize_and_unbox_type T1)
+ (unarize_and_unbox_type T2)
(* (typ * int) list -> typ -> typ -> int -> term *)
fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
let
@@ -418,8 +418,10 @@
else NONE)
(discr_jsss ~~ constrs) |> the
val arg_Ts = curried_binder_types constr_T
- val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
- (index_seq 0 (length arg_Ts))
+ val sel_xs =
+ map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
+ constr_x)
+ (index_seq 0 (length arg_Ts))
val sel_Rs =
map (fn x => get_first
(fn ConstName (s', T', R) =>
@@ -550,7 +552,7 @@
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
- in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
+ in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
-> nut -> term *)
@@ -618,7 +620,7 @@
nondef_table, user_nondefs, simp_table, psimp_table,
intro_table, ground_thm_table, ersatz_table, skolems,
special_funs, unrolled_preds, wf_cache, constr_cache},
- card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
+ binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
val pool = Unsynchronized.ref []
@@ -638,9 +640,9 @@
ersatz_table = ersatz_table, skolems = skolems,
special_funs = special_funs, unrolled_preds = unrolled_preds,
wf_cache = wf_cache, constr_cache = constr_cache}
- val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
- bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
- ofs = ofs}
+ val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
+ card_assigns = card_assigns, bits = bits,
+ bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
(* bool -> typ -> typ -> rep -> int list list -> term *)
fun term_for_rep unfold =
reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
@@ -677,7 +679,7 @@
val (oper, (t1, T'), T) =
case name of
FreeName (s, T, _) =>
- let val t = Free (s, unbit_and_unbox_type T) in
+ let val t = Free (s, unarize_and_unbox_type T) in
("=", (t, format_term_type thy def_table formats t), T)
end
| ConstName (s, T, _) =>
@@ -699,7 +701,7 @@
(* dtype_spec -> Pretty.T *)
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
Pretty.block (Pretty.breaks
- [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
+ [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
Pretty.enum "," "{" "}"
(map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
(if complete then [] else [Pretty.str unrep]))])
@@ -742,8 +744,8 @@
val free_names =
map (fn x as (s, T) =>
case filter (curry (op =) x
- o pairf nickname_of (unbit_and_unbox_type o type_of))
- free_names of
+ o pairf nickname_of (unarize_and_unbox_type o type_of))
+ free_names of
[name] => name
| [] => FreeName (s, T, Any)
| _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Feb 17 20:46:50 2010 +0100
@@ -11,7 +11,7 @@
type hol_context = Nitpick_HOL.hol_context
val formulas_monotonic :
- hol_context -> typ -> sign -> term list -> term list -> term -> bool
+ hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -36,6 +36,7 @@
type cdata =
{hol_ctxt: hol_context,
+ binarize: bool,
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
@@ -114,10 +115,10 @@
| flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
| flatten_ctype C = [C]
-(* hol_context -> typ -> cdata *)
-fun initial_cdata hol_ctxt alpha_T =
- ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
- datatype_cache = Unsynchronized.ref [],
+(* hol_context -> bool -> typ -> cdata *)
+fun initial_cdata hol_ctxt binarize alpha_T =
+ ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
+ max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []} : cdata)
(* typ -> typ -> bool *)
@@ -278,9 +279,9 @@
AList.lookup (op =) (!constr_cache) x |> the)
else
fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
- x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
- |> sel_ctype_from_constr_ctype s
+fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
+ x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
+ |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
(* literal list -> ctype -> ctype *)
fun instantiate_ctype lits =
@@ -945,13 +946,14 @@
map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
|> cat_lines |> print_g
-(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
- core_t =
+(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
+ -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
+ nondef_ts core_t =
let
val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
- val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
+ val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
val (gamma, cset) =
(initial_gamma, slack)
|> fold (consider_definitional_axiom cdata) def_ts
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 20:46:50 2010 +0100
@@ -747,10 +747,10 @@
(* scope -> styp -> int -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
- (vs, table) =
+fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
+ (x as (_, T)) n (vs, table) =
let
- val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
+ val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
val R' = if n = ~1 orelse is_word_type (body_type T) orelse
(is_fun_type (range_type T') andalso
is_boolean_type (body_type T')) then
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Feb 17 20:46:50 2010 +0100
@@ -9,7 +9,8 @@
sig
type hol_context = Nitpick_HOL.hol_context
val preprocess_term :
- hol_context -> term -> ((term list * term list) * (bool * bool)) * term
+ hol_context -> term
+ -> ((term list * term list) * (bool * bool)) * term * bool
end
structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -54,15 +55,6 @@
| should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
| should_use_binary_ints _ = false
-(* typ -> typ *)
-fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
- | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
- | binarize_nat_and_int_in_type (Type (s, Ts)) =
- Type (s, map binarize_nat_and_int_in_type Ts)
- | binarize_nat_and_int_in_type T = T
-(* term -> term *)
-val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
-
(** Uncurrying **)
(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
@@ -1383,7 +1375,8 @@
(** Preprocessor entry point **)
-(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
+(* 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 =
let
@@ -1424,7 +1417,7 @@
in
(((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
(got_all_mono_user_axioms, no_poly_user_axioms)),
- do_rest false true core_t)
+ do_rest false true core_t, binarize)
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 20:46:50 2010 +0100
@@ -30,6 +30,7 @@
type scope = {
hol_ctxt: hol_context,
+ binarize: bool,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -48,7 +49,7 @@
val scopes_equivalent : scope -> scope -> bool
val scope_less_eq : scope -> scope -> bool
val all_scopes :
- hol_context -> int -> (typ option * int list) list
+ hol_context -> bool -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
-> int list -> int list -> typ list -> typ list -> typ list
-> int * scope list
@@ -80,6 +81,7 @@
type scope = {
hol_ctxt: hol_context,
+ binarize: bool,
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
@@ -242,9 +244,10 @@
val max_bits = 31 (* Kodkod limit *)
-(* hol_context -> (typ option * int list) list -> (styp option * int list) list
- -> (styp option * int list) list -> int list -> int list -> typ -> block *)
-fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
+(* hol_context -> bool -> (typ option * int list) list
+ -> (styp option * int list) list -> (styp option * int list) list -> int list
+ -> int list -> typ -> block *)
+fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths T =
if T = @{typ unsigned_bit} then
[(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
@@ -262,18 +265,18 @@
(const_for_iterator_type T)))]
else
(Card T, lookup_type_ints_assign thy cards_assigns T) ::
- (case datatype_constrs hol_ctxt T of
+ (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
-(* hol_context -> (typ option * int list) list -> (styp option * int list) list
- -> (styp option * int list) list -> int list -> int list -> typ list
- -> typ list -> block list *)
-fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
- bisim_depths mono_Ts nonmono_Ts =
+(* hol_context -> bool -> (typ option * int list) list
+ -> (styp option * int list) list -> (styp option * int list) list -> int list
+ -> int list -> typ list -> typ list -> block list *)
+fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
+ bitss bisim_depths mono_Ts nonmono_Ts =
let
(* typ -> block *)
- val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
+ val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
@@ -314,10 +317,10 @@
type scope_desc = (typ * int) list * (styp * int) list
-(* hol_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
- (T, k) =
- case datatype_constrs hol_ctxt T of
+(* hol_context -> bool -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign hol_ctxt binarize
+ (card_assigns, max_assigns) (T, k) =
+ case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
[] => false
| xs =>
let
@@ -330,21 +333,22 @@
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
-(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
- -> bool *)
-fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
- exists (is_surely_inconsistent_card_assign hol_ctxt
+(* hol_context -> bool -> (typ * int) list -> (typ * int) list
+ -> (styp * int) list -> bool *)
+fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
+ max_assigns =
+ exists (is_surely_inconsistent_card_assign hol_ctxt binarize
(seen @ rest, max_assigns)) seen
-(* hol_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
+(* hol_context -> bool -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux seen ((T, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
- (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
- rest max_assigns then
+ (if is_surely_inconsistent_scope_description hol_ctxt binarize
+ ((T, k) :: seen) rest max_assigns then
raise SAME ()
else
case aux ((T, k) :: seen) rest of
@@ -375,13 +379,14 @@
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* hol_context -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
+(* hol_context -> bool -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks
+ columns =
let
val (card_assigns, max_assigns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
- |> the
+ val card_assigns =
+ repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the
in
SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
max_assigns)
@@ -462,14 +467,14 @@
card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
end
-(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
- (desc as (card_assigns, _)) (T, card) =
+(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) 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 xs = boxed_datatype_constrs hol_ctxt 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
@@ -496,21 +501,21 @@
min_bits_for_nat_value (fold Integer.max
(map snd card_assigns @ map snd max_assigns) 0)
-(* hol_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
- (desc as (card_assigns, _)) =
+(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
+ deep_dataTs (desc as (card_assigns, _)) =
let
val datatypes =
- map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
- (filter (is_datatype thy o fst) card_assigns)
+ map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
+ desc) (filter (is_datatype thy 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}
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
- {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
- bits = bits, bisim_depth = bisim_depth,
+ {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
+ datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
else offset_table_for_card_assigns thy card_assigns datatypes}
end
@@ -520,7 +525,7 @@
fun repair_cards_assigns_wrt_boxing _ _ [] = []
| repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
(if is_fun_type T orelse is_pair_type T then
- Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
+ Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
|> map (rpair ks o SOME)
else
[(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
@@ -530,26 +535,29 @@
val max_scopes = 4096
val distinct_threshold = 512
-(* hol_context -> int -> (typ option * int list) list
+(* hol_context -> bool -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
- iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
+fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
+ maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
+ deep_dataTs =
let
val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
cards_assigns
- val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
+ val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths mono_Ts
nonmono_Ts
val ranks = map rank_of_block blocks
val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
val head = take max_scopes all
- val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
- head
+ val descs =
+ map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks)
+ head
in
(length all - length head,
descs |> length descs <= distinct_threshold ? distinct (op =)
- |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
+ |> map (scope_from_descriptor hol_ctxt binarize sym_break
+ deep_dataTs))
end
end;