86 |
86 |
87 (* Locale interpretation *) |
87 (* Locale interpretation *) |
88 val prep_global_registration: |
88 val prep_global_registration: |
89 string * Attrib.src list -> expr -> string option list -> theory -> |
89 string * Attrib.src list -> expr -> string option list -> theory -> |
90 theory * ((string * term list) * term list) list * (theory -> theory) |
90 theory * ((string * term list) * term list) list * (theory -> theory) |
|
91 (* |
|
92 val prep_registration_in_locale: |
|
93 string -> expr -> string option list -> theory -> |
|
94 *) |
91 val prep_local_registration: |
95 val prep_local_registration: |
92 string * Attrib.src list -> expr -> string option list -> context -> |
96 string * Attrib.src list -> expr -> string option list -> context -> |
93 context * ((string * term list) * term list) list * (context -> context) |
97 context * ((string * term list) * term list) list * (context -> context) |
94 val add_global_witness: |
98 val add_global_witness: |
95 string * term list -> thm -> theory -> theory |
99 string * term list -> thm -> theory -> theory |
124 type element = (string, string, thmref) elem; |
128 type element = (string, string, thmref) elem; |
125 type element_i = (typ, term, thm list) elem; |
129 type element_i = (typ, term, thm list) elem; |
126 |
130 |
127 type locale = |
131 type locale = |
128 {predicate: cterm list * thm list, |
132 {predicate: cterm list * thm list, |
129 (* CB: For old-style locales with "(open)" this entry is ([], []). |
133 (* CB: For locales with "(open)" this entry is ([], []). |
130 For new-style locales, which declare predicates, if the locale declares |
134 For new-style locales, which declare predicates, if the locale declares |
131 no predicates, this is also ([], []). |
135 no predicates, this is also ([], []). |
132 If the locale declares predicates, the record field is |
136 If the locale declares predicates, the record field is |
133 ([statement], axioms), where statement is the locale predicate applied |
137 ([statement], axioms), where statement is the locale predicate applied |
134 to the (assumed) locale parameters. Axioms contains the projections |
138 to the (assumed) locale parameters. Axioms contains the projections |
135 from the locale predicate to the normalised assumptions of the locale |
139 from the locale predicate to the normalised assumptions of the locale |
136 (cf. [1], normalisation of locale expressions.) |
140 (cf. [1], normalisation of locale expressions.) |
137 *) |
141 *) |
138 import: expr, (*dynamic import*) |
142 import: expr, (*dynamic import*) |
139 elems: (element_i * stamp) list, (*static content*) |
143 elems: (element_i * stamp) list, (*static content*) |
140 params: ((string * typ) * mixfix option) list * string list} |
144 params: ((string * typ) * mixfix option) list * string list, |
141 (*all/local params*) |
145 (*all/local params*) |
|
146 regs: ((string * string list) * thm list) list} |
|
147 (* Registrations: indentifiers and witness theorems of locales interpreted |
|
148 in the locale. |
|
149 *) |
142 |
150 |
143 |
151 |
144 (* CB: an internal (Int) locale element was either imported or included, |
152 (* CB: an internal (Int) locale element was either imported or included, |
145 an external (Ext) element appears directly in the locale text. *) |
153 an external (Ext) element appears directly in the locale text. *) |
146 |
154 |
335 |
344 |
336 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); |
345 val empty = (NameSpace.empty, Symtab.empty, Symtab.empty); |
337 val copy = I; |
346 val copy = I; |
338 val extend = I; |
347 val extend = I; |
339 |
348 |
340 fun join_locs _ ({predicate, import, elems, params}: locale, |
349 fun join_locs _ ({predicate, import, elems, params, regs}: locale, |
341 {elems = elems', ...}: locale) = |
350 {elems = elems', regs = regs', ...}: locale) = |
342 SOME {predicate = predicate, import = import, |
351 SOME {predicate = predicate, import = import, |
343 elems = gen_merge_lists eq_snd elems elems', |
352 elems = gen_merge_lists eq_snd elems elems', |
344 params = params}; |
353 params = params, |
|
354 regs = merge_alists regs regs'}; |
345 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = |
355 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) = |
346 (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), |
356 (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2), |
347 Symtab.join (K (SOME o Registrations.join)) (regs1, regs2)); |
357 Symtab.join (K (SOME o Registrations.join)) (regs1, regs2)); |
348 |
358 |
349 fun print _ (space, locs, _) = |
359 fun print _ (space, locs, _) = |
450 gen_put_registration (fn f => |
460 gen_put_registration (fn f => |
451 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; |
461 GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I; |
452 val put_local_registration = |
462 val put_local_registration = |
453 gen_put_registration LocalLocalesData.map ProofContext.theory_of; |
463 gen_put_registration LocalLocalesData.map ProofContext.theory_of; |
454 |
464 |
455 (* TODO: needed? *) |
|
456 (* |
|
457 fun smart_put_registration id attn ctxt = |
|
458 (* ignore registration if already present in theory *) |
|
459 let |
|
460 val thy = ProofContext.theory_of ctxt; |
|
461 in case get_global_registration thy id of |
|
462 NONE => put_local_registration id attn ctxt |
|
463 | SOME _ => ctxt |
|
464 end; |
|
465 *) |
|
466 |
465 |
467 (* add witness theorem to registration in theory or context, |
466 (* add witness theorem to registration in theory or context, |
468 ignored if registration not present *) |
467 ignored if registration not present *) |
469 |
468 |
470 fun gen_add_witness map (name, ps) thm = |
469 fun gen_add_witness map (name, ps) thm = |
811 fun inst ((((name, ps), axs), elems), env) = |
810 fun inst ((((name, ps), axs), elems), env) = |
812 (((name, map (apsnd (Option.map (inst_type env))) ps), |
811 (((name, map (apsnd (Option.map (inst_type env))) ps), |
813 map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); |
812 map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems); |
814 in map inst (elemss ~~ envs) end; |
813 in map inst (elemss ~~ envs) end; |
815 |
814 |
816 (* like unify_elemss, but does not touch axioms, |
815 (* like unify_elemss, but does not touch axioms, additional |
817 additional parameter for enforcing further constraints (eg. syntax) *) |
816 parameter c_parms for enforcing further constraints (eg. syntax) *) |
818 |
817 |
819 fun unify_elemss' _ _ [] [] = [] |
818 fun unify_elemss' _ _ [] [] = [] |
820 | unify_elemss' _ [] [elems] [] = [elems] |
819 | unify_elemss' _ [] [elems] [] = [elems] |
821 | unify_elemss' ctxt fixed_parms elemss c_parms = |
820 | unify_elemss' ctxt fixed_parms elemss c_parms = |
822 let |
821 let |
904 (* check for conflicting syntax? *) |
903 (* check for conflicting syntax? *) |
905 in (ids'', parms'', syn'') end |
904 in (ids'', parms'', syn'') end |
906 | identify top (Merge es) = |
905 | identify top (Merge es) = |
907 Library.foldl (fn ((ids, parms, syn), e) => let |
906 Library.foldl (fn ((ids, parms, syn), e) => let |
908 val (ids', parms', syn') = identify top e |
907 val (ids', parms', syn') = identify top e |
909 in (gen_merge_lists eq_fst ids ids', |
908 in (merge_alists ids ids', |
910 merge_lists parms parms', |
909 merge_lists parms parms', |
911 merge_syntax ctxt ids' (syn, syn')) end) |
910 merge_syntax ctxt ids' (syn, syn')) end) |
912 (([], [], Symtab.empty), es); |
911 (([], [], Symtab.empty), es); |
913 |
912 |
914 (* CB: enrich identifiers by parameter types and |
913 (* CB: enrich identifiers by parameter types and |
1286 fun finish_elemss ctxt parms do_close = |
1285 fun finish_elemss ctxt parms do_close = |
1287 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
1286 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
1288 |
1287 |
1289 end; |
1288 end; |
1290 |
1289 |
1291 (* CB: type inference and consistency checks for locales *) |
1290 |
|
1291 (* CB: type inference and consistency checks for locales. |
|
1292 |
|
1293 Works by building a context (through declare_elemss), extracting the |
|
1294 required information and adjusting the context elements (finish_elemss). |
|
1295 Can also universally close free vars in assms and defs. This is only |
|
1296 needed for Ext elements and controlled by parameter do_close. |
|
1297 *) |
1292 |
1298 |
1293 fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl = |
1299 fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl = |
1294 let |
1300 let |
1295 (* CB: contexts computed in the course of this function are discarded. |
1301 (* CB: contexts computed in the course of this function are discarded. |
1296 They are used for type inference and consistency checks only. *) |
1302 They are used for type inference and consistency checks only. *) |
1615 |
1621 |
1616 (* add facts to locale in theory *) |
1622 (* add facts to locale in theory *) |
1617 |
1623 |
1618 fun put_facts loc args thy = |
1624 fun put_facts loc args thy = |
1619 let |
1625 let |
1620 val {predicate, import, elems, params} = the_locale thy loc; |
1626 val {predicate, import, elems, params, regs} = the_locale thy loc; |
1621 val note = Notes (map (fn ((a, atts), bs) => |
1627 val note = Notes (map (fn ((a, atts), bs) => |
1622 ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args); |
1628 ((a, atts), map (apfst (map (curry Thm.name_thm a))) bs)) args); |
1623 in |
1629 in |
1624 thy |> put_locale loc {predicate = predicate, import = import, |
1630 thy |> put_locale loc {predicate = predicate, import = import, |
1625 elems = elems @ [(note, stamp ())], params = params} |
1631 elems = elems @ [(note, stamp ())], params = params, regs = regs} |
1626 end; |
1632 end; |
1627 |
1633 |
1628 (* add theorem to locale and theory, |
1634 (* add theorem to locale and theory, |
1629 base for theorems (in loc) and declare (in loc) *) |
1635 base for theorems (in loc) and declare (in loc) *) |
1630 |
1636 |
1836 |> note_thmss_qualified "" name facts' |> #1 |
1842 |> note_thmss_qualified "" name facts' |> #1 |
1837 |> declare_locale name |
1843 |> declare_locale name |
1838 |> put_locale name {predicate = predicate, import = import, |
1844 |> put_locale name {predicate = predicate, import = import, |
1839 elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))), |
1845 elems = map (fn e => (e, stamp ())) (List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))), |
1840 params = (params_of elemss' |> |
1846 params = (params_of elemss' |> |
1841 map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss))} |
1847 map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)), |
|
1848 regs = []} |
1842 end; |
1849 end; |
1843 |
1850 |
1844 in |
1851 in |
1845 |
1852 |
1846 val add_locale = gen_add_locale read_context intern_expr; |
1853 val add_locale = gen_add_locale read_context intern_expr; |
1935 val thy = ProofContext.theory_of ctxt; |
1942 val thy = ProofContext.theory_of ctxt; |
1936 |
1943 |
1937 val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init; |
1944 val ctxt' = ctxt |> ProofContext.theory_of |> ProofContext.init; |
1938 val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy) |
1945 val ((ids, _), raw_elemss) = flatten (ctxt', intern_expr thy) |
1939 (([], Symtab.empty), Expr expr); |
1946 (([], Symtab.empty), Expr expr); |
1940 val do_close = false; (* effect unknown *) |
|
1941 val ((parms, all_elemss, _), (spec, (xs, defs, _))) = |
1947 val ((parms, all_elemss, _), (spec, (xs, defs, _))) = |
1942 read_elemss do_close ctxt' [] raw_elemss []; |
1948 read_elemss false ctxt' [] raw_elemss []; |
1943 |
1949 |
1944 |
1950 |
1945 (** compute instantiation **) |
1951 (** compute instantiation **) |
1946 |
1952 |
1947 (* user input *) |
1953 (* user input *) |