--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
@@ -378,7 +378,7 @@
". " ^ extra))
end
fun is_type_fundamentally_monotonic T =
- (is_datatype ctxt T andalso not (is_quot_type ctxt T) andalso
+ (is_data_type ctxt T andalso not (is_quot_type ctxt T) andalso
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type ctxt T orelse is_bit_type T
fun is_type_actually_monotonic T =
@@ -395,15 +395,15 @@
SOME (SOME b) => b
| _ => is_type_fundamentally_monotonic T orelse
is_type_actually_monotonic T
- fun is_deep_datatype_finitizable T =
+ fun is_deep_data_type_finitizable T =
triple_lookup (type_match thy) finitizes T = SOME (SOME true)
- fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
+ fun is_shallow_data_type_finitizable (T as Type (@{type_name fun_box}, _)) =
is_type_kind_of_monotonic T
- | is_shallow_datatype_finitizable T =
+ | is_shallow_data_type_finitizable T =
case triple_lookup (type_match thy) finitizes T of
SOME (SOME b) => b
| _ => is_type_kind_of_monotonic T
- fun is_datatype_deep T =
+ fun is_data_type_deep T =
T = @{typ unit} 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 (nondef_ts @ def_ts)
@@ -438,13 +438,13 @@
else
()
val (deep_dataTs, shallow_dataTs) =
- all_Ts |> filter (is_datatype ctxt)
- |> List.partition is_datatype_deep
+ all_Ts |> filter (is_data_type ctxt)
+ |> List.partition is_data_type_deep
val finitizable_dataTs =
(deep_dataTs |> filter_out (is_finite_type hol_ctxt)
- |> filter is_deep_datatype_finitizable) @
+ |> filter is_deep_data_type_finitizable) @
(shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
- |> filter is_shallow_datatype_finitizable)
+ |> filter is_shallow_data_type_finitizable)
val _ =
if verbose andalso not (null finitizable_dataTs) then
pprint_v (K (monotonicity_message finitizable_dataTs
@@ -484,7 +484,7 @@
val too_big_scopes = Unsynchronized.ref []
fun problem_for_scope unsound
- (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
+ (scope as {card_assigns, bits, bisim_depth, data_types, ofs, ...}) =
let
val _ = not (exists (fn other => scope_less_eq other scope)
(!too_big_scopes)) orelse
@@ -500,7 +500,7 @@
val effective_total_consts =
case total_consts of
SOME b => b
- | NONE => forall (is_exact_type datatypes true) all_Ts
+ | NONE => forall (is_exact_type data_types true) all_Ts
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
@@ -569,12 +569,13 @@
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val need_vals =
map (fn dtype as {typ, ...} =>
- (typ, needed_values_for_datatype need_us ofs dtype)) datatypes
+ (typ, needed_values_for_data_type need_us ofs dtype))
+ data_types
val sel_bounds =
- map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels
+ map (bound_for_sel_rel ctxt debug need_vals data_types) sel_rels
val dtype_axioms =
- declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
- datatype_sym_break bits ofs kk rel_table datatypes
+ declarative_axioms_for_data_types hol_ctxt binarize need_us need_vals
+ datatype_sym_break bits ofs kk rel_table data_types
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = Int.max (univ_card nat_card int_card main_j0
(plain_bounds @ sel_bounds) formula,
@@ -607,7 +608,7 @@
problem_for_scope unsound
{hol_ctxt = hol_ctxt, binarize = binarize,
card_assigns = card_assigns, bits = bits,
- bisim_depth = bisim_depth, datatypes = datatypes,
+ bisim_depth = bisim_depth, data_types = data_types,
ofs = Typtab.empty}
else if loc = "Nitpick.pick_them_nits_in_term.\
\problem_for_scope" then
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 22:33:22 2014 +0100
@@ -115,7 +115,7 @@
val is_quot_type : Proof.context -> typ -> bool
val is_pure_typedef : Proof.context -> typ -> bool
val is_univ_typedef : Proof.context -> typ -> bool
- val is_datatype : Proof.context -> typ -> bool
+ val is_data_type : Proof.context -> typ -> bool
val is_record_constr : string * typ -> bool
val is_record_get : theory -> string * typ -> bool
val is_record_update : theory -> string * typ -> bool
@@ -160,10 +160,10 @@
val unregister_codatatype :
typ -> morphism -> Context.generic -> Context.generic
val unregister_codatatype_global : typ -> theory -> theory
- val datatype_constrs : hol_context -> typ -> (string * typ) list
- val binarized_and_boxed_datatype_constrs :
+ val data_type_constrs : hol_context -> typ -> (string * typ) list
+ val binarized_and_boxed_data_type_constrs :
hol_context -> bool -> typ -> (string * typ) list
- val num_datatype_constrs : hol_context -> typ -> int
+ val num_data_type_constrs : hol_context -> typ -> int
val constr_name_for_sel_like : string -> string
val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
string * typ -> string * typ
@@ -613,9 +613,7 @@
val is_raw_typedef = is_some oo typedef_info
val is_raw_old_datatype = is_some oo Datatype.get_info
-(* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
- e.g., by adding a field to "Datatype_Aux.info". *)
-val is_basic_datatype =
+val is_interpreted_type =
member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
@{type_name nat}, @{type_name int}, @{type_name natural},
@{type_name integer}]
@@ -665,7 +663,7 @@
val (co_s, coTs) = dest_Type coT
val _ =
if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
- co_s <> @{type_name fun} andalso not (is_basic_datatype co_s) then
+ co_s <> @{type_name fun} andalso not (is_interpreted_type co_s) then
()
else
raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
@@ -744,11 +742,11 @@
| NONE => false)
| is_univ_typedef _ _ = false
-fun is_datatype ctxt (T as Type (s, _)) =
+fun is_data_type ctxt (T as Type (s, _)) =
(is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse
T = @{typ ind} orelse is_raw_quot_type ctxt T) andalso
- not (is_basic_datatype s)
- | is_datatype _ _ = false
+ not (is_interpreted_type s)
+ | is_data_type _ _ = false
fun all_record_fields thy T =
let val (recs, more) = Record.get_extT_fields thy T in
@@ -891,7 +889,7 @@
fun is_constr ctxt (x as (_, T)) =
is_nonfree_constr ctxt x andalso
- not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
+ not (is_interpreted_type (fst (dest_Type (unarize_type (body_type T))))) andalso
not (is_stale_constr ctxt x)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -1000,8 +998,8 @@
fun zero_const T = Const (@{const_name zero_class.zero}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-fun uncached_datatype_constrs ({thy, ctxt, ...} : hol_context)
- (T as Type (s, Ts)) =
+fun uncached_data_type_constrs ({thy, ctxt, ...} : hol_context)
+ (T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
@@ -1017,7 +1015,7 @@
[(Abs_name,
varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
| NONE => [] (* impossible *)
- else if is_datatype ctxt T then
+ else if is_data_type ctxt T then
case Datatype.get_info thy s of
SOME {index, descr, ...} =>
let
@@ -1047,20 +1045,20 @@
[]
else
[]))
- | uncached_datatype_constrs _ _ = []
+ | uncached_data_type_constrs _ _ = []
-fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
+fun data_type_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 hol_ctxt T in
+ let val xs = uncached_data_type_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
-fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
+fun binarized_and_boxed_data_type_constrs hol_ctxt binarize =
map (apsnd ((binarize ? binarize_nat_and_int_in_type)
- o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
-val num_datatype_constrs = length oo datatype_constrs
+ o box_type hol_ctxt InConstr)) o data_type_constrs hol_ctxt
+val num_data_type_constrs = length oo data_type_constrs
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
@@ -1069,7 +1067,7 @@
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 =)
- (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
+ (binarized_and_boxed_data_type_constrs hol_ctxt binarize (domain_type T'))
s
|> the |> pair s
end
@@ -1146,7 +1144,7 @@
| @{typ prop} => 2
| @{typ bool} => 2
| Type _ =>
- (case datatype_constrs hol_ctxt T of
+ (case data_type_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
else raise SAME ()
| constrs =>
@@ -1243,7 +1241,7 @@
if s = @{const_name Suc} then
Abs (Name.uu, dataT,
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
- else if num_datatype_constrs hol_ctxt dataT >= 2 then
+ else if num_data_type_constrs hol_ctxt dataT >= 2 then
Const (discr_for_constr x)
else
Abs (Name.uu, dataT, @{const True})
@@ -1317,7 +1315,7 @@
(@{const_name Pair}, T1 --> T2 --> T)
end
else
- datatype_constrs hol_ctxt T |> hd
+ data_type_constrs hol_ctxt T |> hd
val arg_Ts = binder_types T'
in
list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t)
@@ -1383,7 +1381,6 @@
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
-(* FIXME: detect "rep_datatype"? *)
fun is_funky_typedef_name ctxt s =
member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
@{type_name Sum_Type.sum}, @{type_name int}] s orelse
@@ -1529,7 +1526,7 @@
fun case_const_names ctxt =
let val thy = Proof_Context.theory_of ctxt in
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
- if is_basic_datatype dtype_s then
+ if is_interpreted_type dtype_s then
I
else
cons (case_name, AList.lookup (op =) descr index
@@ -1668,7 +1665,7 @@
fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
let
- val xs = datatype_constrs hol_ctxt dataT
+ val xs = data_type_constrs hol_ctxt dataT
val cases =
func_ts ~~ xs
|> map (fn (func_t, x) =>
@@ -1695,7 +1692,7 @@
|> absdummy dataT
fun optimized_record_get (hol_ctxt as {thy, ctxt, ...}) s rec_T res_T t =
- let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
+ let val constr_x = hd (data_type_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
~1 => (case rec_T of
Type (_, Ts as _ :: _) =>
@@ -1714,7 +1711,7 @@
fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
rec_t =
let
- val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
+ val constr_x as (_, constr_T) = hd (data_type_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
@@ -1858,7 +1855,7 @@
else if is_quot_abs_fun ctxt x then
case T of
Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
- if is_basic_datatype abs_s then
+ if is_interpreted_type abs_s then
raise NOT_SUPPORTED ("abstraction function on " ^
quote abs_s)
else
@@ -1869,7 +1866,7 @@
else if is_quot_rep_fun ctxt x then
case T of
Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
- if is_basic_datatype abs_s then
+ if is_interpreted_type abs_s then
raise NOT_SUPPORTED ("representation function on " ^
quote abs_s)
else
@@ -2109,7 +2106,7 @@
fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T =
let
- val xs = datatype_constrs hol_ctxt T
+ val xs = data_type_constrs hol_ctxt T
val pred_T = T --> bool_T
val iter_T = @{typ bisim_iterator}
val bisim_max = @{const bisim_iterator_max}
@@ -2495,8 +2492,8 @@
accum
else
T :: accum
- |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
- binarize T of
+ |> fold aux (case binarized_and_boxed_data_type_constrs hol_ctxt
+ binarize T of
[] => Ts
| xs => map snd xs)
| _ => insert (op =) T accum
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Mar 03 22:33:22 2014 +0100
@@ -8,7 +8,7 @@
signature NITPICK_KODKOD =
sig
type hol_context = Nitpick_HOL.hol_context
- type datatype_spec = Nitpick_Scope.datatype_spec
+ type data_type_spec = Nitpick_Scope.data_type_spec
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
type nut = Nitpick_Nut.nut
@@ -28,17 +28,17 @@
val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
val bound_for_sel_rel :
Proof.context -> bool -> (typ * (nut * int) list option) list
- -> datatype_spec list -> nut -> Kodkod.bound
+ -> data_type_spec list -> nut -> Kodkod.bound
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val kodkod_formula_from_nut :
int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
- val needed_values_for_datatype :
- nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option
+ val needed_values_for_data_type :
+ nut list -> int Typtab.table -> data_type_spec -> (nut * int) list option
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
- val declarative_axioms_for_datatypes :
+ val declarative_axioms_for_data_types :
hol_context -> bool -> nut list -> (typ * (nut * int) list option) list
-> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
- -> datatype_spec list -> Kodkod.formula list
+ -> data_type_spec list -> Kodkod.formula list
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -55,8 +55,8 @@
fun pull x xs = x :: filter_out (curry (op =) x) xs
-fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
- | is_datatype_acyclic _ = false
+fun is_data_type_acyclic ({co = false, deep = true, ...} : data_type_spec) = true
+ | is_data_type_acyclic _ = false
fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
@@ -317,7 +317,7 @@
| bound_for_plain_rel _ _ u =
raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
-fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
+fun is_data_type_nat_like ({typ, constrs, ...} : data_type_spec) =
case constrs of
[_, _] =>
(case constrs |> map (snd o #const) |> List.partition is_fun_type of
@@ -328,7 +328,7 @@
fun needed_values need_vals T =
AList.lookup (op =) need_vals T |> the_default NONE |> these
-fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) =
+fun all_values_are_needed need_vals ({typ, card, ...} : data_type_spec) =
length (needed_values need_vals typ) = card
fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) =
@@ -342,7 +342,7 @@
val constr_s = original_name nick
val {delta, epsilon, exclusive, explicit_max, ...} =
constr_spec dtypes (constr_s, T1)
- val dtype as {card, ...} = datatype_spec dtypes T1 |> the
+ val dtype as {card, ...} = data_type_spec dtypes T1 |> the
val T1_need_vals = needed_values need_vals T1
in
([(x, bound_comment ctxt debug nick T R)],
@@ -352,7 +352,7 @@
val (my_need_vals, other_need_vals) =
T1_need_vals |> List.partition (is_sel_of_constr x)
fun atom_seq_for_self_rec j =
- if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0)
+ if is_data_type_nat_like dtype then (1, j + j0 - 1) else (j, j0)
fun exact_bound_for_perhaps_needy_atom j =
case AList.find (op =) my_need_vals j of
[constr_u] =>
@@ -408,7 +408,7 @@
else
[bound_tuples false,
if T1 = T2 andalso epsilon > delta andalso
- is_datatype_acyclic dtype then
+ is_data_type_acyclic dtype then
index_seq delta (epsilon - delta)
|> map (fn j => tuple_product (KK.TupleSet [KK.Tuple [j + j0]])
(KK.TupleAtomSeq (atom_seq_for_self_rec j)))
@@ -1502,7 +1502,7 @@
fun nfa_transitions_for_sel hol_ctxt binarize
({kk_project, ...} : kodkod_constrs) rel_table
- (dtypes : datatype_spec list) constr_x n =
+ (dtypes : data_type_spec list) constr_x n =
let
val x as (_, T) =
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
@@ -1520,10 +1520,10 @@
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
- {typ, constrs, ...} =
+fun nfa_entry_for_data_type _ _ _ _ _ ({co = true, ...} : data_type_spec) = NONE
+ | nfa_entry_for_data_type _ _ _ _ _ {deep = false, ...} = NONE
+ | nfa_entry_for_data_type 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)
@@ -1566,17 +1566,17 @@
|> Typ_Graph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
+(* Cycle breaking in the bounds takes care of singly recursive data types, hence
the first equation. *)
-fun acyclicity_axioms_for_datatype _ [_] _ = []
- | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
- start_T =
+fun acyclicity_axioms_for_data_type _ [_] _ = []
+ | acyclicity_axioms_for_data_type (kk as {kk_no, kk_intersect, ...}) nfa
+ start_T =
[kk_no (kk_intersect
(loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
KK.Iden)]
-fun acyclicity_axioms_for_datatypes kk =
- maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
+fun acyclicity_axioms_for_data_types kk =
+ maps (fn nfa => maps (acyclicity_axioms_for_data_type kk nfa o fst) nfa)
fun atom_equation_for_nut ofs kk (u, j) =
let val dummy_u = RelReg (0, type_of u, rep_of u) in
@@ -1587,9 +1587,9 @@
"malformed Kodkod formula")
end
-fun needed_values_for_datatype [] _ _ = SOME []
- | needed_values_for_datatype need_us ofs
- ({typ, card, constrs, ...} : datatype_spec) =
+fun needed_values_for_data_type [] _ _ = SOME []
+ | needed_values_for_data_type need_us ofs
+ ({typ, card, constrs, ...} : data_type_spec) =
let
fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
fold aux us
@@ -1620,9 +1620,9 @@
SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
end
-fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False]
- | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) =
- if is_datatype_nat_like (the (datatype_spec dtypes T)) then []
+fun needed_value_axioms_for_data_type _ _ _ (_, NONE) = [KK.False]
+ | needed_value_axioms_for_data_type ofs kk dtypes (T, SOME fixed) =
+ if is_data_type_nat_like (the (data_type_spec dtypes T)) then []
else fixed |> map_filter (atom_equation_for_nut ofs kk)
fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
@@ -1637,19 +1637,19 @@
prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
o pairself constr_quadruple
-fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
- {card = card2, self_rec = self_rec2, constrs = constr2, ...})
- : datatype_spec * datatype_spec) =
+fun data_type_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
+ {card = card2, self_rec = self_rec2, constrs = constr2, ...})
+ : data_type_spec * data_type_spec) =
prod_ord int_ord (prod_ord bool_ord int_ord)
((card1, (self_rec1, length constr1)),
(card2, (self_rec2, length constr2)))
-(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
+(* We must absolutely tabulate "suc" for all data types whose selector bounds
break cycles; otherwise, we may end up with two incompatible symmetry
breaking orders, leading to spurious models. *)
fun should_tabulate_suc_for_type dtypes T =
- is_asymmetric_nondatatype T orelse
- case datatype_spec dtypes T of
+ is_asymmetric_non_data_type T orelse
+ case data_type_spec dtypes T of
SOME {self_rec, ...} => self_rec
| NONE => false
@@ -1673,7 +1673,7 @@
| _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
fun is_nil_like_constr_type dtypes T =
- case datatype_spec dtypes T of
+ case data_type_spec dtypes T of
SOME {constrs, ...} =>
(case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
[{const = (_, T'), ...}] => T = T'
@@ -1752,8 +1752,8 @@
end
end
-fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
- ({constrs, ...} : datatype_spec) =
+fun sym_break_axioms_for_data_type hol_ctxt binarize kk rel_table nfas dtypes
+ ({constrs, ...} : data_type_spec) =
let
val constrs = sort constr_ord constrs
val constr_pairs = all_distinct_unordered_pairs_of constrs
@@ -1765,18 +1765,18 @@
nfas dtypes)
end
-fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
- T = T' orelse exists (is_datatype_in_needed_value T) us
- | is_datatype_in_needed_value _ _ = false
+fun is_data_type_in_needed_value T (Construct (_, T', _, us)) =
+ T = T' orelse exists (is_data_type_in_needed_value T) us
+ | is_data_type_in_needed_value _ _ = false
val min_sym_break_card = 7
-fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
- kk rel_table nfas dtypes =
+fun sym_break_axioms_for_data_types hol_ctxt binarize need_us
+ datatype_sym_break kk rel_table nfas dtypes =
if datatype_sym_break = 0 then
[]
else
- dtypes |> filter is_datatype_acyclic
+ dtypes |> filter is_data_type_acyclic
|> filter (fn {constrs = [_], ...} => false
| {card, constrs, ...} =>
card >= min_sym_break_card andalso
@@ -1784,13 +1784,13 @@
o binder_types o snd o #const) constrs)
|> filter_out
(fn {typ, ...} =>
- exists (is_datatype_in_needed_value typ) need_us)
+ exists (is_data_type_in_needed_value typ) need_us)
|> (fn dtypes' =>
dtypes' |> length dtypes' > datatype_sym_break
- ? (sort (datatype_ord o swap)
+ ? (sort (data_type_ord o swap)
#> take datatype_sym_break))
- |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
- nfas dtypes)
+ |> maps (sym_break_axioms_for_data_type hol_ctxt binarize kk rel_table
+ nfas dtypes)
fun sel_axioms_for_sel hol_ctxt binarize j0
(kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
@@ -1849,8 +1849,8 @@
end
end
-fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
- (dtype as {constrs, ...}) =
+fun sel_axioms_for_data_type hol_ctxt binarize bits j0 kk rel_table need_vals
+ (dtype as {constrs, ...}) =
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
dtype) constrs
@@ -1879,14 +1879,14 @@
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
end
-fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
- (dtype as {constrs, ...}) =
+fun uniqueness_axioms_for_data_type hol_ctxt binarize kk need_vals rel_table
+ (dtype as {constrs, ...}) =
maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
dtype) constrs
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
-fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
+fun partition_axioms_for_data_type j0 (kk as {kk_rel_eq, kk_union, ...})
need_vals rel_table (dtype as {card, constrs, ...}) =
if forall #exclusive constrs then
[Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
@@ -1898,31 +1898,31 @@
kk_disjoint_sets kk rs]
end
-fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table
- (dtype as {typ, ...}) =
+fun other_axioms_for_data_type _ _ _ _ _ _ _ {deep = false, ...} = []
+ | other_axioms_for_data_type hol_ctxt binarize need_vals bits ofs kk rel_table
+ (dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table
- dtype @
- uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
- dtype @
- partition_axioms_for_datatype j0 kk need_vals rel_table dtype
+ sel_axioms_for_data_type hol_ctxt binarize bits j0 kk need_vals rel_table
+ dtype @
+ uniqueness_axioms_for_data_type hol_ctxt binarize kk need_vals rel_table
+ dtype @
+ partition_axioms_for_data_type j0 kk need_vals rel_table dtype
end
-fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
+fun declarative_axioms_for_data_types hol_ctxt binarize need_us need_vals
datatype_sym_break bits ofs kk rel_table dtypes =
let
val nfas =
- dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
- rel_table dtypes)
+ dtypes |> map_filter (nfa_entry_for_data_type hol_ctxt binarize kk
+ rel_table dtypes)
|> strongly_connected_sub_nfas
in
- acyclicity_axioms_for_datatypes kk nfas @
- maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @
- sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
- kk rel_table nfas dtypes @
- maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk
- rel_table) dtypes
+ acyclicity_axioms_for_data_types kk nfas @
+ maps (needed_value_axioms_for_data_type ofs kk dtypes) need_vals @
+ sym_break_axioms_for_data_types hol_ctxt binarize need_us datatype_sym_break
+ kk rel_table nfas dtypes @
+ maps (other_axioms_for_data_type hol_ctxt binarize need_vals bits ofs kk
+ rel_table) dtypes
end
end;
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Mar 03 22:33:22 2014 +0100
@@ -367,7 +367,7 @@
and reconstruct_term maybe_opt unfold pool
(wacky_names as ((maybe_name, abs_name), _))
(scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
- datatypes, ofs, ...})
+ data_types, ofs, ...})
atomss sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
@@ -403,7 +403,7 @@
val empty_const = Const (@{const_abbrev Set.empty}, set_T)
val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
fun aux [] =
- if maybe_opt andalso not (is_complete_type datatypes false T) then
+ if maybe_opt andalso not (is_complete_type data_types false T) then
insert_const $ Const (unrep (), T) $ empty_const
else
empty_const
@@ -432,7 +432,7 @@
Const (@{const_name None}, _) => aux' tps
| _ => update_const $ aux' tps $ t1 $ t2)
fun aux tps =
- if maybe_opt andalso not (is_complete_type datatypes false T1) then
+ if maybe_opt andalso not (is_complete_type data_types false T1) then
update_const $ aux' tps $ Const (unrep (), T1)
$ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
else
@@ -463,7 +463,7 @@
| Const (s, Type (@{type_name fun}, [T1, T2])) =>
if s = opt_flag orelse s = non_opt_flag then
Abs ("x", T1,
- Const (if is_complete_type datatypes false T1 then
+ Const (if is_complete_type data_types false T1 then
irrelevant
else
unknown, T2))
@@ -525,7 +525,7 @@
HOLogic.mk_number nat_T (k - j - 1)
else if T = @{typ bisim_iterator} then
HOLogic.mk_number nat_T j
- else case datatype_spec datatypes T of
+ else case data_type_spec data_types T of
NONE => nth_atom thy atomss pool for_auto T j
| SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
| SOME {co, constrs, ...} =>
@@ -888,7 +888,7 @@
simp_table, psimp_table, choice_spec_table, intro_table,
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache}, binarize,
- card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
+ card_assigns, bits, bisim_depth, data_types, ofs} : scope)
formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
rel_table bounds =
let
@@ -910,15 +910,16 @@
wf_cache = wf_cache, constr_cache = constr_cache}
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
- bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
+ bits = bits, bisim_depth = bisim_depth, data_types = data_types,
+ ofs = ofs}
fun term_for_rep maybe_opt unfold =
reconstruct_term maybe_opt unfold pool wacky_names scope atomss
sel_names rel_table bounds
val all_values =
all_values_of_type pool wacky_names scope atomss sel_names rel_table
bounds
- fun is_codatatype_wellformed (cos : datatype_spec list)
- ({typ, card, ...} : datatype_spec) =
+ fun is_codatatype_wellformed (cos : data_type_spec list)
+ ({typ, card, ...} : data_type_spec) =
let
val ts = all_values card typ
val max_depth = Integer.sum (map #card cos)
@@ -950,7 +951,7 @@
[Syntax.pretty_term ctxt t1, Pretty.str oper,
Syntax.pretty_term ctxt t2])
end
- fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
+ fun pretty_for_data_type ({typ, card, complete, ...} : data_type_spec) =
Pretty.block (Pretty.breaks
(pretty_for_type ctxt typ ::
(case typ of
@@ -962,24 +963,18 @@
(map (Syntax.pretty_term ctxt) (all_values card typ) @
(if fun_from_pair complete false then []
else [Pretty.str (unrep ())]))]))
- fun integer_datatype T =
+ fun integer_data_type T =
[{typ = T, card = card_of_type card_assigns T, co = false,
self_rec = true, complete = (false, false), concrete = (true, true),
deep = true, constrs = []}]
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)
- val block_of_datatypes =
- if show_types andalso not (null datatypes) then
- [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
- (map pretty_for_datatype datatypes)]
- else
- []
- val block_of_codatatypes =
- if show_types andalso not (null codatatypes) then
- [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
- (map pretty_for_datatype codatatypes)]
+ val data_types =
+ data_types |> filter #deep
+ |> append (maps integer_data_type [nat_T, int_T])
+ val block_of_data_types =
+ if show_types andalso not (null data_types) then
+ [Pretty.big_list ("Type" ^ plural_s_for_list data_types ^ ":")
+ (map pretty_for_data_type data_types)]
else
[]
fun block_of_names show title names =
@@ -1010,9 +1005,10 @@
val chunks = block_of_names true "Free variable" real_free_names @
block_of_names show_skolems "Skolem constant" skolem_names @
block_of_names true "Evaluated term" eval_names @
- block_of_datatypes @ block_of_codatatypes @
+ block_of_data_types @
block_of_names show_consts "Constant"
noneval_nonskolem_nonsel_names
+ val codatatypes = filter #co data_types;
in
(Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
else chunks),
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Mar 03 22:33:22 2014 +0100
@@ -41,7 +41,7 @@
binarize: bool,
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
- datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
+ data_type_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
constr_mcache: ((string * typ) * mtyp) list Unsynchronized.ref}
exception UNSOLVABLE of unit
@@ -123,7 +123,7 @@
fun initial_mdata hol_ctxt binarize alpha_T =
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
- max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
+ max_fresh = Unsynchronized.ref 0, data_type_mcache = Unsynchronized.ref [],
constr_mcache = Unsynchronized.ref []} : mdata)
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -134,7 +134,7 @@
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
| could_exist_alpha_sub_mtype ctxt alpha_T T =
- (T = alpha_T orelse is_datatype ctxt T)
+ (T = alpha_T orelse is_data_type ctxt T)
fun exists_alpha_sub_mtype MAlpha = true
| exists_alpha_sub_mtype (MFun (M1, _, M2)) =
@@ -170,7 +170,7 @@
| M => if member (op =) seen M then MType (s, [])
else repair_mtype cache (M :: seen) M
-fun repair_datatype_mcache cache =
+fun repair_data_type_mcache cache =
let
fun repair_one (z, M) =
Unsynchronized.change cache
@@ -219,7 +219,7 @@
A Gen
in (M1, aa, M2) end
and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
- datatype_mcache, constr_mcache, ...})
+ data_type_mcache, constr_mcache, ...})
all_minus =
let
fun do_type T =
@@ -232,12 +232,12 @@
| Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
| Type (z as (s, _)) =>
if could_exist_alpha_sub_mtype ctxt alpha_T T then
- case AList.lookup (op =) (!datatype_mcache) z of
+ case AList.lookup (op =) (!data_type_mcache) z of
SOME M => M
| NONE =>
let
- val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
- val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
+ val _ = Unsynchronized.change data_type_mcache (cons (z, MRec z))
+ val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
val (all_Ms, constr_Ms) =
fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
let
@@ -252,15 +252,15 @@
end)
xs ([], [])
val M = MType (s, all_Ms)
- val _ = Unsynchronized.change datatype_mcache
+ val _ = Unsynchronized.change data_type_mcache
(AList.update (op =) (z, M))
val _ = Unsynchronized.change constr_mcache
(append (xs ~~ constr_Ms))
in
- if forall (not o is_MRec o snd) (!datatype_mcache) then
- (repair_datatype_mcache datatype_mcache;
- repair_constr_mcache (!datatype_mcache) constr_mcache;
- AList.lookup (op =) (!datatype_mcache) z |> the)
+ if forall (not o is_MRec o snd) (!data_type_mcache) then
+ (repair_data_type_mcache data_type_mcache;
+ repair_constr_mcache (!data_type_mcache) constr_mcache;
+ AList.lookup (op =) (!data_type_mcache) z |> the)
else
M
end
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Mar 03 22:33:22 2014 +0100
@@ -702,12 +702,12 @@
fold_rev (choose_rep_for_nth_sel_for_constr scope x)
(~1 upto num_sels_for_constr_type T - 1)
-fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
- | choose_rep_for_sels_of_datatype scope {constrs, ...} =
+fun choose_rep_for_sels_of_data_type _ ({deep = false, ...} : data_type_spec) = I
+ | choose_rep_for_sels_of_data_type scope {constrs, ...} =
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
-fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
- fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
+fun choose_reps_for_all_sels (scope as {data_types, ...}) =
+ fold (choose_rep_for_sels_of_data_type scope) data_types o pair []
val min_univ_card = 2
@@ -813,7 +813,7 @@
fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
| untuple f u = [f u]
-fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
+fun choose_reps_in_nut (scope as {card_assigns, bits, data_types, ofs, ...})
unsound table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
@@ -924,7 +924,7 @@
if is_opt_rep R then
triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
else if not opt orelse unsound orelse polar = Neg orelse
- is_concrete_type datatypes true (type_of u1) then
+ is_concrete_type data_types true (type_of u1) then
s_op2 Subset T R u1 u2
else
Cst (False, T, Formula Pos)
@@ -947,7 +947,7 @@
else opt_opt_case ()
in
if unsound orelse polar = Neg orelse
- is_concrete_type datatypes true (type_of u1) then
+ is_concrete_type data_types true (type_of u1) then
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
(true, true) => opt_opt_case ()
| (true, false) => hybrid_case u1'
@@ -1002,7 +1002,7 @@
let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
if def orelse
(unsound andalso (polar = Pos) = (oper = All)) orelse
- is_complete_type datatypes true (type_of u1) then
+ is_complete_type data_types true (type_of u1) then
quant_u
else
let
@@ -1072,7 +1072,7 @@
val Rs = map rep_of us
val R = best_one_rep_for_type scope T
val {total, ...} =
- constr_spec datatypes (original_name (nickname_of (hd us')), T)
+ constr_spec data_types (original_name (nickname_of (hd us')), T)
val opt = exists is_opt_rep Rs orelse not total
in Construct (map sub us', T, R |> opt ? Opt, us) end
| _ =>
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Mar 03 22:33:22 2014 +0100
@@ -274,8 +274,8 @@
best_non_opt_set_rep_for_type scope (T' --> bool_T)
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
-fun best_set_rep_for_type (scope as {datatypes, ...}) T =
- (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
+fun best_set_rep_for_type (scope as {data_types, ...}) T =
+ (if is_exact_type data_types true T then best_non_opt_set_rep_for_type
else best_opt_set_rep_for_type) scope T
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Mar 03 22:33:22 2014 +0100
@@ -17,7 +17,7 @@
explicit_max: int,
total: bool}
- type datatype_spec =
+ type data_type_spec =
{typ: typ,
card: int,
co: bool,
@@ -33,15 +33,15 @@
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
- datatypes: datatype_spec list,
+ data_types: data_type_spec list,
ofs: int Typtab.table}
- val is_asymmetric_nondatatype : typ -> bool
- val datatype_spec : datatype_spec list -> typ -> datatype_spec option
- val constr_spec : datatype_spec list -> string * typ -> constr_spec
- val is_complete_type : datatype_spec list -> bool -> typ -> bool
- val is_concrete_type : datatype_spec list -> bool -> typ -> bool
- val is_exact_type : datatype_spec list -> bool -> typ -> bool
+ val is_asymmetric_non_data_type : typ -> bool
+ val data_type_spec : data_type_spec list -> typ -> data_type_spec option
+ val constr_spec : data_type_spec list -> string * typ -> constr_spec
+ val is_complete_type : data_type_spec list -> bool -> typ -> bool
+ val is_concrete_type : data_type_spec list -> bool -> typ -> bool
+ val is_exact_type : data_type_spec list -> bool -> typ -> bool
val offset_of_type : int Typtab.table -> typ -> int
val spec_of_type : scope -> typ -> int * int
val pretties_for_scope : scope -> bool -> Pretty.T list
@@ -70,7 +70,7 @@
explicit_max: int,
total: bool}
-type datatype_spec =
+type data_type_spec =
{typ: typ,
card: int,
co: bool,
@@ -86,7 +86,7 @@
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
- datatypes: datatype_spec list,
+ data_types: data_type_spec list,
ofs: int Typtab.table}
datatype row_kind = Card of typ | Max of string * typ
@@ -94,14 +94,14 @@
type row = row_kind * int list
type block = row list
-val is_asymmetric_nondatatype =
+val is_asymmetric_non_data_type =
is_iterator_type orf is_integer_type orf is_bit_type
-fun datatype_spec (dtypes : datatype_spec list) T =
+fun data_type_spec (dtypes : data_type_spec list) T =
List.find (curry (op =) T o #typ) dtypes
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
- | constr_spec ({constrs, ...} :: dtypes : datatype_spec list) (x as (s, T)) =
+ | constr_spec ({constrs, ...} :: dtypes : data_type_spec list) (x as (s, T)) =
case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
constrs of
SOME c => c
@@ -115,7 +115,7 @@
is_concrete_type dtypes facto T'
| is_complete_type dtypes facto T =
not (is_integer_like_type T) andalso not (is_bit_type T) andalso
- fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
+ fun_from_pair (#complete (the (data_type_spec dtypes T))) facto
handle Option.Option => true
and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
@@ -124,7 +124,7 @@
| is_concrete_type dtypes facto (Type (@{type_name set}, [T'])) =
is_complete_type dtypes facto T'
| is_concrete_type dtypes facto T =
- fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
+ fun_from_pair (#concrete (the (data_type_spec dtypes T))) facto
handle Option.Option => true
and is_exact_type dtypes facto =
is_complete_type dtypes facto andf is_concrete_type dtypes facto
@@ -140,7 +140,7 @@
fun quintuple_for_scope code_type code_term code_string
({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
- datatypes, ...} : scope) =
+ data_types, ...} : scope) =
let
val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@{typ bisim_iterator}]
@@ -149,7 +149,7 @@
|> 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 ctxt) o fst)
+ |> List.partition ((is_integer_type orf is_data_type ctxt) o fst)
val cards =
map (fn (T, k) =>
[code_type ctxt T, code_string (" = " ^ string_of_int k)])
@@ -161,7 +161,7 @@
else
SOME [code_term ctxt (Const const),
code_string (" = " ^ string_of_int explicit_max)])
- o #constrs) datatypes
+ o #constrs) data_types
fun iters () =
map (fn (T, k) =>
[code_term ctxt (Const (const_for_iterator_type T)),
@@ -169,7 +169,7 @@
fun miscs () =
(if bits = 0 then []
else [code_string ("bits = " ^ string_of_int bits)]) @
- (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
+ (if bisim_depth < 0 andalso forall (not o #co) data_types then []
else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
in
(cards primary_card_assigns, cards secondary_card_assigns,
@@ -210,7 +210,7 @@
end
fun scopes_equivalent (s1 : scope, s2 : scope) =
- #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
+ #data_types s1 = #data_types s2 andalso #card_assigns s1 = #card_assigns s2
fun scope_less_eq (s1 : scope) (s2 : scope) =
(s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
@@ -265,7 +265,7 @@
(const_for_iterator_type T)))]
else
(Card T, lookup_type_ints_assign thy cards_assigns T) ::
- (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
+ (case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
@@ -304,7 +304,7 @@
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
+ case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
[] => false
| xs =>
let
@@ -376,9 +376,9 @@
let
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
- if k = 1 orelse is_asymmetric_nondatatype T then
+ if k = 1 orelse is_asymmetric_non_data_type T then
aux next reusable assigns
- else if length (these (Option.map #constrs (datatype_spec dtypes T)))
+ else if length (these (Option.map #constrs (data_type_spec dtypes T)))
> 1 then
Typtab.update_new (T, next) #> aux (next + k) reusable assigns
else
@@ -439,13 +439,13 @@
card_assigns T
end
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
+fun data_type_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
(T, card) =
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype ctxt T
- val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
+ val xs = binarized_and_boxed_data_type_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
@@ -475,10 +475,10 @@
fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) binarize deep_dataTs
finitizable_dataTs (desc as (card_assigns, _)) =
let
- val datatypes =
- map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
- finitizable_dataTs desc)
- (filter (is_datatype ctxt o fst) card_assigns)
+ val data_types =
+ map (data_type_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
+ finitizable_dataTs desc)
+ (filter (is_data_type ctxt 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}
@@ -486,8 +486,8 @@
val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
- datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
- ofs = offset_table_for_card_assigns datatypes card_assigns}
+ data_types = data_types, bits = bits, bisim_depth = bisim_depth,
+ ofs = offset_table_for_card_assigns data_types card_assigns}
end
fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []