support dynamic facts;

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:58 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:59 2008 +0100
@@ -811,7 +811,7 @@
         val thms =
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
-            (case Facts.lookup local_facts name of
+            (case Facts.lookup (Context.Proof ctxt) local_facts name of
               SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
             | NONE => from_thy thy xthmref);
       in pick name thms end;

--- a/src/Pure/facts.ML	Tue Mar 25 19:39:58 2008 +0100
+++ b/src/Pure/facts.ML	Tue Mar 25 19:39:59 2008 +0100
@@ -20,17 +20,18 @@
   val select: ref -> thm list -> thm list
   val selections: string * thm list -> (ref * thm) list
   type T
+  val empty: T
   val space_of: T -> NameSpace.T
-  val lookup: T -> string -> thm list option
+  val lookup: Context.generic -> T -> string -> thm list option
   val dest: T -> (string * thm list) list
   val extern: T -> (xstring * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list
-  val empty: T
   val merge: T * T -> T
+  val del: string -> T -> T
   val add_global: NameSpace.naming -> string * thm list -> T -> T
   val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
-  val del: string -> T -> T
+  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
 end;
 
 structure Facts: FACTS =
@@ -112,13 +113,16 @@
 
 (** fact environment **)
 
-(* datatype T *)
+(* datatypes *)
+
+datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
 
 datatype T = Facts of
- {facts: thm list NameSpace.table,
+ {facts: (fact * serial) NameSpace.table,
   props: thm Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
+val empty = make_facts NameSpace.empty_table Net.empty;
 
 
 (* named facts *)
@@ -126,9 +130,21 @@
 fun facts_of (Facts {facts, ...}) = facts;
 
 val space_of = #1 o facts_of;
-val lookup = Symtab.lookup o #2 o facts_of;
-val dest = NameSpace.dest_table o facts_of;
-val extern = NameSpace.extern_table o facts_of;
+val table_of = #2 o facts_of;
+
+fun lookup context facts name =
+  (case Symtab.lookup (table_of facts) name of
+    NONE => NONE
+  | SOME (Static ths, _) => SOME ths
+  | SOME (Dynamic f, _) => SOME (f context));
+
+fun dest facts =
+  Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
+
+fun extern facts =
+  dest facts
+  |> map (apfst (NameSpace.extern (space_of facts)))
+  |> sort_wrt #1;
 
 
 (* indexed props *)
@@ -139,16 +155,28 @@
 fun could_unify (Facts {props, ...}) = Net.unify_term props;
 
 
-(* build facts *)
+(* merge facts *)
 
-val empty = make_facts NameSpace.empty_table Net.empty;
+fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
 
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
-    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
+    (* FIXME authentic version
+    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
+      handle Symtab.DUP dup => err_dup_fact dup; *)
+    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   in make_facts facts' props' end;
 
+
+(* static entries *)
+
+fun del name (Facts {facts = (space, tab), props}) =
+  let
+    val space' = NameSpace.hide true name space handle ERROR _ => space;
+    val tab' = Symtab.delete_safe name tab;
+  in make_facts (space', tab') props end;
+
 fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
   let
     val facts' =
@@ -157,7 +185,8 @@
         let
           val (space, tab) = facts;
           val space' = NameSpace.declare naming name space;
-          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
+          val entry = (name, (Static ths, serial ()));
+          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
             handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
               Position.str_of (Position.thread_data ())); tab);
         in (space', tab') end;
@@ -169,10 +198,15 @@
 val add_global = add false false;
 val add_local = add true;
 
-fun del name (Facts {facts = (space, tab), props}) =
+
+(* dynamic entries *)
+
+fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
   let
-    val space' = NameSpace.hide true name space handle ERROR _ => space;
-    val tab' = Symtab.delete_safe name tab;
+    val space' = NameSpace.declare naming name space;
+    val entry = (name, (Dynamic f, serial ()));
+    val tab' = Symtab.update_new entry tab
+      handle Symtab.DUP dup => err_dup_fact dup;
   in make_facts (space', tab') props end;
 
 end;

--- a/src/Pure/pure_thy.ML	Tue Mar 25 19:39:58 2008 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 25 19:39:59 2008 +0100
@@ -58,6 +58,7 @@
   val smart_store_thms_open: (bstring * thm list) -> thm list
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
+  val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
   val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
   val note: string -> string * thm -> theory -> thm * theory
@@ -180,7 +181,7 @@
   let
     val facts = all_facts_of thy;
     val name = NameSpace.intern (Facts.space_of facts) xname;
-  in Option.map (pair name) (Facts.lookup facts name) end;
+  in Option.map (pair name) (Facts.lookup (Context.Theory thy) facts name) end;
 
 fun show_result NONE = "none"
   | show_result (SOME (name, _)) = quote name;
@@ -265,6 +266,17 @@
   burrow_fact (name_thms true official name) fact;
 
 
+(* add_thms_dynamic *)
+
+fun add_thms_dynamic (bname, f) thy = CRITICAL (fn () =>
+  let
+    val name = Sign.full_name thy bname;
+    val r as ref (Thms {theorems, all_facts}) = get_theorems_ref thy;
+    val all_facts' = Facts.add_dynamic (Sign.naming_of thy) (name, f) all_facts;
+    val _ = r := make_thms theorems all_facts';
+  in thy end);
+
+
 (* enter_thms *)
 
 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
@@ -544,3 +556,4 @@
 
 structure BasicPureThy: BASIC_PURE_THY = PureThy;
 open BasicPureThy;
+