--- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 25 15:34:35 2007 +0200
@@ -486,8 +486,8 @@
hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
in
thy
- |> DatatypePackage.add_interpretator datatype_hook
- |> TypecopyPackage.add_interpretator typecopy_hook
+ |> DatatypePackage.interpretation datatype_hook
+ |> TypecopyPackage.interpretation typecopy_hook
end;
fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
@@ -604,8 +604,8 @@
val setup =
add_codegen "datatype" datatype_codegen
#> add_tycodegen "datatype" datatype_tycodegen
- #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
- #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
+ #> DatatypePackage.interpretation (fold add_datatype_case_const)
+ #> DatatypePackage.interpretation (fold add_datatype_case_defs)
val setup_hooks =
add_codetypes_hook codetype_hook
--- a/src/HOL/Tools/datatype_package.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Sep 25 15:34:35 2007 +0200
@@ -65,7 +65,7 @@
val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
val get_datatype_constrs : theory -> string -> (string * typ) list option
- val add_interpretator: (string list -> theory -> theory) -> theory -> theory
+ val interpretation: (string list -> theory -> theory) -> theory -> theory
val print_datatypes : theory -> unit
val make_case : Proof.context -> bool -> string list -> term ->
(term * term) list -> term * (term * (int * bool)) list
@@ -134,7 +134,7 @@
fun get_datatype_descr thy dtco =
get_datatype thy dtco
- |> Option.map (fn info as { descr, index, ... } =>
+ |> Option.map (fn info as { descr, index, ... } =>
(info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
fun get_datatype_spec thy dtco =
@@ -210,7 +210,7 @@
in
-fun gen_induct_tac inst_tac (varss, opt_rule) i state =
+fun gen_induct_tac inst_tac (varss, opt_rule) i state =
SUBGOAL (fn (Bi,_) =>
let
val (rule, rule_name) =
@@ -219,7 +219,7 @@
| NONE =>
let val tn = find_tname (hd (map_filter I (flat varss))) Bi
val thy = Thm.theory_of_thm state
- in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
+ in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
end
val concls = HOLogic.dest_concls (Thm.concl_of rule);
val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
@@ -423,7 +423,7 @@
fun add_case_tr' case_names thy =
Theory.add_advanced_trfuns ([], [],
- map (fn case_name =>
+ map (fn case_name =>
let val case_name' = Sign.const_syntax_name thy case_name
in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
end) case_names, []) thy;
@@ -519,9 +519,8 @@
val specify_consts = gen_specify_consts Sign.add_consts_i;
val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
-structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string list; val eq = op = end);
-
-fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator (fold interpretator);
+structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
+val interpretation = DatatypeInterpretation.interpretation;
fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
@@ -641,7 +640,7 @@
|> Theory.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
- |> DatatypeInterpretator.add_those [map fst dt_infos];
+ |> DatatypeInterpretation.data (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -698,7 +697,7 @@
|> add_cases_induct dt_infos induct
|> Theory.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
- |> DatatypeInterpretator.add_those [map fst dt_infos];
+ |> DatatypeInterpretation.data (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -799,7 +798,7 @@
|> Theory.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
- |> DatatypeInterpretator.add_those [map fst dt_infos];
+ |> DatatypeInterpretation.data (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -902,7 +901,7 @@
Method.add_methods tactic_emulations #>
simproc_setup #>
trfun_setup #>
- DatatypeInterpretator.init;
+ DatatypeInterpretation.init;
(* outer syntax *)
--- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 15:34:35 2007 +0200
@@ -228,6 +228,6 @@
|> fold_rev (make_casedists (#sorts info)) infos
end;
-val setup = DatatypePackage.add_interpretator add_dt_realizers;
+val setup = DatatypePackage.interpretation add_dt_realizers;
end;
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 25 15:34:35 2007 +0200
@@ -177,7 +177,7 @@
val case_cong = fold add_case_cong
-val setup_case_cong = DatatypePackage.add_interpretator case_cong
+val setup_case_cong = DatatypePackage.interpretation case_cong
--- a/src/HOL/Tools/function_package/size.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/function_package/size.ML Tue Sep 25 15:34:35 2007 +0200
@@ -204,6 +204,6 @@
fun size_thms thy = the o Symtab.lookup (SizeData.get thy);
-val setup = DatatypePackage.add_interpretator add_size_thms;
+val setup = DatatypePackage.interpretation add_size_thms;
end;
\ No newline at end of file
--- a/src/HOL/Tools/typecopy_package.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 25 15:34:35 2007 +0200
@@ -19,8 +19,7 @@
-> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_typecopy_info: theory -> string -> info option
- type interpretator = string * info -> theory -> theory
- val add_interpretator: interpretator -> theory -> theory
+ val interpretation: (string * info -> theory -> theory) -> theory -> theory
val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
val get_eq: theory -> string -> thm
val print_typecopies: theory -> unit
@@ -41,8 +40,6 @@
proj_def: thm
};
-structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
-
structure TypecopyData = TheoryDataFun
(
type T = info Symtab.table;
@@ -71,12 +68,12 @@
val get_typecopy_info = Symtab.lookup o TypecopyData.get;
-(* interpretator management *)
+(* interpretation *)
-type interpretator = string * info -> theory -> theory;
+structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
-fun add_interpretator interp = TypecopyInterpretator.add_interpretator
- (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy));
+fun interpretation interp = TypecopyInterpretation.interpretation
+ (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy);
(* add a type copy *)
@@ -108,7 +105,7 @@
in
thy
|> (TypecopyData.map o Symtab.update_new) (tyco, info)
- |> TypecopyInterpretator.add_those [tyco]
+ |> TypecopyInterpretation.data tyco
|> pair (tyco, info)
end
in
@@ -137,10 +134,10 @@
in (vs, [(constr, [typ])]) end;
-(* interpretator for projection function code *)
+(* interpretation for projection function code *)
-fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def;
+fun add_project (_, {proj_def, ...} : info) = Code.add_default_func proj_def;
-val setup = TypecopyInterpretator.init #> add_interpretator add_project;
+val setup = TypecopyInterpretation.init #> interpretation add_project;
end;
--- a/src/Pure/interpretation.ML Tue Sep 25 13:42:59 2007 +0200
+++ b/src/Pure/interpretation.ML Tue Sep 25 15:34:35 2007 +0200
@@ -5,78 +5,47 @@
Generic interpretation of theory data.
*)
-signature THEORY_INTERPRETATOR =
+signature INTERPRETATION =
sig
type T
- type interpretator = T list -> theory -> theory
- val add_those: T list -> theory -> theory
- val all_those: theory -> T list
- val add_interpretator: interpretator -> theory -> theory
+ val result: theory -> T list
+ val interpretation: (T -> theory -> theory) -> theory -> theory
+ val data: T -> theory -> theory
val init: theory -> theory
end;
-signature THEORY_INTERPRETATOR_KEY =
-sig
- type T
- val eq: T * T -> bool
-end;
-
-functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
+functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
struct
-open Key;
-
-type interpretator = T list -> theory -> theory;
+type T = T;
-fun apply ips x = fold_rev (fn (_, f) => f x) ips;
-
-structure InterpretatorData = TheoryDataFun
+structure Interp = TheoryDataFun
(
- type T = ((serial * interpretator) list * T list) * (theory -> theory) list;
- val empty = (([], []), []);
+ type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
+ val empty = ([], []);
val extend = I;
val copy = I;
- fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
- let
- fun diff (interpretators1 : (serial * interpretator) list, done1)
- (interpretators2, done2) = let
- val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
- val undone = subtract eq done2 done1;
- in if null interpretators then [] else [apply interpretators undone] end;
- val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
- val done = Library.merge eq (done1, done2);
- val upd_new = diff (interpretators2, done2) (interpretators1, done1)
- @ diff (interpretators1, done1) (interpretators2, done2);
- val upd = upd1 @ upd2 @ upd_new;
- in ((interpretators, done), upd) end;
+ fun merge _ ((data1, interps1), (data2, interps2)) : T =
+ (Library.merge eq (data1, data2),
+ AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
);
+val result = #1 o Interp.get;
+
fun consolidate thy =
- (case #2 (InterpretatorData.get thy) of
- [] => NONE
- | upd => SOME (thy |> Library.apply upd |> (InterpretatorData.map o apsnd) (K [])));
+ let
+ val (data, interps) = Interp.get thy;
+ val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
+ val finished = map (fn (interp, _) => (interp, data)) interps;
+ in
+ if forall (null o #2) unfinished then NONE
+ else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
+ end;
+
+fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
+fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
val init = Theory.at_begin consolidate;
-fun add_those xs thy =
- let
- val ((interpretators, _), _) = InterpretatorData.get thy;
- in
- thy
- |> apply interpretators xs
- |> (InterpretatorData.map o apfst o apsnd) (append xs)
- end;
-
-val all_those = snd o fst o InterpretatorData.get;
-
-fun add_interpretator interpretator thy =
- let
- val ((interpretators, xs), _) = InterpretatorData.get thy;
- in
- thy
- |> interpretator (rev xs)
- |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
- end;
-
end;