tuned make/map/merge combinators
authorhaftmann
Tue Jun 09 22:59:55 2009 +0200 (2009-06-09)
changeset 3159997b4d289c646
parent 31598 946a7a175bf1
child 31600 c4ab772b3e8b
tuned make/map/merge combinators
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Tools/code/code_preproc.ML
src/Tools/code/code_target.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
     1.3 @@ -127,22 +127,21 @@
     1.4  
     1.5  };
     1.6  
     1.7 -fun rep_class_data (ClassData data) = data;
     1.8 -fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     1.9 +fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.10      (defs, operations)) =
    1.11    ClassData { consts = consts, base_sort = base_sort,
    1.12      base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
    1.13      defs = defs, operations = operations };
    1.14  fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
    1.15      of_class, axiom, defs, operations }) =
    1.16 -  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.17 +  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.18      (defs, operations)));
    1.19  fun merge_class_data _ (ClassData { consts = consts,
    1.20      base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
    1.21      of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
    1.22    ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
    1.23      of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
    1.24 -  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.25 +  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
    1.26      (Thm.merge_thms (defs1, defs2),
    1.27        AList.merge (op =) (K true) (operations1, operations2)));
    1.28  
    1.29 @@ -158,7 +157,9 @@
    1.30  
    1.31  (* queries *)
    1.32  
    1.33 -val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
    1.34 +fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
    1.35 + of SOME (ClassData data) => SOME data
    1.36 +  | NONE => NONE;
    1.37  
    1.38  fun the_class_data thy class = case lookup_class_data thy class
    1.39   of NONE => error ("Undeclared class " ^ quote class)
    1.40 @@ -188,8 +189,8 @@
    1.41    in (axiom, of_class) end;
    1.42  
    1.43  fun all_assm_intros thy =
    1.44 -  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
    1.45 -    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
    1.46 +  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
    1.47 +    (the_list assm_intro)) (ClassData.get thy) [];
    1.48  
    1.49  fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
    1.50  fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
    1.51 @@ -240,7 +241,7 @@
    1.52      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
    1.53        (c, (class, (ty, Free v_ty)))) params;
    1.54      val add_class = Graph.new_node (class,
    1.55 -        mk_class_data (((map o pairself) fst params, base_sort,
    1.56 +        make_class_data (((map o pairself) fst params, base_sort,
    1.57            morph, assm_intro, of_class, axiom), ([], operations)))
    1.58        #> fold (curry Graph.add_edge class) sups;
    1.59    in ClassData.map add_class thy end;
     2.1 --- a/src/Pure/Isar/code.ML	Tue Jun 09 22:59:55 2009 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 09 22:59:55 2009 +0200
     2.3 @@ -580,13 +580,11 @@
     2.4    cases: (int * (int * string list)) Symtab.table * unit Symtab.table
     2.5  };
     2.6  
     2.7 -fun mk_spec ((concluded_history, eqns), (dtyps, cases)) =
     2.8 +fun make_spec ((concluded_history, eqns), (dtyps, cases)) =
     2.9    Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases };
    2.10 -val empty_spec =
    2.11 -  mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty)));
    2.12  fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns,
    2.13    dtyps = dtyps, cases = cases }) =
    2.14 -  mk_spec (f ((concluded_history, eqns), (dtyps, cases)));
    2.15 +  make_spec (f ((concluded_history, eqns), (dtyps, cases)));
    2.16  fun merge_spec (Spec { concluded_history = _, eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) },
    2.17    Spec { concluded_history = _, eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
    2.18    let
    2.19 @@ -602,15 +600,16 @@
    2.20      val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
    2.21      val cases = (Symtab.merge (K true) (cases1, cases2),
    2.22        Symtab.merge (K true) (undefs1, undefs2));
    2.23 -  in mk_spec ((false, eqns), (dtyps, cases)) end;
    2.24 +  in make_spec ((false, eqns), (dtyps, cases)) end;
    2.25  
    2.26  
    2.27  (* code setup data *)
    2.28  
    2.29  fun the_spec (Spec x) = x;
    2.30 -val the_eqns = #eqns o the_spec;
    2.31 -val the_dtyps = #dtyps o the_spec;
    2.32 -val the_cases = #cases o the_spec;
    2.33 +fun the_eqns (Spec { eqns, ... }) = eqns;
    2.34 +fun the_dtyps (Spec { dtyps, ... }) = dtyps;
    2.35 +fun the_cases (Spec { cases, ... }) = cases;
    2.36 +fun history_concluded (Spec { concluded_history, ... }) = concluded_history;
    2.37  val map_concluded_history = map_spec o apfst o apfst;
    2.38  val map_eqns = map_spec o apfst o apsnd;
    2.39  val map_dtyps = map_spec o apsnd o apfst;
    2.40 @@ -665,7 +664,8 @@
    2.41  structure Code_Data = TheoryDataFun
    2.42  (
    2.43    type T = spec * data ref;
    2.44 -  val empty = (empty_spec, ref empty_data);
    2.45 +  val empty = (make_spec ((false, Symtab.empty),
    2.46 +    (Symtab.empty, (Symtab.empty, Symtab.empty))), ref empty_data);
    2.47    fun copy (spec, data) = (spec, ref (! data));
    2.48    val extend = copy;
    2.49    fun merge pp ((spec1, data1), (spec2, data2)) =
    2.50 @@ -706,13 +706,13 @@
    2.51    |> Option.map (Lazy.force o snd o snd o fst)
    2.52    |> these;
    2.53  
    2.54 -fun continue_history thy = if (#concluded_history o the_spec o the_exec) thy
    2.55 +fun continue_history thy = if (history_concluded o the_exec) thy
    2.56    then thy
    2.57      |> (Code_Data.map o apfst o map_concluded_history) (K false)
    2.58      |> SOME
    2.59    else NONE;
    2.60  
    2.61 -fun conclude_history thy = if (#concluded_history o the_spec o the_exec) thy
    2.62 +fun conclude_history thy = if (history_concluded o the_exec) thy
    2.63    then NONE
    2.64    else thy
    2.65      |> (Code_Data.map o apfst)
     3.1 --- a/src/Tools/code/code_preproc.ML	Tue Jun 09 22:59:55 2009 +0200
     3.2 +++ b/src/Tools/code/code_preproc.ML	Tue Jun 09 22:59:55 2009 +0200
     3.3 @@ -44,22 +44,22 @@
     3.4    functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
     3.5  };
     3.6  
     3.7 -fun mk_thmproc ((pre, post), functrans) =
     3.8 +fun make_thmproc ((pre, post), functrans) =
     3.9    Thmproc { pre = pre, post = post, functrans = functrans };
    3.10  fun map_thmproc f (Thmproc { pre, post, functrans }) =
    3.11 -  mk_thmproc (f ((pre, post), functrans));
    3.12 +  make_thmproc (f ((pre, post), functrans));
    3.13  fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
    3.14    Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
    3.15      let
    3.16        val pre = Simplifier.merge_ss (pre1, pre2);
    3.17        val post = Simplifier.merge_ss (post1, post2);
    3.18        val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    3.19 -    in mk_thmproc ((pre, post), functrans) end;
    3.20 +    in make_thmproc ((pre, post), functrans) end;
    3.21  
    3.22  structure Code_Preproc_Data = TheoryDataFun
    3.23  (
    3.24    type T = thmproc;
    3.25 -  val empty = mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
    3.26 +  val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
    3.27    fun copy spec = spec;
    3.28    val extend = copy;
    3.29    fun merge pp = merge_thmproc;
     4.1 --- a/src/Tools/code/code_target.ML	Tue Jun 09 22:59:55 2009 +0200
     4.2 +++ b/src/Tools/code/code_target.ML	Tue Jun 09 22:59:55 2009 +0200
     4.3 @@ -128,11 +128,11 @@
     4.4    module_alias: string Symtab.table
     4.5  };
     4.6  
     4.7 -fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
     4.8 +fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
     4.9    Target { serial = serial, serializer = serializer, reserved = reserved, 
    4.10      includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
    4.11  fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
    4.12 -  mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
    4.13 +  make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
    4.14  fun merge_target strict target (Target { serial = serial1, serializer = serializer,
    4.15    reserved = reserved1, includes = includes1,
    4.16    name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
    4.17 @@ -140,7 +140,7 @@
    4.18        reserved = reserved2, includes = includes2,
    4.19        name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
    4.20    if serial1 = serial2 orelse not strict then
    4.21 -    mk_target ((serial1, serializer),
    4.22 +    make_target ((serial1, serializer),
    4.23        ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
    4.24          (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
    4.25            Symtab.join (K snd) (module_alias1, module_alias2))
    4.26 @@ -190,7 +190,7 @@
    4.27    in
    4.28      thy
    4.29      |> (CodeTargetData.map o apfst oo Symtab.map_default)
    4.30 -          (target, mk_target ((serial (), seri), (([], Symtab.empty),
    4.31 +          (target, make_target ((serial (), seri), (([], Symtab.empty),
    4.32              (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
    4.33                Symtab.empty))))
    4.34            ((map_target o apfst o apsnd o K) seri)
     5.1 --- a/src/Tools/quickcheck.ML	Tue Jun 09 22:59:55 2009 +0200
     5.2 +++ b/src/Tools/quickcheck.ML	Tue Jun 09 22:59:55 2009 +0200
     5.3 @@ -42,13 +42,13 @@
     5.4  
     5.5  fun dest_test_params (Test_Params { size, iterations, default_type }) =
     5.6    ((size, iterations), default_type);
     5.7 -fun mk_test_params ((size, iterations), default_type) =
     5.8 +fun make_test_params ((size, iterations), default_type) =
     5.9    Test_Params { size = size, iterations = iterations, default_type = default_type };
    5.10  fun map_test_params f (Test_Params { size, iterations, default_type}) =
    5.11 -  mk_test_params (f ((size, iterations), default_type));
    5.12 +  make_test_params (f ((size, iterations), default_type));
    5.13  fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
    5.14    Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
    5.15 -  mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    5.16 +  make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    5.17      case default_type1 of NONE => default_type2 | _ => default_type1);
    5.18  
    5.19  structure Data = TheoryDataFun(