# HG changeset patch # User blanchet # Date 1393882402 -3600 # Node ID bd7927cca152415469a7e90b004d41fcf6244210 # Parent 6bfbec3dff62ddd8a4b9a6bc2a93a879b560aa10 tuned ML names diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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; diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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), diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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 | _ => diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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, ...}) diff -r 6bfbec3dff62 -r bd7927cca152 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 _ _ [] = []