181 structure Registrations : |
181 structure Registrations : |
182 sig |
182 sig |
183 type T |
183 type T |
184 val empty: T |
184 val empty: T |
185 val join: T * T -> T |
185 val join: T * T -> T |
186 val dest: T -> (term list * ((string * Attrib.src list) * Element.witness list)) list |
186 val dest: theory -> T -> |
|
187 (term list * ((string * Attrib.src list) * Element.witness list)) list |
187 val lookup: theory -> T * term list -> |
188 val lookup: theory -> T * term list -> |
188 ((string * Attrib.src list) * Element.witness list) option |
189 ((string * Attrib.src list) * Element.witness list) option |
189 val insert: theory -> term list * (string * Attrib.src list) -> T -> |
190 val insert: theory -> term list * (string * Attrib.src list) -> T -> |
190 T * (term list * ((string * Attrib.src list) * Element.witness list)) list |
191 T * (term list * ((string * Attrib.src list) * Element.witness list)) list |
191 val add_witness: term list -> Element.witness -> T -> T |
192 val add_witness: term list -> Element.witness -> T -> T |
192 end = |
193 end = |
193 struct |
194 struct |
194 (* a registration consists of theorems instantiating locale assumptions |
195 (* a registration consists of theorems (actually, witnesses) instantiating locale |
195 and prefix and attributes, indexed by parameter instantiation *) |
196 assumptions and prefix and attributes, indexed by parameter instantiation *) |
196 type T = ((string * Attrib.src list) * Element.witness list) Termtab.table; |
197 type T = ((string * Attrib.src list) * Element.witness list) Termtab.table; |
197 |
198 |
198 val empty = Termtab.empty; |
199 val empty = Termtab.empty; |
199 |
200 |
200 (* term list represented as single term, for simultaneous matching *) |
201 (* term list represented as single term, for simultaneous matching *) |
207 |
208 |
208 (* joining of registrations: prefix and attributes of left theory, |
209 (* joining of registrations: prefix and attributes of left theory, |
209 thms are equal, no attempt to subsumption testing *) |
210 thms are equal, no attempt to subsumption testing *) |
210 fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2); |
211 fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2); |
211 |
212 |
212 fun dest regs = map (apfst untermify) (Termtab.dest regs); |
213 fun dest_transfer thy regs = |
|
214 Termtab.dest regs |> map (apsnd (apsnd (map (Element.transfer_witness thy)))); |
|
215 |
|
216 fun dest thy regs = dest_transfer thy regs |> map (apfst untermify); |
213 |
217 |
214 (* registrations that subsume t *) |
218 (* registrations that subsume t *) |
215 fun subsumers thy t regs = |
219 fun subsumers thy t regs = |
216 filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); |
220 filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); |
217 |
221 |
218 (* look up registration, pick one that subsumes the query *) |
222 (* look up registration, pick one that subsumes the query *) |
219 fun lookup thy (regs, ts) = |
223 fun lookup thy (regs, ts) = |
220 let |
224 let |
221 val t = termify ts; |
225 val t = termify ts; |
236 end) |
240 end) |
237 end; |
241 end; |
238 |
242 |
239 (* add registration if not subsumed by ones already present, |
243 (* add registration if not subsumed by ones already present, |
240 additionally returns registrations that are strictly subsumed *) |
244 additionally returns registrations that are strictly subsumed *) |
241 fun insert sign (ts, attn) regs = |
245 fun insert thy (ts, attn) regs = |
242 let |
246 let |
243 val t = termify ts; |
247 val t = termify ts; |
244 val subs = subsumers sign t regs ; |
248 val subs = subsumers thy t regs ; |
245 in (case subs of |
249 in (case subs of |
246 [] => let |
250 [] => let |
247 val sups = |
251 val sups = |
248 filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); |
252 filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); |
249 val sups' = map (apfst untermify) sups |
253 val sups' = map (apfst untermify) sups |
250 in (Termtab.update (t, (attn, [])) regs, sups') end |
254 in (Termtab.update (t, (attn, [])) regs, sups') end |
251 | _ => (regs, [])) |
255 | _ => (regs, [])) |
252 end; |
256 end; |
253 |
257 |
355 Ids of local registrations are not. |
359 Ids of local registrations are not. |
356 Thms of registrations are never varified. *) |
360 Thms of registrations are never varified. *) |
357 |
361 |
358 (* retrieve registration from theory or context *) |
362 (* retrieve registration from theory or context *) |
359 |
363 |
360 fun gen_get_registrations get thy_ctxt name = |
364 fun gen_get_registrations get thy_of thy_ctxt name = |
361 case Symtab.lookup (get thy_ctxt) name of |
365 case Symtab.lookup (get thy_ctxt) name of |
362 NONE => [] |
366 NONE => [] |
363 | SOME reg => Registrations.dest reg; |
367 | SOME reg => Registrations.dest (thy_of thy_ctxt) reg; |
364 |
368 |
365 val get_global_registrations = |
369 val get_global_registrations = |
366 gen_get_registrations (#3 o GlobalLocalesData.get); |
370 gen_get_registrations (#3 o GlobalLocalesData.get) I; |
367 val get_local_registrations = |
371 val get_local_registrations = |
368 gen_get_registrations LocalLocalesData.get; |
372 gen_get_registrations LocalLocalesData.get ProofContext.theory_of; |
369 |
373 |
370 fun gen_get_registration get thy_of thy_ctxt (name, ps) = |
374 fun gen_get_registration get thy_of thy_ctxt (name, ps) = |
371 case Symtab.lookup (get thy_ctxt) name of |
375 case Symtab.lookup (get thy_ctxt) name of |
372 NONE => NONE |
376 NONE => NONE |
373 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); |
377 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); |
464 val loc_regs = Symtab.lookup regs loc_int; |
468 val loc_regs = Symtab.lookup regs loc_int; |
465 in |
469 in |
466 (case loc_regs of |
470 (case loc_regs of |
467 NONE => Pretty.str ("no interpretations in " ^ msg) |
471 NONE => Pretty.str ("no interpretations in " ^ msg) |
468 | SOME r => let |
472 | SOME r => let |
469 val r' = Registrations.dest r; |
473 val r' = Registrations.dest thy r; |
470 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; |
474 val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r'; |
471 in Pretty.big_list ("interpretations in " ^ msg ^ ":") |
475 in Pretty.big_list ("interpretations in " ^ msg ^ ":") |
472 (map prt_reg r'') |
476 (map prt_reg r'') |
473 end) |
477 end) |
474 |> Pretty.writeln |
478 |> Pretty.writeln |
742 val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps; |
746 val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps; |
743 (* dummy syntax, since required by rename *) |
747 (* dummy syntax, since required by rename *) |
744 val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps'); |
748 val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps'); |
745 val [env] = unify_parms ctxt ps [map (apsnd SOME) ps'']; |
749 val [env] = unify_parms ctxt ps [map (apsnd SOME) ps'']; |
746 (* propagate parameter types, to keep them consistent *) |
750 (* propagate parameter types, to keep them consistent *) |
747 val regs' = map (fn ((name, ps), ths) => |
751 val regs' = map (fn ((name, ps), wits) => |
748 ((name, map (Element.rename ren) ps), ths)) regs; |
752 ((name, map (Element.rename ren) ps), |
|
753 map (Element.transfer_witness thy) wits)) regs; |
749 val new_regs = gen_rems (eq_fst (op =)) (regs', ids); |
754 val new_regs = gen_rems (eq_fst (op =)) (regs', ids); |
750 val new_ids = map fst new_regs; |
755 val new_ids = map fst new_regs; |
751 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; |
756 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids; |
752 |
757 |
753 val new_ths = new_regs |> map (#2 #> map |
758 val new_ths = new_regs |> map (#2 #> map |
1938 |
1943 |
1939 fun all_witnesses ctxt = |
1944 fun all_witnesses ctxt = |
1940 let |
1945 let |
1941 val thy = ProofContext.theory_of ctxt; |
1946 val thy = ProofContext.theory_of ctxt; |
1942 fun get registrations = Symtab.fold (fn (_, regs) => fn thms => |
1947 fun get registrations = Symtab.fold (fn (_, regs) => fn thms => |
1943 (Registrations.dest regs |> map (fn (_, (_, wits)) => |
1948 (Registrations.dest thy regs |> map (fn (_, (_, wits)) => |
1944 map Element.conclude_witness wits) |> flat) @ thms) |
1949 map Element.conclude_witness wits) |> flat) @ thms) |
1945 registrations []; |
1950 registrations []; |
1946 val globals = get (#3 (GlobalLocalesData.get thy)); |
1951 val globals = get (#3 (GlobalLocalesData.get thy)); |
1947 val locals = get (LocalLocalesData.get ctxt); |
1952 val locals = get (LocalLocalesData.get ctxt); |
1948 in globals @ locals end; |
1953 in globals @ locals end; |