33 val empty: expr |
33 val empty: expr |
34 datatype ('typ, 'term, 'fact, 'att) elem_expr = |
34 datatype ('typ, 'term, 'fact, 'att) elem_expr = |
35 Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr |
35 Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr |
36 type 'att element |
36 type 'att element |
37 type 'att element_i |
37 type 'att element_i |
|
38 type 'att elem_or_expr |
|
39 type 'att elem_or_expr_i |
38 type locale |
40 type locale |
39 val intern: Sign.sg -> xstring -> string |
41 val intern: Sign.sg -> xstring -> string |
40 val cond_extern: Sign.sg -> string -> xstring |
42 val cond_extern: Sign.sg -> string -> xstring |
41 val the_locale: theory -> string -> locale |
43 val the_locale: theory -> string -> locale |
42 val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr |
44 val map_attrib_elem: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem |
|
45 -> ('typ, 'term, 'thm, context attribute) elem |
|
46 val map_attrib_elem_expr: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr |
43 -> ('typ, 'term, 'thm, context attribute) elem_expr |
47 -> ('typ, 'term, 'thm, context attribute) elem_expr |
44 val read_context_statement: xstring option -> context attribute element list -> |
48 val read_context_statement: xstring option -> context attribute elem_or_expr list -> |
45 (string * (string list * string list)) list list -> context -> |
49 (string * (string list * string list)) list list -> context -> |
46 string option * cterm list * context * context * (term * (term list * term list)) list list |
50 string option * cterm list * context * context * (term * (term list * term list)) list list |
47 val cert_context_statement: string option -> context attribute element_i list -> |
51 val cert_context_statement: string option -> context attribute elem_or_expr_i list -> |
48 (term * (term list * term list)) list list -> context -> |
52 (term * (term list * term list)) list list -> context -> |
49 string option * cterm list * context * context * (term * (term list * term list)) list list |
53 string option * cterm list * context * context * (term * (term list * term list)) list list |
50 val print_locales: theory -> unit |
54 val print_locales: theory -> unit |
51 val print_locale: theory -> expr -> context attribute element list -> unit |
55 val print_locale: theory -> expr -> context attribute element list -> unit |
52 val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory |
56 val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory |
90 val empty = Merge []; |
94 val empty = Merge []; |
91 |
95 |
92 datatype ('typ, 'term, 'fact, 'att) elem_expr = |
96 datatype ('typ, 'term, 'fact, 'att) elem_expr = |
93 Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr; |
97 Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr; |
94 |
98 |
95 type 'att element = (string, string, string, 'att) elem_expr; |
99 type 'att element = (string, string, string, 'att) elem; |
96 type 'att element_i = (typ, term, thm list, 'att) elem_expr; |
100 type 'att element_i = (typ, term, thm list, 'att) elem; |
|
101 type 'att elem_or_expr = (string, string, string, 'att) elem_expr; |
|
102 type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr; |
97 |
103 |
98 type locale = |
104 type locale = |
99 {view: cterm list * thm list, |
105 {view: cterm list * thm list, |
100 (* CB: If locale "loc" contains assumptions, either via import or in the |
106 (* CB: If locale "loc" contains assumptions, either via import or in the |
101 locale body, a locale predicate "loc" is defined capturing all the |
107 locale body, a locale predicate "loc" is defined capturing all the |
114 generated when entering the locale. |
120 generated when entering the locale. |
115 It appears that an axiom of the form A [A] is never generated. |
121 It appears that an axiom of the form A [A] is never generated. |
116 *) |
122 *) |
117 import: expr, (*dynamic import*) |
123 import: expr, (*dynamic import*) |
118 elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) |
124 elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) |
119 params: (string * typ option) list * string list}; (*all/local params*) |
125 params: (string * typ option) list * string list, (*all/local params*) |
120 |
126 typing: (string * typ) list}; (*inferred parameter types, currently unused*) |
121 fun make_locale view import elems params = |
|
122 {view = view, import = import, elems = elems, params = params}: locale; |
|
123 |
127 |
124 |
128 |
125 (** theory data **) |
129 (** theory data **) |
126 |
130 |
127 structure LocalesArgs = |
131 structure LocalesArgs = |
132 val empty = (NameSpace.empty, Symtab.empty); |
136 val empty = (NameSpace.empty, Symtab.empty); |
133 val copy = I; |
137 val copy = I; |
134 val prep_ext = I; |
138 val prep_ext = I; |
135 |
139 |
136 (*joining of locale elements: only facts may be added later!*) |
140 (*joining of locale elements: only facts may be added later!*) |
137 fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) = |
141 fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) = |
138 Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); |
142 Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems', |
|
143 params = params, typing = typing}; |
139 fun merge ((space1, locs1), (space2, locs2)) = |
144 fun merge ((space1, locs1), (space2, locs2)) = |
140 (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); |
145 (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); |
141 |
146 |
142 fun print _ (space, locs) = |
147 fun print _ (space, locs) = |
143 Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) |
148 Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs)) |
702 * A context element: add attrib to attribute lists of assumptions, |
707 * A context element: add attrib to attribute lists of assumptions, |
703 definitions and facts (on both sides for facts). |
708 definitions and facts (on both sides for facts). |
704 * Locale expression: no effect. *) |
709 * Locale expression: no effect. *) |
705 |
710 |
706 |
711 |
707 fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) |
712 fun map_attrib_elem _ (Fixes fixes) = Fixes fixes |
708 | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) |
713 | map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms) |
709 | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) |
714 | map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs) |
710 | attribute attrib (Elem (Notes facts)) = |
715 | map_attrib_elem attrib (Notes facts) = |
711 Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) |
716 Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts) |
712 | attribute _ (Expr expr) = Expr expr; |
717 |
|
718 fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem) |
|
719 | map_attrib_elem_expr _ (Expr expr) = Expr expr; |
713 |
720 |
714 end; |
721 end; |
715 |
722 |
716 |
723 |
717 (* parameters *) |
724 (* parameters *) |
892 fun finish_elemss ctxt parms do_close = |
899 fun finish_elemss ctxt parms do_close = |
893 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
900 foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
894 |
901 |
895 end; |
902 end; |
896 |
903 |
|
904 (* CB: type inference and consistency checks for locales *) |
|
905 |
897 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = |
906 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = |
898 let |
907 let |
|
908 (* CB: contexts computed in the course of this function are discarded. |
|
909 They are used for type inference and consistency checks only. *) |
899 (* CB: raw_elemss are list of pairs consisting of identifiers and |
910 (* CB: raw_elemss are list of pairs consisting of identifiers and |
900 context elements, the latter marked as internal or external. *) |
911 context elements, the latter marked as internal or external. *) |
901 val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; |
912 val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; |
902 (* CB: raw_ctxt is context with additional fixed variables derived from |
913 (* CB: raw_ctxt is context with additional fixed variables derived from |
903 the fixes elements in raw_elemss, |
914 the fixes elements in raw_elemss, |
1030 prep_ctxt false view_axioms fixed_params import elems concl ctxt; |
1041 prep_ctxt false view_axioms fixed_params import elems concl ctxt; |
1031 in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end; |
1042 in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end; |
1032 |
1043 |
1033 in |
1044 in |
1034 |
1045 |
1035 (* CB: arguments are: x->import, y->body (elements), z->context *) |
1046 (* CB: processing of locales for add_locale(_i) and print_locale *) |
1036 fun read_context x y z = #1 (gen_context true [] [] x y [] z); |
1047 (* CB: arguments are: x->import, y->body (elements), z->context *) |
1037 fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z); |
1048 fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z); |
1038 |
1049 fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z); |
|
1050 |
|
1051 (* CB: processing of locales for note_thmss(_i), |
|
1052 Proof.multi_theorem(_i) and antiquotations with option "locale" *) |
1039 val read_context_statement = gen_statement intern gen_context; |
1053 val read_context_statement = gen_statement intern gen_context; |
1040 val cert_context_statement = gen_statement (K I) gen_context_i; |
1054 val cert_context_statement = gen_statement (K I) gen_context_i; |
1041 |
1055 |
1042 end; |
1056 end; |
1043 |
1057 |
1278 |
1292 |
1279 local |
1293 local |
1280 |
1294 |
1281 fun put_facts loc args thy = |
1295 fun put_facts loc args thy = |
1282 let |
1296 let |
1283 val {view, import, elems, params} = the_locale thy loc; |
1297 val {view, import, elems, params, typing} = the_locale thy loc; |
1284 val note = Notes (map (fn ((a, more_atts), th_atts) => |
1298 val note = Notes (map (fn ((a, more_atts), th_atts) => |
1285 ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); |
1299 ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); |
1286 in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end; |
1300 in thy |> put_locale loc {view = view, import = import, elems = elems @ [(note, stamp ())], |
|
1301 params = params, typing = typing} end; |
1287 |
1302 |
1288 fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy = |
1303 fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy = |
1289 let |
1304 let |
1290 val thy_ctxt = ProofContext.init thy; |
1305 val thy_ctxt = ProofContext.init thy; |
1291 val loc = prep_locale (Theory.sign_of thy) raw_loc; |
1306 val loc = prep_locale (Theory.sign_of thy) raw_loc; |
1461 error ("Duplicate definition of locale " ^ quote name)); |
1476 error ("Duplicate definition of locale " ^ quote name)); |
1462 |
1477 |
1463 val thy_ctxt = ProofContext.init thy; |
1478 val thy_ctxt = ProofContext.init thy; |
1464 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) = |
1479 val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) = |
1465 prep_ctxt raw_import raw_body thy_ctxt; |
1480 prep_ctxt raw_import raw_body thy_ctxt; |
|
1481 (* typing: all parameters with their types *) |
|
1482 val (typing, _, _) = text; |
1466 val elemss = import_elemss @ body_elemss; |
1483 val elemss = import_elemss @ body_elemss; |
1467 |
1484 |
1468 val (pred_thy, (elemss', view as (view_statement, view_axioms))) = |
1485 val (pred_thy, (elemss', view as (view_statement, view_axioms))) = |
1469 if do_pred then thy |> define_preds bname text elemss |
1486 if do_pred then thy |> define_preds bname text elemss |
1470 else (thy, (elemss, ([], []))); |
1487 else (thy, (elemss, ([], []))); |
1475 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); |
1492 val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); |
1476 in |
1493 in |
1477 pred_thy |
1494 pred_thy |
1478 |> note_thmss_qualified "" name facts' |> #1 |
1495 |> note_thmss_qualified "" name facts' |> #1 |
1479 |> declare_locale name |
1496 |> declare_locale name |
1480 |> put_locale name (make_locale view (prep_expr sign raw_import) |
1497 |> put_locale name {view = view, import = prep_expr sign raw_import, |
1481 (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) |
1498 elems = map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))), |
1482 (params_of elemss', map #1 (params_of body_elemss))) |
1499 params = (params_of elemss', map #1 (params_of body_elemss)), typing = typing} |
1483 end; |
1500 end; |
1484 |
1501 |
1485 in |
1502 in |
1486 |
1503 |
1487 val add_locale = gen_add_locale read_context intern_expr; |
1504 val add_locale = gen_add_locale read_context intern_expr; |