# HG changeset patch
# User haftmann
# Date 1244581195 -7200
# Node ID 97b4d289c64658d4d4e6e23322a0c4b26cb3a5ab
# Parent  946a7a175bf1a1146a15122315c01f45e5f8c24f
tuned make/map/merge combinators

diff -r 946a7a175bf1 -r 97b4d289c646 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Tue Jun 09 22:59:55 2009 +0200
@@ -127,22 +127,21 @@
 
 };
 
-fun rep_class_data (ClassData data) = data;
-fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+fun make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
   ClassData { consts = consts, base_sort = base_sort,
     base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
     defs = defs, operations = operations };
 fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
     of_class, axiom, defs, operations }) =
-  mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+  make_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
     base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
   ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
     of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
-  mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
+  make_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
@@ -158,7 +157,9 @@
 
 (* queries *)
 
-val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
+fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
+ of SOME (ClassData data) => SOME data
+  | NONE => NONE;
 
 fun the_class_data thy class = case lookup_class_data thy class
  of NONE => error ("Undeclared class " ^ quote class)
@@ -188,8 +189,8 @@
   in (axiom, of_class) end;
 
 fun all_assm_intros thy =
-  Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
-    ((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
+  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
+    (the_list assm_intro)) (ClassData.get thy) [];
 
 fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
@@ -240,7 +241,7 @@
     val operations = map (fn (v_ty as (_, ty), (c, _)) =>
       (c, (class, (ty, Free v_ty)))) params;
     val add_class = Graph.new_node (class,
-        mk_class_data (((map o pairself) fst params, base_sort,
+        make_class_data (((map o pairself) fst params, base_sort,
           morph, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) sups;
   in ClassData.map add_class thy end;
diff -r 946a7a175bf1 -r 97b4d289c646 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Jun 09 22:59:55 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jun 09 22:59:55 2009 +0200
@@ -580,13 +580,11 @@
   cases: (int * (int * string list)) Symtab.table * unit Symtab.table
 };
 
-fun mk_spec ((concluded_history, eqns), (dtyps, cases)) =
+fun make_spec ((concluded_history, eqns), (dtyps, cases)) =
   Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases };
-val empty_spec =
-  mk_spec ((false, Symtab.empty), (Symtab.empty, (Symtab.empty, Symtab.empty)));
 fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns,
   dtyps = dtyps, cases = cases }) =
-  mk_spec (f ((concluded_history, eqns), (dtyps, cases)));
+  make_spec (f ((concluded_history, eqns), (dtyps, cases)));
 fun merge_spec (Spec { concluded_history = _, eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) },
   Spec { concluded_history = _, eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) =
   let
@@ -602,15 +600,16 @@
     val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
     val cases = (Symtab.merge (K true) (cases1, cases2),
       Symtab.merge (K true) (undefs1, undefs2));
-  in mk_spec ((false, eqns), (dtyps, cases)) end;
+  in make_spec ((false, eqns), (dtyps, cases)) end;
 
 
 (* code setup data *)
 
 fun the_spec (Spec x) = x;
-val the_eqns = #eqns o the_spec;
-val the_dtyps = #dtyps o the_spec;
-val the_cases = #cases o the_spec;
+fun the_eqns (Spec { eqns, ... }) = eqns;
+fun the_dtyps (Spec { dtyps, ... }) = dtyps;
+fun the_cases (Spec { cases, ... }) = cases;
+fun history_concluded (Spec { concluded_history, ... }) = concluded_history;
 val map_concluded_history = map_spec o apfst o apfst;
 val map_eqns = map_spec o apfst o apsnd;
 val map_dtyps = map_spec o apsnd o apfst;
@@ -665,7 +664,8 @@
 structure Code_Data = TheoryDataFun
 (
   type T = spec * data ref;
-  val empty = (empty_spec, ref empty_data);
+  val empty = (make_spec ((false, Symtab.empty),
+    (Symtab.empty, (Symtab.empty, Symtab.empty))), ref empty_data);
   fun copy (spec, data) = (spec, ref (! data));
   val extend = copy;
   fun merge pp ((spec1, data1), (spec2, data2)) =
@@ -706,13 +706,13 @@
   |> Option.map (Lazy.force o snd o snd o fst)
   |> these;
 
-fun continue_history thy = if (#concluded_history o the_spec o the_exec) thy
+fun continue_history thy = if (history_concluded o the_exec) thy
   then thy
     |> (Code_Data.map o apfst o map_concluded_history) (K false)
     |> SOME
   else NONE;
 
-fun conclude_history thy = if (#concluded_history o the_spec o the_exec) thy
+fun conclude_history thy = if (history_concluded o the_exec) thy
   then NONE
   else thy
     |> (Code_Data.map o apfst)
diff -r 946a7a175bf1 -r 97b4d289c646 src/Tools/code/code_preproc.ML
--- a/src/Tools/code/code_preproc.ML	Tue Jun 09 22:59:55 2009 +0200
+++ b/src/Tools/code/code_preproc.ML	Tue Jun 09 22:59:55 2009 +0200
@@ -44,22 +44,22 @@
   functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
 };
 
-fun mk_thmproc ((pre, post), functrans) =
+fun make_thmproc ((pre, post), functrans) =
   Thmproc { pre = pre, post = post, functrans = functrans };
 fun map_thmproc f (Thmproc { pre, post, functrans }) =
-  mk_thmproc (f ((pre, post), functrans));
+  make_thmproc (f ((pre, post), functrans));
 fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
   Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
     let
       val pre = Simplifier.merge_ss (pre1, pre2);
       val post = Simplifier.merge_ss (post1, post2);
       val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
-    in mk_thmproc ((pre, post), functrans) end;
+    in make_thmproc ((pre, post), functrans) end;
 
 structure Code_Preproc_Data = TheoryDataFun
 (
   type T = thmproc;
-  val empty = mk_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
+  val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
   fun copy spec = spec;
   val extend = copy;
   fun merge pp = merge_thmproc;
diff -r 946a7a175bf1 -r 97b4d289c646 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Jun 09 22:59:55 2009 +0200
+++ b/src/Tools/code/code_target.ML	Tue Jun 09 22:59:55 2009 +0200
@@ -128,11 +128,11 @@
   module_alias: string Symtab.table
 };
 
-fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
+fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
   Target { serial = serial, serializer = serializer, reserved = reserved, 
     includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
 fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
-  mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
+  make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
 fun merge_target strict target (Target { serial = serial1, serializer = serializer,
   reserved = reserved1, includes = includes1,
   name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
@@ -140,7 +140,7 @@
       reserved = reserved2, includes = includes2,
       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   if serial1 = serial2 orelse not strict then
-    mk_target ((serial1, serializer),
+    make_target ((serial1, serializer),
       ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
           Symtab.join (K snd) (module_alias1, module_alias2))
@@ -190,7 +190,7 @@
   in
     thy
     |> (CodeTargetData.map o apfst oo Symtab.map_default)
-          (target, mk_target ((serial (), seri), (([], Symtab.empty),
+          (target, make_target ((serial (), seri), (([], Symtab.empty),
             (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
               Symtab.empty))))
           ((map_target o apfst o apsnd o K) seri)
diff -r 946a7a175bf1 -r 97b4d289c646 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Jun 09 22:59:55 2009 +0200
+++ b/src/Tools/quickcheck.ML	Tue Jun 09 22:59:55 2009 +0200
@@ -42,13 +42,13 @@
 
 fun dest_test_params (Test_Params { size, iterations, default_type }) =
   ((size, iterations), default_type);
-fun mk_test_params ((size, iterations), default_type) =
+fun make_test_params ((size, iterations), default_type) =
   Test_Params { size = size, iterations = iterations, default_type = default_type };
 fun map_test_params f (Test_Params { size, iterations, default_type}) =
-  mk_test_params (f ((size, iterations), default_type));
+  make_test_params (f ((size, iterations), default_type));
 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 },
   Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) =
-  mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
+  make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
     case default_type1 of NONE => default_type2 | _ => default_type1);
 
 structure Data = TheoryDataFun(