180 (* instantiate TFrees *) |
180 (* instantiate TFrees *) |
181 |
181 |
182 fun tinst_tab_type tinst T = if Symtab.is_empty tinst |
182 fun tinst_tab_type tinst T = if Symtab.is_empty tinst |
183 then T |
183 then T |
184 else Term.map_type_tfree |
184 else Term.map_type_tfree |
185 (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T; |
185 (fn (v as (x, _)) => getOpt (Symtab.lookup tinst x, (TFree v))) T; |
186 |
186 |
187 fun tinst_tab_term tinst t = if Symtab.is_empty tinst |
187 fun tinst_tab_term tinst t = if Symtab.is_empty tinst |
188 then t |
188 then t |
189 else Term.map_term_types (tinst_tab_type tinst) t; |
189 else Term.map_term_types (tinst_tab_type tinst) t; |
190 |
190 |
213 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst |
213 fun inst_tab_term (inst, tinst) = if Symtab.is_empty inst |
214 then tinst_tab_term tinst |
214 then tinst_tab_term tinst |
215 else (* instantiate terms and types simultaneously *) |
215 else (* instantiate terms and types simultaneously *) |
216 let |
216 let |
217 fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) |
217 fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T) |
218 | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of |
218 | instf (Free (x, T)) = (case Symtab.lookup inst x of |
219 NONE => Free (x, tinst_tab_type tinst T) |
219 NONE => Free (x, tinst_tab_type tinst T) |
220 | SOME t => t) |
220 | SOME t => t) |
221 | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) |
221 | instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T) |
222 | instf (b as Bound _) = b |
222 | instf (b as Bound _) = b |
223 | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) |
223 | instf (Abs (x, T, t)) = Abs (x, tinst_tab_type tinst T, instf t) |
334 in (case subs of |
334 in (case subs of |
335 [] => let |
335 [] => let |
336 val sups = |
336 val sups = |
337 List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); |
337 List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); |
338 val sups' = map (apfst untermify) sups |
338 val sups' = map (apfst untermify) sups |
339 in (Termtab.curried_update (t, (attn, [])) regs, sups') end |
339 in (Termtab.update (t, (attn, [])) regs, sups') end |
340 | _ => (regs, [])) |
340 | _ => (regs, [])) |
341 end; |
341 end; |
342 |
342 |
343 (* add witness theorem to registration, |
343 (* add witness theorem to registration, |
344 only if instantiation is exact, otherwise exception Option raised *) |
344 only if instantiation is exact, otherwise exception Option raised *) |
345 fun add_witness ts thm regs = |
345 fun add_witness ts thm regs = |
346 let |
346 let |
347 val t = termify ts; |
347 val t = termify ts; |
348 val (x, thms) = valOf (Termtab.curried_lookup regs t); |
348 val (x, thms) = valOf (Termtab.lookup regs t); |
349 in |
349 in |
350 Termtab.curried_update (t, (x, thm::thms)) regs |
350 Termtab.update (t, (x, thm::thms)) regs |
351 end; |
351 end; |
352 end; |
352 end; |
353 |
353 |
354 |
354 |
355 (** theory data **) |
355 (** theory data **) |
410 thy |> GlobalLocalesData.map (fn (space, locs, regs) => |
410 thy |> GlobalLocalesData.map (fn (space, locs, regs) => |
411 (Sign.declare_name thy name space, locs, regs)); |
411 (Sign.declare_name thy name space, locs, regs)); |
412 |
412 |
413 fun put_locale name loc = |
413 fun put_locale name loc = |
414 GlobalLocalesData.map (fn (space, locs, regs) => |
414 GlobalLocalesData.map (fn (space, locs, regs) => |
415 (space, Symtab.curried_update (name, loc) locs, regs)); |
415 (space, Symtab.update (name, loc) locs, regs)); |
416 |
416 |
417 fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name; |
417 fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name; |
418 |
418 |
419 fun the_locale thy name = |
419 fun the_locale thy name = |
420 (case get_locale thy name of |
420 (case get_locale thy name of |
421 SOME loc => loc |
421 SOME loc => loc |
422 | NONE => error ("Unknown locale " ^ quote name)); |
422 | NONE => error ("Unknown locale " ^ quote name)); |
429 Thms of registrations are never varified. *) |
429 Thms of registrations are never varified. *) |
430 |
430 |
431 (* retrieve registration from theory or context *) |
431 (* retrieve registration from theory or context *) |
432 |
432 |
433 fun gen_get_registrations get thy_ctxt name = |
433 fun gen_get_registrations get thy_ctxt name = |
434 case Symtab.curried_lookup (get thy_ctxt) name of |
434 case Symtab.lookup (get thy_ctxt) name of |
435 NONE => [] |
435 NONE => [] |
436 | SOME reg => Registrations.dest reg; |
436 | SOME reg => Registrations.dest reg; |
437 |
437 |
438 val get_global_registrations = |
438 val get_global_registrations = |
439 gen_get_registrations (#3 o GlobalLocalesData.get); |
439 gen_get_registrations (#3 o GlobalLocalesData.get); |
440 val get_local_registrations = |
440 val get_local_registrations = |
441 gen_get_registrations LocalLocalesData.get; |
441 gen_get_registrations LocalLocalesData.get; |
442 |
442 |
443 fun gen_get_registration get thy_of thy_ctxt (name, ps) = |
443 fun gen_get_registration get thy_of thy_ctxt (name, ps) = |
444 case Symtab.curried_lookup (get thy_ctxt) name of |
444 case Symtab.lookup (get thy_ctxt) name of |
445 NONE => NONE |
445 NONE => NONE |
446 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); |
446 | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps); |
447 |
447 |
448 val get_global_registration = |
448 val get_global_registration = |
449 gen_get_registration (#3 o GlobalLocalesData.get) I; |
449 gen_get_registration (#3 o GlobalLocalesData.get) I; |
464 |
464 |
465 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = |
465 fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt = |
466 map_data (fn regs => |
466 map_data (fn regs => |
467 let |
467 let |
468 val thy = thy_of thy_ctxt; |
468 val thy = thy_of thy_ctxt; |
469 val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty); |
469 val reg = getOpt (Symtab.lookup regs name, Registrations.empty); |
470 val (reg', sups) = Registrations.insert thy (ps, attn) reg; |
470 val (reg', sups) = Registrations.insert thy (ps, attn) reg; |
471 val _ = if not (null sups) then warning |
471 val _ = if not (null sups) then warning |
472 ("Subsumed interpretation(s) of locale " ^ |
472 ("Subsumed interpretation(s) of locale " ^ |
473 quote (extern thy name) ^ |
473 quote (extern thy name) ^ |
474 "\nby interpretation(s) with the following prefix(es):\n" ^ |
474 "\nby interpretation(s) with the following prefix(es):\n" ^ |
475 commas_quote (map (fn (_, ((s, _), _)) => s) sups)) |
475 commas_quote (map (fn (_, ((s, _), _)) => s) sups)) |
476 else (); |
476 else (); |
477 in Symtab.curried_update (name, reg') regs end) thy_ctxt; |
477 in Symtab.update (name, reg') regs end) thy_ctxt; |
478 |
478 |
479 val put_global_registration = |
479 val put_global_registration = |
480 gen_put_registration (fn f => |
480 gen_put_registration (fn f => |
481 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; |
481 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; |
482 val put_local_registration = |
482 val put_local_registration = |
557 else Pretty.block ((prt_attn attn @ |
557 else Pretty.block ((prt_attn attn @ |
558 [Pretty.str ":", Pretty.brk 1, prt_inst ts])); |
558 [Pretty.str ":", Pretty.brk 1, prt_inst ts])); |
559 |
559 |
560 val loc_int = intern thy loc; |
560 val loc_int = intern thy loc; |
561 val regs = get_regs thy_ctxt; |
561 val regs = get_regs thy_ctxt; |
562 val loc_regs = Symtab.curried_lookup regs loc_int; |
562 val loc_regs = Symtab.lookup regs loc_int; |
563 in |
563 in |
564 (case loc_regs of |
564 (case loc_regs of |
565 NONE => Pretty.str ("no interpretations in " ^ msg) |
565 NONE => Pretty.str ("no interpretations in " ^ msg) |
566 | SOME r => let |
566 | SOME r => let |
567 val r' = Registrations.dest r; |
567 val r' = Registrations.dest r; |
769 |
769 |
770 fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)); |
770 fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss)); |
771 fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); |
771 fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss)); |
772 fun params_syn_of syn elemss = |
772 fun params_syn_of syn elemss = |
773 gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |> |
773 gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |> |
774 map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x)))); |
774 map (apfst (fn x => (x, valOf (Symtab.lookup syn x)))); |
775 |
775 |
776 |
776 |
777 (* CB: param_types has the following type: |
777 (* CB: param_types has the following type: |
778 ('a * 'b option) list -> ('a * 'b) list *) |
778 ('a * 'b option) list -> ('a * 'b) list *) |
779 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
779 fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
1015 fun eval syn ((name, xs), axs) = |
1015 fun eval syn ((name, xs), axs) = |
1016 let |
1016 let |
1017 val {params = (ps, qs), elems, ...} = the_locale thy name; |
1017 val {params = (ps, qs), elems, ...} = the_locale thy name; |
1018 val ps' = map (apsnd SOME o #1) ps; |
1018 val ps' = map (apsnd SOME o #1) ps; |
1019 val ren = map #1 ps' ~~ |
1019 val ren = map #1 ps' ~~ |
1020 map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs; |
1020 map (fn x => (x, valOf (Symtab.lookup syn x))) xs; |
1021 val (params', elems') = |
1021 val (params', elems') = |
1022 if null ren then ((ps', qs), map #1 elems) |
1022 if null ren then ((ps', qs), map #1 elems) |
1023 else ((map (apfst (rename ren)) ps', map (rename ren) qs), |
1023 else ((map (apfst (rename ren)) ps', map (rename ren) qs), |
1024 map (rename_elem ren o #1) elems); |
1024 map (rename_elem ren o #1) elems); |
1025 val elems'' = map (rename_facts (space_implode "_" xs)) elems'; |
1025 val elems'' = map (rename_facts (space_implode "_" xs)) elems'; |
1752 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; |
1752 val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; |
1753 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) |
1753 val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) |
1754 |> Symtab.make; |
1754 |> Symtab.make; |
1755 (* replace parameter names in ids by instantiations *) |
1755 (* replace parameter names in ids by instantiations *) |
1756 val vinst = Symtab.make (parms ~~ vts); |
1756 val vinst = Symtab.make (parms ~~ vts); |
1757 fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps; |
1757 fun vinst_names ps = map (the o Symtab.lookup vinst) ps; |
1758 val inst = Symtab.make (parms ~~ ts); |
1758 val inst = Symtab.make (parms ~~ ts); |
1759 val ids' = map (apsnd vinst_names) ids; |
1759 val ids' = map (apsnd vinst_names) ids; |
1760 val wits = List.concat (map (snd o valOf o get_global_registration thy) ids'); |
1760 val wits = List.concat (map (snd o valOf o get_global_registration thy) ids'); |
1761 in ((inst, tinst), wits) end; |
1761 in ((inst, tinst), wits) end; |
1762 |
1762 |
2026 |> note_thmss_qualified "" name facts' |> #1 |
2026 |> note_thmss_qualified "" name facts' |> #1 |
2027 |> declare_locale name |
2027 |> declare_locale name |
2028 |> put_locale name {predicate = predicate, import = import, |
2028 |> put_locale name {predicate = predicate, import = import, |
2029 elems = map (fn e => (e, stamp ())) elems', |
2029 elems = map (fn e => (e, stamp ())) elems', |
2030 params = (params_of elemss' |> |
2030 params = (params_of elemss' |> |
2031 map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)), |
2031 map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), map #1 (params_of body_elemss)), |
2032 regs = []} |
2032 regs = []} |
2033 |> pair (elems', body_ctxt) |
2033 |> pair (elems', body_ctxt) |
2034 end; |
2034 end; |
2035 |
2035 |
2036 in |
2036 in |
2262 let |
2262 let |
2263 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of |
2263 val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of |
2264 NONE => error ("Instance missing for parameter " ^ quote p) |
2264 NONE => error ("Instance missing for parameter " ^ quote p) |
2265 | SOME (Free (_, T), t) => (t, T); |
2265 | SOME (Free (_, T), t) => (t, T); |
2266 val d = inst_tab_term (inst, tinst) t; |
2266 val d = inst_tab_term (inst, tinst) t; |
2267 in (Symtab.curried_update_new (p, d) inst, tinst) end; |
2267 in (Symtab.update_new (p, d) inst, tinst) end; |
2268 val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given); |
2268 val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given); |
2269 (* Note: inst and tinst contain no vars. *) |
2269 (* Note: inst and tinst contain no vars. *) |
2270 |
2270 |
2271 (** compute proof obligations **) |
2271 (** compute proof obligations **) |
2272 |
2272 |