# HG changeset patch
# User wenzelm
# Date 1190727275 -7200
# Node ID e8bba7723858a89bf9a8d90ff0e7cf6cd2924c9a
# Parent  141df8b68f6321e51bf0b67dc5da2332fff65676
simplified interpretation setup;

diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/datatype_codegen.ML
--- 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
diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/datatype_package.ML
--- 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 *)
diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/datatype_realizer.ML
--- 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;
diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/function_package/fundef_package.ML
--- 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
 
 
 
diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/function_package/size.ML
--- 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
diff -r 141df8b68f63 -r e8bba7723858 src/HOL/Tools/typecopy_package.ML
--- 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;
diff -r 141df8b68f63 -r e8bba7723858 src/Pure/interpretation.ML
--- 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;