avoid name particle "the" where no selection is implied
authorhaftmann
Tue Jun 20 08:01:56 2017 +0200 (2017-06-20)
changeset 661298a3b141179c2
parent 66128 0181bb24bdca
child 66130 d0476618a94c
avoid name particle "the" where no selection is implied
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 @@ -232,10 +232,10 @@
     1.4    in make_spec (false, (functions, (types, (cases, undefineds)))) end;
     1.5  
     1.6  fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
     1.7 -fun the_functions (Spec { functions, ... }) = functions;
     1.8 -fun the_types (Spec { types, ... }) = types;
     1.9 -fun the_cases (Spec { cases, ... }) = cases;
    1.10 -fun the_undefineds (Spec { undefineds, ... }) = undefineds;
    1.11 +fun types_of (Spec { types, ... }) = types;
    1.12 +fun functions_of (Spec { functions, ... }) = functions;
    1.13 +fun cases_of (Spec { cases, ... }) = cases;
    1.14 +fun undefineds_of (Spec { undefineds, ... }) = undefineds;
    1.15  val map_history_concluded = map_spec o apfst;
    1.16  val map_functions = map_spec o apsnd o apfst;
    1.17  val map_typs = map_spec o apsnd o apsnd o apfst;
    1.18 @@ -295,7 +295,7 @@
    1.19  
    1.20  (* access to executable code *)
    1.21  
    1.22 -val the_exec : theory -> spec = fst o Code_Data.get;
    1.23 +val spec_of : theory -> spec = fst o Code_Data.get;
    1.24  
    1.25  fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
    1.26  
    1.27 @@ -306,13 +306,13 @@
    1.28  
    1.29  (* tackling equation history *)
    1.30  
    1.31 -fun continue_history thy = if (history_concluded o the_exec) thy
    1.32 +fun continue_history thy = if (history_concluded o spec_of) thy
    1.33    then thy
    1.34      |> (Code_Data.map o apfst o map_history_concluded) (K false)
    1.35      |> SOME
    1.36    else NONE;
    1.37  
    1.38 -fun conclude_history thy = if (history_concluded o the_exec) thy
    1.39 +fun conclude_history thy = if (history_concluded o spec_of) thy
    1.40    then NONE
    1.41    else thy
    1.42      |> (Code_Data.map o apfst)
    1.43 @@ -395,7 +395,7 @@
    1.44      val constructors = map (inst vs o snd) raw_constructors;
    1.45    in (tyco, (map (rpair []) vs, constructors)) end;
    1.46  
    1.47 -fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
    1.48 +fun get_type_entry thy tyco = case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
    1.49   of (_, entry) :: _ => SOME entry
    1.50    | _ => NONE;
    1.51  
    1.52 @@ -909,7 +909,7 @@
    1.53  (* code certificate access with preprocessing *)
    1.54  
    1.55  fun retrieve_raw thy c =
    1.56 -  Symtab.lookup ((the_functions o the_exec) thy) c
    1.57 +  Symtab.lookup ((functions_of o spec_of) thy) c
    1.58    |> Option.map (snd o fst)
    1.59    |> the_default Unimplemented
    1.60  
    1.61 @@ -1003,11 +1003,11 @@
    1.62  end;
    1.63  
    1.64  fun get_case_scheme thy =
    1.65 -  Option.map fst o (Symtab.lookup o the_cases o the_exec) thy;
    1.66 +  Option.map fst o (Symtab.lookup o cases_of o spec_of) thy;
    1.67  fun get_case_cong thy =
    1.68 -  Option.map snd o (Symtab.lookup o the_cases o the_exec) thy;
    1.69 +  Option.map snd o (Symtab.lookup o cases_of o spec_of) thy;
    1.70  
    1.71 -val undefineds = Symtab.keys o the_undefineds o the_exec;
    1.72 +val undefineds = Symtab.keys o undefineds_of o spec_of;
    1.73  
    1.74  
    1.75  (* diagnostic *)
    1.76 @@ -1015,7 +1015,7 @@
    1.77  fun print_codesetup thy =
    1.78    let
    1.79      val ctxt = Proof_Context.init_global thy;
    1.80 -    val exec = the_exec thy;
    1.81 +    val exec = spec_of thy;
    1.82      fun pretty_equations const thms =
    1.83        (Pretty.block o Pretty.fbreaks)
    1.84          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
    1.85 @@ -1047,17 +1047,17 @@
    1.86        | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
    1.87            Pretty.str (string_of_const thy const), Pretty.str "with",
    1.88            (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
    1.89 -    val functions = the_functions exec
    1.90 +    val functions = functions_of exec
    1.91        |> Symtab.dest
    1.92        |> (map o apsnd) (snd o fst)
    1.93        |> sort (string_ord o apply2 fst);
    1.94 -    val datatypes = the_types exec
    1.95 +    val datatypes = types_of exec
    1.96        |> Symtab.dest
    1.97        |> map (fn (tyco, (_, (vs, spec)) :: _) =>
    1.98            ((tyco, vs), constructors_of spec))
    1.99        |> sort (string_ord o apply2 (fst o fst));
   1.100 -    val cases = Symtab.dest ((the_cases o the_exec) thy);
   1.101 -    val undefineds = Symtab.keys ((the_undefineds o the_exec) thy);
   1.102 +    val cases = Symtab.dest ((cases_of o spec_of) thy);
   1.103 +    val undefineds = Symtab.keys ((undefineds_of o spec_of) thy);
   1.104    in
   1.105      Pretty.writeln_chunks [
   1.106        Pretty.block (
   1.107 @@ -1253,7 +1253,7 @@
   1.108  fun register_type (tyco, vs_spec) thy =
   1.109    let
   1.110      val (old_constrs, some_old_proj) =
   1.111 -      case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
   1.112 +      case these (Symtab.lookup ((types_of o spec_of) thy) tyco)
   1.113         of (_, (_, Constructors (cos, _))) :: _ => (map fst cos, NONE)
   1.114          | (_, (_, Abstractor ((co, _), (proj, _)))) :: _ => ([co], SOME proj)
   1.115          | [] => ([], NONE);
   1.116 @@ -1264,7 +1264,7 @@
   1.117            (fn (c, ((_, spec), _)) =>
   1.118              if member (op =) (the_list (associated_abstype spec)) tyco
   1.119              then insert (op =) c else I)
   1.120 -            ((the_functions o the_exec) thy) [old_proj];
   1.121 +            ((functions_of o spec_of) thy) [old_proj];
   1.122      fun drop_outdated_cases cases = fold Symtab.delete_safe
   1.123        (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
   1.124          if exists (member (op =) old_constrs) (map_filter I cos)