more consistent terminology
authorhaftmann
Tue Jun 20 08:01:56 2017 +0200 (2017-06-20)
changeset 66130d0476618a94c
parent 66129 8a3b141179c2
child 66131 39e1c876bfec
more consistent terminology
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4    | Proj of (term * string) * bool
     1.5    | Abstr of (thm * string) * bool;
     1.6  
     1.7 -val initial_fun_spec = Eqns_Default ([], Lazy.value []);
     1.8 +val default_fun_spec = Eqns_Default ([], Lazy.value []);
     1.9  
    1.10  fun is_default (Eqns_Default _) = true
    1.11    | is_default (Proj (_, default)) = default
    1.12 @@ -202,6 +202,8 @@
    1.13  fun make_spec (history_concluded, (functions, (types, (cases, undefineds)))) =
    1.14    Spec { history_concluded = history_concluded, functions = functions, types = types,
    1.15      cases = cases, undefineds = undefineds };
    1.16 +val empty_spec =
    1.17 +  make_spec (false, (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty))));
    1.18  fun map_spec f (Spec { history_concluded = history_concluded,
    1.19    functions = functions, types = types, cases = cases, undefineds = undefineds }) =
    1.20    make_spec (f (history_concluded, (functions, (types, (cases, undefineds)))));
    1.21 @@ -225,7 +227,7 @@
    1.22      val invalidated_case_consts = union (op =) (case_consts_of' types1) (case_consts_of' types2)
    1.23        |> subtract (op =) (maps case_consts_of all_datatype_specs)
    1.24      val functions = Symtab.join (K merge_functions) (functions1, functions2)
    1.25 -      |> fold (fn c => Symtab.map_entry c (apfst (K (true, initial_fun_spec)))) all_constructors;
    1.26 +      |> fold (fn c => Symtab.map_entry c (apfst (K (true, default_fun_spec)))) all_constructors;
    1.27      val cases = Symtab.merge (K true) (cases1, cases2)
    1.28        |> fold Symtab.delete invalidated_case_consts;
    1.29      val undefineds = Symtab.merge (K true) (undefineds1, undefineds2);
    1.30 @@ -238,7 +240,7 @@
    1.31  fun undefineds_of (Spec { undefineds, ... }) = undefineds;
    1.32  val map_history_concluded = map_spec o apfst;
    1.33  val map_functions = map_spec o apsnd o apfst;
    1.34 -val map_typs = map_spec o apsnd o apsnd o apfst;
    1.35 +val map_types = map_spec o apsnd o apsnd o apfst;
    1.36  val map_cases = map_spec o apsnd o apsnd o apsnd o apfst;
    1.37  val map_undefineds = map_spec o apsnd o apsnd o apsnd o apsnd;
    1.38  
    1.39 @@ -283,8 +285,7 @@
    1.40  structure Code_Data = Theory_Data
    1.41  (
    1.42    type T = spec * (data * theory) option Synchronized.var;
    1.43 -  val empty = (make_spec (false, (Symtab.empty,
    1.44 -    (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
    1.45 +  val empty = (empty_spec, empty_dataref ());
    1.46    val extend : T -> T = apsnd (K (empty_dataref ()));
    1.47    fun merge ((spec1, _), (spec2, _)) =
    1.48      (merge_spec (spec1, spec2), empty_dataref ());
    1.49 @@ -297,10 +298,10 @@
    1.50  
    1.51  val spec_of : theory -> spec = fst o Code_Data.get;
    1.52  
    1.53 -fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
    1.54 +fun map_spec_purge f = Code_Data.map (fn (spec, _) => (f spec, empty_dataref ()));
    1.55  
    1.56 -fun change_fun_spec c f = (map_exec_purge o map_functions
    1.57 -  o (Symtab.map_default (c, ((false, initial_fun_spec), [])))
    1.58 +fun change_fun_spec c f = (map_spec_purge o map_functions
    1.59 +  o (Symtab.map_default (c, ((false, default_fun_spec), [])))
    1.60      o apfst) (fn (_, spec) => (true, f spec));
    1.61  
    1.62  
    1.63 @@ -705,7 +706,7 @@
    1.64        (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
    1.65      val inst = map2 (fn (v, sort) => fn (_, sort') =>
    1.66        (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
    1.67 -    val subst = (map_types o map_type_tfree)
    1.68 +    val subst = (Term.map_types o map_type_tfree)
    1.69        (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
    1.70    in
    1.71      thm
    1.72 @@ -1015,7 +1016,7 @@
    1.73  fun print_codesetup thy =
    1.74    let
    1.75      val ctxt = Proof_Context.init_global thy;
    1.76 -    val exec = spec_of thy;
    1.77 +    val spec = spec_of thy;
    1.78      fun pretty_equations const thms =
    1.79        (Pretty.block o Pretty.fbreaks)
    1.80          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
    1.81 @@ -1047,11 +1048,11 @@
    1.82        | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
    1.83            Pretty.str (string_of_const thy const), Pretty.str "with",
    1.84            (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
    1.85 -    val functions = functions_of exec
    1.86 +    val functions = functions_of spec
    1.87        |> Symtab.dest
    1.88        |> (map o apsnd) (snd o fst)
    1.89        |> sort (string_ord o apply2 fst);
    1.90 -    val datatypes = types_of exec
    1.91 +    val datatypes = types_of spec
    1.92        |> Symtab.dest
    1.93        |> map (fn (tyco, (_, (vs, spec)) :: _) =>
    1.94            ((tyco, vs), constructors_of spec))
    1.95 @@ -1105,7 +1106,7 @@
    1.96      fun update_subsume verbose (thm, proper) eqns = 
    1.97        let
    1.98          val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
    1.99 -          o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.100 +          o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
   1.101          val args = args_of thm;
   1.102          val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
   1.103          fun matches_args args' =
   1.104 @@ -1184,7 +1185,7 @@
   1.105  fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
   1.106   of SOME (thm, _) =>
   1.107        let
   1.108 -        fun del_eqn' (Eqns_Default _) = initial_fun_spec
   1.109 +        fun del_eqn' (Eqns_Default _) = default_fun_spec
   1.110            | del_eqn' (Eqns eqns) =
   1.111                let
   1.112                  val eqns' = filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns
   1.113 @@ -1236,16 +1237,16 @@
   1.114             then insert (op =) case_const cases
   1.115             else cases)
   1.116        | register_for_constructors (x as Abstractor _) = x;
   1.117 -    val register_type = (map_typs o Symtab.map)
   1.118 +    val register_type = (map_types o Symtab.map)
   1.119        (K ((map o apsnd o apsnd) register_for_constructors));
   1.120    in
   1.121      thy
   1.122      |> `(fn thy => case_cong thy case_const entry)
   1.123 -    |-> (fn cong => map_exec_purge (register_case cong #> register_type))
   1.124 +    |-> (fn cong => map_spec_purge (register_case cong #> register_type))
   1.125    end;
   1.126  
   1.127  fun add_undefined c thy =
   1.128 -  (map_exec_purge o map_undefineds) (Symtab.update (c, ())) thy;
   1.129 +  (map_spec_purge o map_undefineds) (Symtab.update (c, ())) thy;
   1.130  
   1.131  
   1.132  (* types *)
   1.133 @@ -1272,8 +1273,8 @@
   1.134    in
   1.135      thy
   1.136      |> fold del_eqns (outdated_funs1 @ outdated_funs2)
   1.137 -    |> map_exec_purge
   1.138 -        ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
   1.139 +    |> map_spec_purge
   1.140 +        ((map_types o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
   1.141          #> map_cases drop_outdated_cases)
   1.142    end;
   1.143