# HG changeset patch # User wenzelm # Date 1206470399 -3600 # Node ID 42febbed54605bec212a4e9e282eef8df0c8d5c6 # Parent 748b263f0e404cd44c4dd34bf7b357af8a05d1a6 support dynamic facts; diff -r 748b263f0e40 -r 42febbed5460 src/Pure/Isar/proof_context.ML --- 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; diff -r 748b263f0e40 -r 42febbed5460 src/Pure/facts.ML --- 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; diff -r 748b263f0e40 -r 42febbed5460 src/Pure/pure_thy.ML --- 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; +