equal
deleted
inserted
replaced
24 val intern: T -> xstring -> string |
24 val intern: T -> xstring -> string |
25 val extern: T -> string -> xstring |
25 val extern: T -> string -> xstring |
26 val lookup: Context.generic -> T -> string -> thm list option |
26 val lookup: Context.generic -> T -> string -> thm list option |
27 val defined: T -> string -> bool |
27 val defined: T -> string -> bool |
28 val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a |
28 val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a |
29 val dest_static: T -> (string * thm list) list |
29 val dest_static: T list -> T -> (string * thm list) list |
30 val extern_static: T -> (xstring * thm list) list |
30 val extern_static: T list -> T -> (xstring * thm list) list |
31 val props: T -> thm list |
31 val props: T -> thm list |
32 val could_unify: T -> term -> thm list |
32 val could_unify: T -> term -> thm list |
33 val merge: T * T -> T |
33 val merge: T * T -> T |
34 val add_global: NameSpace.naming -> string * thm list -> T -> T |
34 val add_global: NameSpace.naming -> string * thm list -> T -> T |
35 val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T |
35 val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T |
147 | SOME (Static ths, _) => SOME ths |
147 | SOME (Static ths, _) => SOME ths |
148 | SOME (Dynamic f, _) => SOME (f context)); |
148 | SOME (Dynamic f, _) => SOME (f context)); |
149 |
149 |
150 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of; |
150 fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of; |
151 |
151 |
152 fun dest_static facts = sort_wrt #1 (fold_static cons facts []); |
152 |
153 fun extern_static facts = |
153 (* content difference *) |
154 sort_wrt #1 (fold_static (fn (name, ths) => cons (extern facts name, ths)) facts []); |
154 |
|
155 fun diff_table prev_facts facts = |
|
156 fold_static (fn (name, ths) => |
|
157 if exists (fn prev => defined prev name) prev_facts then I |
|
158 else cons (name, ths)) facts []; |
|
159 |
|
160 fun dest_static prev_facts facts = |
|
161 sort_wrt #1 (diff_table prev_facts facts); |
|
162 |
|
163 fun extern_static prev_facts facts = |
|
164 sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts))); |
155 |
165 |
156 |
166 |
157 (* indexed props *) |
167 (* indexed props *) |
158 |
168 |
159 val prop_ord = Term.term_ord o pairself Thm.full_prop_of; |
169 val prop_ord = Term.term_ord o pairself Thm.full_prop_of; |
164 |
174 |
165 (* merge facts *) |
175 (* merge facts *) |
166 |
176 |
167 fun err_dup_fact name = error ("Duplicate fact " ^ quote name); |
177 fun err_dup_fact name = error ("Duplicate fact " ^ quote name); |
168 |
178 |
|
179 (* FIXME stamp identity! *) |
169 fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2)) |
180 fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2)) |
170 | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2; |
181 | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2; |
171 |
182 |
172 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) = |
183 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) = |
173 let |
184 let |