Generic interpretation of theory data.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/interpretation.ML	Thu Sep 20 20:56:54 2007 +0200
@@ -0,0 +1,82 @@
+(*  Title:      Pure/interpretation.ML
+    ID:         $Id$
+    Author:     Florian Haftmann and Makarius
+
+Generic interpretation of theory data.
+*)
+
+signature THEORY_INTERPRETATOR =
+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 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 =
+struct
+
+open Key;
+
+type interpretator = T list -> theory -> theory;
+
+fun apply ips x = fold_rev (fn (_, f) => f x) ips;
+
+structure InterpretatorData = TheoryDataFun
+(
+  type T = ((serial * interpretator) list * T list) * (theory -> theory) 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 consolidate thy =
+  (case #2 (InterpretatorData.get thy) of
+    [] => NONE
+  | upd => SOME (thy |> Library.apply upd |> (InterpretatorData.map o apsnd) (K [])));
+
+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;
+