--- 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;
--- 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)
--- 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;
--- 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)
--- 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(