# HG changeset patch # User haftmann # Date 1497938516 -7200 # Node ID d0476618a94cf2ed999f31a1b5e417bed541ff3c # Parent 8a3b141179c25b12c97da6c70488309d2a78db1c more consistent terminology diff -r 8a3b141179c2 -r d0476618a94c src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 @@ -176,7 +176,7 @@ | Proj of (term * string) * bool | Abstr of (thm * string) * bool; -val initial_fun_spec = Eqns_Default ([], Lazy.value []); +val default_fun_spec = Eqns_Default ([], Lazy.value []); fun is_default (Eqns_Default _) = true | is_default (Proj (_, default)) = default @@ -202,6 +202,8 @@ fun make_spec (history_concluded, (functions, (types, (cases, undefineds)))) = Spec { history_concluded = history_concluded, functions = functions, types = types, cases = cases, undefineds = undefineds }; +val empty_spec = + make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))); fun map_spec f (Spec { history_concluded = history_concluded, functions = functions, types = types, cases = cases, undefineds = undefineds }) = make_spec (f (history_concluded, (functions, (types, (cases, undefineds))))); @@ -225,7 +227,7 @@ val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2) |> subtract (op =) (maps case_consts_of all_datatype_specs) val functions = Symtab.join (K merge_functions) (functions1, functions2) - |> fold (fn c => Symtab.map_entry c (apfst (K (true, initial_fun_spec)))) all_constructors; + |> fold (fn c => Symtab.map_entry c (apfst (K (true, default_fun_spec)))) all_constructors; val cases = Symtab.merge (K true) (cases1, cases2) |> fold Symtab.delete invalidated_case_consts; val undefineds = Symtab.merge (K true) (undefineds1, undefineds2); @@ -238,7 +240,7 @@ fun undefineds_of (Spec { undefineds, ... }) = undefineds; val map_history_concluded = map_spec o apfst; val map_functions = map_spec o apsnd o apfst; -val map_typs = map_spec o apsnd o apsnd o apfst; +val map_types = map_spec o apsnd o apsnd o apfst; val map_cases = map_spec o apsnd o apsnd o apsnd o apfst; val map_undefineds = map_spec o apsnd o apsnd o apsnd o apsnd; @@ -283,8 +285,7 @@ structure Code_Data = Theory_Data ( type T = spec * (data * theory) option Synchronized.var; - val empty = (make_spec (false, (Symtab.empty, - (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ()); + val empty = (empty_spec, empty_dataref ()); val extend : T -> T = apsnd (K (empty_dataref ())); fun merge ((spec1, _), (spec2, _)) = (merge_spec (spec1, spec2), empty_dataref ()); @@ -297,10 +298,10 @@ val spec_of : theory -> spec = fst o Code_Data.get; -fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ())); +fun map_spec_purge f = Code_Data.map (fn (spec, _) => (f spec, empty_dataref ())); -fun change_fun_spec c f = (map_exec_purge o map_functions - o (Symtab.map_default (c, ((false, initial_fun_spec), []))) +fun change_fun_spec c f = (map_spec_purge o map_functions + o (Symtab.map_default (c, ((false, default_fun_spec), []))) o apfst) (fn (_, spec) => (true, f spec)); @@ -705,7 +706,7 @@ (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; val inst = map2 (fn (v, sort) => fn (_, sort') => (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping; - val subst = (map_types o map_type_tfree) + val subst = (Term.map_types o map_type_tfree) (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); in thm @@ -1015,7 +1016,7 @@ fun print_codesetup thy = let val ctxt = Proof_Context.init_global thy; - val exec = spec_of thy; + val spec = spec_of thy; fun pretty_equations const thms = (Pretty.block o Pretty.fbreaks) (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms); @@ -1047,11 +1048,11 @@ | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [ Pretty.str (string_of_const thy const), Pretty.str "with", (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos]; - val functions = functions_of exec + val functions = functions_of spec |> Symtab.dest |> (map o apsnd) (snd o fst) |> sort (string_ord o apply2 fst); - val datatypes = types_of exec + val datatypes = types_of spec |> Symtab.dest |> map (fn (tyco, (_, (vs, spec)) :: _) => ((tyco, vs), constructors_of spec)) @@ -1105,7 +1106,7 @@ fun update_subsume verbose (thm, proper) eqns = let val args_of = snd o take_prefix is_Var o rev o snd o strip_comb - o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; + o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of; val args = args_of thm; val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1); fun matches_args args' = @@ -1184,7 +1185,7 @@ fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true) of SOME (thm, _) => let - fun del_eqn' (Eqns_Default _) = initial_fun_spec + fun del_eqn' (Eqns_Default _) = default_fun_spec | del_eqn' (Eqns eqns) = let val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns @@ -1236,16 +1237,16 @@ then insert (op =) case_const cases else cases) | register_for_constructors (x as Abstractor _) = x; - val register_type = (map_typs o Symtab.map) + val register_type = (map_types o Symtab.map) (K ((map o apsnd o apsnd) register_for_constructors)); in thy |> `(fn thy => case_cong thy case_const entry) - |-> (fn cong => map_exec_purge (register_case cong #> register_type)) + |-> (fn cong => map_spec_purge (register_case cong #> register_type)) end; fun add_undefined c thy = - (map_exec_purge o map_undefineds) (Symtab.update (c, ())) thy; + (map_spec_purge o map_undefineds) (Symtab.update (c, ())) thy; (* types *) @@ -1272,8 +1273,8 @@ in thy |> fold del_eqns (outdated_funs1 @ outdated_funs2) - |> map_exec_purge - ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec)) + |> map_spec_purge + ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec)) #> map_cases drop_outdated_cases) end;