src/Pure/facts.ML
changeset 26393 42febbed5460
parent 26366 5c089f4219c2
child 26654 1f711934f221
     1.1 --- a/src/Pure/facts.ML	Tue Mar 25 19:39:58 2008 +0100
     1.2 +++ b/src/Pure/facts.ML	Tue Mar 25 19:39:59 2008 +0100
     1.3 @@ -20,17 +20,18 @@
     1.4    val select: ref -> thm list -> thm list
     1.5    val selections: string * thm list -> (ref * thm) list
     1.6    type T
     1.7 +  val empty: T
     1.8    val space_of: T -> NameSpace.T
     1.9 -  val lookup: T -> string -> thm list option
    1.10 +  val lookup: Context.generic -> T -> string -> thm list option
    1.11    val dest: T -> (string * thm list) list
    1.12    val extern: T -> (xstring * thm list) list
    1.13    val props: T -> thm list
    1.14    val could_unify: T -> term -> thm list
    1.15 -  val empty: T
    1.16    val merge: T * T -> T
    1.17 +  val del: string -> T -> T
    1.18    val add_global: NameSpace.naming -> string * thm list -> T -> T
    1.19    val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    1.20 -  val del: string -> T -> T
    1.21 +  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
    1.22  end;
    1.23  
    1.24  structure Facts: FACTS =
    1.25 @@ -112,13 +113,16 @@
    1.26  
    1.27  (** fact environment **)
    1.28  
    1.29 -(* datatype T *)
    1.30 +(* datatypes *)
    1.31 +
    1.32 +datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
    1.33  
    1.34  datatype T = Facts of
    1.35 - {facts: thm list NameSpace.table,
    1.36 + {facts: (fact * serial) NameSpace.table,
    1.37    props: thm Net.net};
    1.38  
    1.39  fun make_facts facts props = Facts {facts = facts, props = props};
    1.40 +val empty = make_facts NameSpace.empty_table Net.empty;
    1.41  
    1.42  
    1.43  (* named facts *)
    1.44 @@ -126,9 +130,21 @@
    1.45  fun facts_of (Facts {facts, ...}) = facts;
    1.46  
    1.47  val space_of = #1 o facts_of;
    1.48 -val lookup = Symtab.lookup o #2 o facts_of;
    1.49 -val dest = NameSpace.dest_table o facts_of;
    1.50 -val extern = NameSpace.extern_table o facts_of;
    1.51 +val table_of = #2 o facts_of;
    1.52 +
    1.53 +fun lookup context facts name =
    1.54 +  (case Symtab.lookup (table_of facts) name of
    1.55 +    NONE => NONE
    1.56 +  | SOME (Static ths, _) => SOME ths
    1.57 +  | SOME (Dynamic f, _) => SOME (f context));
    1.58 +
    1.59 +fun dest facts =
    1.60 +  Symtab.fold (fn (name, (Static ths, _)) => cons (name, ths) | _ => I) (table_of facts) [];
    1.61 +
    1.62 +fun extern facts =
    1.63 +  dest facts
    1.64 +  |> map (apfst (NameSpace.extern (space_of facts)))
    1.65 +  |> sort_wrt #1;
    1.66  
    1.67  
    1.68  (* indexed props *)
    1.69 @@ -139,16 +155,28 @@
    1.70  fun could_unify (Facts {props, ...}) = Net.unify_term props;
    1.71  
    1.72  
    1.73 -(* build facts *)
    1.74 +(* merge facts *)
    1.75  
    1.76 -val empty = make_facts NameSpace.empty_table Net.empty;
    1.77 +fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
    1.78  
    1.79  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    1.80    let
    1.81 -    val facts' = NameSpace.merge_tables (K true) (facts1, facts2);
    1.82 +    (* FIXME authentic version
    1.83 +    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
    1.84 +      handle Symtab.DUP dup => err_dup_fact dup; *)
    1.85 +    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
    1.86      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.87    in make_facts facts' props' end;
    1.88  
    1.89 +
    1.90 +(* static entries *)
    1.91 +
    1.92 +fun del name (Facts {facts = (space, tab), props}) =
    1.93 +  let
    1.94 +    val space' = NameSpace.hide true name space handle ERROR _ => space;
    1.95 +    val tab' = Symtab.delete_safe name tab;
    1.96 +  in make_facts (space', tab') props end;
    1.97 +
    1.98  fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
    1.99    let
   1.100      val facts' =
   1.101 @@ -157,7 +185,8 @@
   1.102          let
   1.103            val (space, tab) = facts;
   1.104            val space' = NameSpace.declare naming name space;
   1.105 -          val tab' = (if permissive then Symtab.update else Symtab.update_new) (name, ths) tab
   1.106 +          val entry = (name, (Static ths, serial ()));
   1.107 +          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   1.108              handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
   1.109                Position.str_of (Position.thread_data ())); tab);
   1.110          in (space', tab') end;
   1.111 @@ -169,10 +198,15 @@
   1.112  val add_global = add false false;
   1.113  val add_local = add true;
   1.114  
   1.115 -fun del name (Facts {facts = (space, tab), props}) =
   1.116 +
   1.117 +(* dynamic entries *)
   1.118 +
   1.119 +fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
   1.120    let
   1.121 -    val space' = NameSpace.hide true name space handle ERROR _ => space;
   1.122 -    val tab' = Symtab.delete_safe name tab;
   1.123 +    val space' = NameSpace.declare naming name space;
   1.124 +    val entry = (name, (Dynamic f, serial ()));
   1.125 +    val tab' = Symtab.update_new entry tab
   1.126 +      handle Symtab.DUP dup => err_dup_fact dup;
   1.127    in make_facts (space', tab') props end;
   1.128  
   1.129  end;