# 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(