src/Pure/theory.ML
changeset 24626 85eceef2edc7
parent 24199 8be734b5f59f
child 24666 9885a86f14a8
--- a/src/Pure/theory.ML	Tue Sep 18 07:36:38 2007 +0200
+++ b/src/Pure/theory.ML	Tue Sep 18 07:46:00 2007 +0200
@@ -51,10 +51,108 @@
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
 
-structure Theory: THEORY =
+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;
+
+structure Theory =
 struct
 
 
+(** datatype thy **)
+
+datatype thy = Thy of
+ {axioms: term NameSpace.table,
+  defs: Defs.T,
+  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
+  consolidate: theory -> theory};
+
+fun make_thy (axioms, defs, oracles, consolidate) =
+  Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
+
+fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
+
+structure ThyData = TheoryDataFun
+(
+  type T = thy;
+  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
+  val copy = I;
+
+  fun extend (Thy {axioms, defs, oracles, consolidate}) =
+    make_thy (NameSpace.empty_table, defs, oracles, consolidate);
+
+  fun merge pp (thy1, thy2) =
+    let
+      val Thy {axioms = _, defs = defs1, oracles = oracles1,
+        consolidate = consolidate1} = thy1;
+      val Thy {axioms = _, defs = defs2, oracles = oracles2,
+        consolidate = consolidate2} = thy2;
+
+      val axioms = NameSpace.empty_table;
+      val defs = Defs.merge pp (defs1, defs2);
+      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
+        handle Symtab.DUP dup => err_dup_ora dup;
+      val consolidate = consolidate1 #> consolidate2;
+    in make_thy (axioms, defs, oracles, consolidate) end;
+);
+
+fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
+  {axioms = axioms, defs = defs, oracles = oracles});
+
+fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
+  make_thy (f (axioms, defs, oracles, consolidate)));
+
+fun map_axioms f = map_thy
+  (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
+fun map_defs f = map_thy
+  (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
+fun map_oracles f = map_thy
+  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
+
+
+(* basic operations *)
+
+val axiom_space = #1 o #axioms o rep_theory;
+val axiom_table = #2 o #axioms o rep_theory;
+
+val oracle_space = #1 o #oracles o rep_theory;
+val oracle_table = #2 o #oracles o rep_theory;
+
+val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
+
+val defs_of = #defs o rep_theory;
+
+fun requires thy name what =
+  if Context.exists_name name thy then ()
+  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
+
+
+(* interpretators *)
+
+fun add_consolidate f = map_thy
+  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
+
+fun consolidate thy =
+  let
+    val Thy {consolidate, ...} = ThyData.get thy;
+  in
+    thy |> consolidate
+  end;
+
+
 (** type theory **)
 
 (* context operations *)
@@ -62,6 +160,10 @@
 val eq_thy = Context.eq_thy;
 val subthy = Context.subthy;
 
+fun assert_super thy1 thy2 =
+  if subthy (thy1, thy2) then thy2
+  else raise THEORY ("Not a super theory", [thy1, thy2]);
+
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 
@@ -73,7 +175,7 @@
 fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
 
-val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
+val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
 val end_theory = Context.finish_thy;
 val checkpoint = Context.checkpoint_thy;
 val copy = Context.copy_thy;
@@ -86,73 +188,10 @@
 
 
 
-(** datatype thy **)
-
-datatype thy = Thy of
- {axioms: term NameSpace.table,
-  defs: Defs.T,
-  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table};
-
-fun make_thy (axioms, defs, oracles) =
-  Thy {axioms = axioms, defs = defs, oracles = oracles};
-
-fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
-
-structure ThyData = TheoryDataFun
-(
-  type T = thy;
-  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
-  val copy = I;
-
-  fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles);
-
-  fun merge pp (thy1, thy2) =
-    let
-      val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
-      val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
+(** axioms **)
 
-      val axioms = NameSpace.empty_table;
-      val defs = Defs.merge pp (defs1, defs2);
-      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
-        handle Symtab.DUP dup => err_dup_ora dup;
-    in make_thy (axioms, defs, oracles) end;
-);
-
-fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
-
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) =>
-  make_thy (f (axioms, defs, oracles)));
-
-fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles));
-fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles));
-fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles));
-
-
-(* basic operations *)
-
-val axiom_space = #1 o #axioms o rep_theory;
-val axiom_table = #2 o #axioms o rep_theory;
-
-val oracle_space = #1 o #oracles o rep_theory;
-val oracle_table = #2 o #oracles o rep_theory;
-
-val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
 
-val defs_of = #defs o rep_theory;
-
-fun requires thy name what =
-  if Context.exists_name name thy then ()
-  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
-
-fun assert_super thy1 thy2 =
-  if subthy (thy1, thy2) then thy2
-  else raise THEORY ("Not a super theory", [thy1, thy2]);
-
-
-
-(** add axioms **)
 
 (* prepare axioms *)
 
@@ -311,5 +350,66 @@
 
 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);
+  val empty = (([], []), I);
+  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 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 =
+  let
+    val (_, upd) = InterpretatorData.get thy;
+  in
+    thy |> upd |> (InterpretatorData.map o apsnd) (K I)
+  end;
+
+val init = Theory.add_consolidate 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;
+
+structure Theory: THEORY = Theory;
 structure BasicTheory: BASIC_THEORY = Theory;
 open BasicTheory;