author | wenzelm |
Wed, 07 Jan 2009 16:22:10 +0100 | |
changeset 29383 | 223f18cfbb32 |
parent 29360 | a5be60c3674e |
permissions | -rw-r--r-- |
12014 | 1 |
(* Title: Pure/Isar/locale.ML |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29004
diff
changeset
|
2 |
Author: Clemens Ballarin, TU Muenchen |
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29004
diff
changeset
|
3 |
Author: Markus Wenzel, LMU/TU Muenchen |
11896 | 4 |
|
12058 | 5 |
Locales -- Isar proof contexts as meta-level predicates, with local |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
6 |
syntax and implicit structures. |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
7 |
|
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
8 |
Draws basic ideas from Florian Kammueller's original version of |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
9 |
locales, but uses the richer infrastructure of Isar instead of the raw |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
10 |
meta-logic. Furthermore, structured import of contexts (with merge |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
11 |
and rename operations) are provided, as well as type-inference of the |
13375 | 12 |
signature parts, and predicate definitions of the specification text. |
14446 | 13 |
|
17437 | 14 |
Interpretation enables the reuse of theorems of locales in other |
15 |
contexts, namely those defined by theories, structured proofs and |
|
16 |
locales themselves. |
|
17 |
||
14446 | 18 |
See also: |
19 |
||
20 |
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar. |
|
21 |
In Stefano Berardi et al., Types for Proofs and Programs: International |
|
15099 | 22 |
Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004. |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
23 |
[2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
24 |
Dependencies between Locales. Technical Report TUM-I0607, Technische |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
25 |
Universitaet Muenchen, 2006. |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
26 |
[3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
27 |
Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108, |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
28 |
pages 31-43, 2006. |
11896 | 29 |
*) |
30 |
||
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
31 |
(* TODO: |
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
32 |
- beta-eta normalisation of interpretation parameters |
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
33 |
- dangling type frees in locales |
16620
2a7f46324218
Proper treatment of beta-redexes in witness theorems.
ballarin
parents:
16458
diff
changeset
|
34 |
- test subsumption of interpretations when merging theories |
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
35 |
*) |
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
36 |
|
29360 | 37 |
signature OLD_LOCALE = |
11896 | 38 |
sig |
12273 | 39 |
datatype expr = |
40 |
Locale of string | |
|
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
41 |
Rename of expr * (string * mixfix option) option list | |
12273 | 42 |
Merge of expr list |
43 |
val empty: expr |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
44 |
|
16458 | 45 |
val intern: theory -> xstring -> string |
24751 | 46 |
val intern_expr: theory -> expr -> expr |
16458 | 47 |
val extern: theory -> string -> xstring |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
48 |
val init: string -> theory -> Proof.context |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
49 |
|
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
50 |
(* The specification of a locale *) |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
51 |
val parameters_of: theory -> string -> ((string * typ) * mixfix) list |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
52 |
val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
53 |
val local_asms_of: theory -> string -> (Attrib.binding * term list) list |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
54 |
val global_asms_of: theory -> string -> (Attrib.binding * term list) list |
27716 | 55 |
|
56 |
(* Theorems *) |
|
25619 | 57 |
val intros: theory -> string -> thm list * thm list |
58 |
val dests: theory -> string -> thm list |
|
27716 | 59 |
(* Not part of the official interface. DO NOT USE *) |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
60 |
val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list |
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
61 |
|
28691 | 62 |
(* Not part of the official interface. DO NOT USE *) |
63 |
val declarations_of: theory -> string -> declaration list * declaration list; |
|
64 |
||
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset
|
65 |
(* Processing of locale statements *) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
66 |
val read_context_statement: string option -> Element.context list -> |
19585 | 67 |
(string * string list) list list -> Proof.context -> |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
68 |
string option * Proof.context * Proof.context * (term * term list) list list |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
69 |
val read_context_statement_cmd: xstring option -> Element.context list -> |
21035 | 70 |
(string * string list) list list -> Proof.context -> |
71 |
string option * Proof.context * Proof.context * (term * term list) list list |
|
28710 | 72 |
val cert_context_statement: string option -> Element.context_i list -> |
19585 | 73 |
(term * term list) list list -> Proof.context -> |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
74 |
string option * Proof.context * Proof.context * (term * term list) list list |
19780 | 75 |
val read_expr: expr -> Element.context list -> Proof.context -> |
76 |
Element.context_i list * Proof.context |
|
77 |
val cert_expr: expr -> Element.context_i list -> Proof.context -> |
|
78 |
Element.context_i list * Proof.context |
|
15596 | 79 |
|
80 |
(* Diagnostic functions *) |
|
12758 | 81 |
val print_locales: theory -> unit |
18137 | 82 |
val print_locale: theory -> bool -> expr -> Element.context list -> unit |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
83 |
val print_registrations: bool -> string -> Proof.context -> unit |
18137 | 84 |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
85 |
val add_locale: string -> bstring -> expr -> Element.context_i list -> theory |
20965 | 86 |
-> string * Proof.context |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
87 |
val add_locale_cmd: bstring -> expr -> Element.context list -> theory |
20965 | 88 |
-> string * Proof.context |
15596 | 89 |
|
21225 | 90 |
(* Tactics *) |
91 |
val intro_locales_tac: bool -> Proof.context -> thm list -> tactic |
|
92 |
||
15696 | 93 |
(* Storing results *) |
28950 | 94 |
val global_note_qualified: string -> |
28965 | 95 |
((Binding.T * attribute list) * (thm list * attribute list) list) list -> |
28950 | 96 |
theory -> (string * thm list) list * theory |
28865 | 97 |
val local_note_qualified: string -> |
28965 | 98 |
((Binding.T * attribute list) * (thm list * attribute list) list) list -> |
28940 | 99 |
Proof.context -> (string * thm list) list * Proof.context |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
100 |
val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list -> |
21582 | 101 |
Proof.context -> Proof.context |
24020 | 102 |
val add_type_syntax: string -> declaration -> Proof.context -> Proof.context |
103 |
val add_term_syntax: string -> declaration -> Proof.context -> Proof.context |
|
104 |
val add_declaration: string -> declaration -> Proof.context -> Proof.context |
|
18137 | 105 |
|
28259 | 106 |
(* Interpretation *) |
28965 | 107 |
val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string -> |
28259 | 108 |
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
109 |
string -> term list -> Morphism.morphism |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
110 |
val interpretation: (Proof.context -> Proof.context) -> |
28965 | 111 |
(Binding.T -> Binding.T) -> expr -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
112 |
term option list * (Attrib.binding * term) list -> |
28259 | 113 |
theory -> |
114 |
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
115 |
val interpretation_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
116 |
theory -> Proof.state |
21005 | 117 |
val interpretation_in_locale: (Proof.context -> Proof.context) -> |
118 |
xstring * expr -> theory -> Proof.state |
|
29383 | 119 |
val interpret: (Proof.state -> Proof.state) -> |
28965 | 120 |
(Binding.T -> Binding.T) -> expr -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
121 |
term option list * (Attrib.binding * term) list -> |
28259 | 122 |
bool -> Proof.state -> |
123 |
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
124 |
val interpret_cmd: string -> expr -> string option list * (Attrib.binding * string) list -> |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
125 |
bool -> Proof.state -> Proof.state |
11896 | 126 |
end; |
12839 | 127 |
|
29360 | 128 |
structure Old_Locale: OLD_LOCALE = |
11896 | 129 |
struct |
130 |
||
23228
05fb9b2b16d7
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
wenzelm
parents:
23178
diff
changeset
|
131 |
(* legacy operations *) |
05fb9b2b16d7
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
wenzelm
parents:
23178
diff
changeset
|
132 |
|
27681 | 133 |
fun merge_lists _ xs [] = xs |
134 |
| merge_lists _ [] ys = ys |
|
135 |
| merge_lists eq xs ys = xs @ filter_out (member eq xs) ys; |
|
136 |
||
137 |
fun merge_alists eq xs = merge_lists (eq_fst eq) xs; |
|
19780 | 138 |
|
20307 | 139 |
|
28940 | 140 |
(* auxiliary: noting name bindings with qualified base names *) |
141 |
||
142 |
fun global_note_qualified kind facts thy = |
|
28792 | 143 |
thy |
144 |
|> Sign.qualified_names |
|
28940 | 145 |
|> PureThy.note_thmss kind facts |
28792 | 146 |
||> Sign.restore_naming thy; |
147 |
||
28940 | 148 |
fun local_note_qualified kind facts ctxt = |
28792 | 149 |
ctxt |
150 |
|> ProofContext.qualified_names |
|
28940 | 151 |
|> ProofContext.note_thmss_i kind facts |
28792 | 152 |
||> ProofContext.restore_naming ctxt; |
28739 | 153 |
|
154 |
||
12273 | 155 |
(** locale elements and expressions **) |
11896 | 156 |
|
18137 | 157 |
datatype ctxt = datatype Element.ctxt; |
17355 | 158 |
|
12273 | 159 |
datatype expr = |
160 |
Locale of string | |
|
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
161 |
Rename of expr * (string * mixfix option) option list | |
12273 | 162 |
Merge of expr list; |
11896 | 163 |
|
12273 | 164 |
val empty = Merge []; |
165 |
||
18137 | 166 |
datatype 'a element = |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
167 |
Elem of 'a | Expr of expr; |
12273 | 168 |
|
18137 | 169 |
fun map_elem f (Elem e) = Elem (f e) |
170 |
| map_elem _ (Expr e) = Expr e; |
|
171 |
||
24020 | 172 |
type decl = declaration * stamp; |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
173 |
|
12070 | 174 |
type locale = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
175 |
{axiom: Element.witness list, |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
176 |
(* For locales that define predicates this is [A [A]], where A is the locale |
20317 | 177 |
specification. Otherwise []. |
178 |
Only required to generate the right witnesses for locales with predicates. *) |
|
19783 | 179 |
elems: (Element.context_i * stamp) list, |
180 |
(* Static content, neither Fixes nor Constrains elements *) |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
181 |
params: ((string * typ) * mixfix) list, (*all term params*) |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
182 |
decls: decl list * decl list, (*type/term_syntax declarations*) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
183 |
regs: ((string * string list) * Element.witness list) list, |
19780 | 184 |
(* Registrations: indentifiers and witnesses of locales interpreted in the locale. *) |
25619 | 185 |
intros: thm list * thm list, |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
186 |
(* Introduction rules: of delta predicate and locale predicate. *) |
25619 | 187 |
dests: thm list} |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
188 |
(* Destruction rules: projections from locale predicate to predicates of fragments. *) |
11896 | 189 |
|
15703 | 190 |
(* CB: an internal (Int) locale element was either imported or included, |
191 |
an external (Ext) element appears directly in the locale text. *) |
|
192 |
||
193 |
datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
|
194 |
||
195 |
||
196 |
||
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
197 |
(** substitutions on Vars -- clone from element.ML **) |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
198 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
199 |
(* instantiate types *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
200 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
201 |
fun var_instT_type env = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
202 |
if Vartab.is_empty env then I |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
203 |
else Term.map_type_tvar (fn (x, S) => the_default (TVar (x, S)) (Vartab.lookup env x)); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
204 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
205 |
fun var_instT_term env = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
206 |
if Vartab.is_empty env then I |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
207 |
else Term.map_types (var_instT_type env); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
208 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
209 |
fun var_inst_term (envT, env) = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
210 |
if Vartab.is_empty env then var_instT_term envT |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
211 |
else |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
212 |
let |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
213 |
val instT = var_instT_type envT; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
214 |
fun inst (Const (x, T)) = Const (x, instT T) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
215 |
| inst (Free (x, T)) = Free(x, instT T) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
216 |
| inst (Var (xi, T)) = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
217 |
(case Vartab.lookup env xi of |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
218 |
NONE => Var (xi, instT T) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
219 |
| SOME t => t) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
220 |
| inst (b as Bound _) = b |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
221 |
| inst (Abs (x, T, t)) = Abs (x, instT T, inst t) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
222 |
| inst (t $ u) = inst t $ inst u; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
223 |
in Envir.beta_norm o inst end; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
224 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
225 |
|
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
226 |
(** management of registrations in theories and proof contexts **) |
11896 | 227 |
|
28005 | 228 |
type registration = |
28965 | 229 |
{prfx: (Binding.T -> Binding.T) * (string * string), |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
230 |
(* first component: interpretation name morphism; |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
231 |
second component: parameter prefix *) |
28005 | 232 |
exp: Morphism.morphism, |
233 |
(* maps content to its originating context *) |
|
234 |
imp: (typ Vartab.table * typ list) * (term Vartab.table * term list), |
|
235 |
(* inverse of exp *) |
|
236 |
wits: Element.witness list, |
|
237 |
(* witnesses of the registration *) |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
238 |
eqns: thm Termtab.table, |
28005 | 239 |
(* theorems (equations) interpreting derived concepts and indexed by lhs *) |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
240 |
morph: unit |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
241 |
(* interpreting morphism *) |
28005 | 242 |
} |
243 |
||
15837 | 244 |
structure Registrations : |
245 |
sig |
|
246 |
type T |
|
247 |
val empty: T |
|
248 |
val join: T * T -> T |
|
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
249 |
val dest: theory -> T -> |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
250 |
(term list * |
28965 | 251 |
(((Binding.T -> Binding.T) * (string * string)) * |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
252 |
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
253 |
Element.witness list * |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
254 |
thm Termtab.table)) list |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
255 |
val test: theory -> T * term list -> bool |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
256 |
val lookup: theory -> |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
257 |
T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
28965 | 258 |
(((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option |
259 |
val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) -> |
|
28005 | 260 |
(Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) -> |
261 |
T -> |
|
28965 | 262 |
T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list |
19780 | 263 |
val add_witness: term list -> Element.witness -> T -> T |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
264 |
val add_equation: term list -> thm -> T -> T |
28259 | 265 |
(* |
266 |
val update_morph: term list -> Morphism.morphism -> T -> T |
|
267 |
val get_morph: theory -> T -> |
|
268 |
term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list)) -> |
|
269 |
Morphism.morphism |
|
270 |
*) |
|
15837 | 271 |
end = |
272 |
struct |
|
28005 | 273 |
(* A registration is indexed by parameter instantiation. |
274 |
NB: index is exported whereas content is internalised. *) |
|
275 |
type T = registration Termtab.table; |
|
276 |
||
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
277 |
fun mk_reg prfx exp imp wits eqns morph = |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
278 |
{prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph}; |
28005 | 279 |
|
280 |
fun map_reg f reg = |
|
281 |
let |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
282 |
val {prfx, exp, imp, wits, eqns, morph} = reg; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
283 |
val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
284 |
in mk_reg prfx' exp' imp' wits' eqns' morph' end; |
15837 | 285 |
|
286 |
val empty = Termtab.empty; |
|
287 |
||
288 |
(* term list represented as single term, for simultaneous matching *) |
|
289 |
fun termify ts = |
|
18343 | 290 |
Term.list_comb (Const ("", map fastype_of ts ---> propT), ts); |
15837 | 291 |
fun untermify t = |
292 |
let fun ut (Const _) ts = ts |
|
293 |
| ut (s $ t) ts = ut s (t::ts) |
|
294 |
in ut t [] end; |
|
295 |
||
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
296 |
(* joining of registrations: |
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
297 |
- prefix and morphisms of right theory; |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
298 |
- witnesses are equal, no attempt to subsumption testing; |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
299 |
- union of equalities, if conflicting (i.e. two eqns with equal lhs) |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
300 |
eqn of right theory takes precedence *) |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
301 |
fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) => |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
302 |
mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2); |
15837 | 303 |
|
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
304 |
fun dest_transfer thy regs = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
305 |
Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) => |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
306 |
(n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m)))); |
28005 | 307 |
|
308 |
fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |> |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
309 |
map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns))); |
15837 | 310 |
|
311 |
(* registrations that subsume t *) |
|
17203 | 312 |
fun subsumers thy t regs = |
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
313 |
filter (fn (t', _) => Pattern.matches thy (t', t)) (dest_transfer thy regs); |
15837 | 314 |
|
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
315 |
(* test if registration that subsumes the query is present *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
316 |
fun test thy (regs, ts) = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
317 |
not (null (subsumers thy (termify ts) regs)); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
318 |
|
15837 | 319 |
(* look up registration, pick one that subsumes the query *) |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
320 |
fun lookup thy (regs, (ts, ((impT, _), (imp, _)))) = |
15837 | 321 |
let |
322 |
val t = termify ts; |
|
19780 | 323 |
val subs = subsumers thy t regs; |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
324 |
in |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
325 |
(case subs of |
15837 | 326 |
[] => NONE |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
327 |
| ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) => |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
328 |
let |
19780 | 329 |
val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty); |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
330 |
val tinst' = domT' |> map (fn (T as TFree (x, _)) => |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
331 |
(x, T |> Morphism.typ exp' |> Envir.typ_subst_TVars tinst |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
332 |
|> var_instT_type impT)) |> Symtab.make; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
333 |
val inst' = dom' |> map (fn (t as Free (x, _)) => |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
334 |
(x, t |> Morphism.term exp' |> Envir.subst_vars (tinst, inst) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
335 |
|> var_inst_term (impT, imp))) |> Symtab.make; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
336 |
val inst'_morph = Element.inst_morphism thy (tinst', inst'); |
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
337 |
in SOME (prfx, |
28005 | 338 |
map (Element.morph_witness inst'_morph) wits, |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
339 |
Termtab.map (Morphism.thm inst'_morph) eqns) |
23918 | 340 |
end) |
15837 | 341 |
end; |
342 |
||
343 |
(* add registration if not subsumed by ones already present, |
|
344 |
additionally returns registrations that are strictly subsumed *) |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
345 |
fun insert thy ts prfx (exp, imp) regs = |
15837 | 346 |
let |
347 |
val t = termify ts; |
|
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
348 |
val subs = subsumers thy t regs ; |
15837 | 349 |
in (case subs of |
350 |
[] => let |
|
351 |
val sups = |
|
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
352 |
filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs); |
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
353 |
val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits))) |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
354 |
in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end |
15837 | 355 |
| _ => (regs, [])) |
356 |
end; |
|
357 |
||
25669 | 358 |
fun gen_add f ts regs = |
23918 | 359 |
let |
360 |
val t = termify ts; |
|
361 |
in |
|
28005 | 362 |
Termtab.update (t, map_reg f (the (Termtab.lookup regs t))) regs |
23918 | 363 |
end; |
364 |
||
15837 | 365 |
(* add witness theorem to registration, |
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
366 |
only if instantiation is exact, otherwise exception Option raised *) |
25669 | 367 |
fun add_witness ts wit regs = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
368 |
gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m)) |
25669 | 369 |
ts regs; |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
370 |
|
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
371 |
(* add equation to registration, replaces previous equation with same lhs; |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
372 |
only if instantiation is exact, otherwise exception Option raised; |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
373 |
exception TERM raised if not a meta equality *) |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
374 |
fun add_equation ts thm regs = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
375 |
gen_add (fn (x, e, i, thms, eqns, m) => |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
376 |
(x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m)) |
25669 | 377 |
ts regs; |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
378 |
|
15837 | 379 |
end; |
380 |
||
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
381 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
382 |
(** theory data : locales **) |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
383 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
384 |
structure LocalesData = TheoryDataFun |
22846 | 385 |
( |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
386 |
type T = NameSpace.T * locale Symtab.table; |
15596 | 387 |
(* 1st entry: locale namespace, |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
388 |
2nd entry: locales of the theory *) |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
389 |
|
28991 | 390 |
val empty = NameSpace.empty_table; |
12063 | 391 |
val copy = I; |
16458 | 392 |
val extend = I; |
12289 | 393 |
|
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
394 |
fun join_locales _ |
27716 | 395 |
({axiom, elems, params, decls = (decls1, decls2), regs, intros, dests}: locale, |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
396 |
{elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
397 |
{axiom = axiom, |
27681 | 398 |
elems = merge_lists (eq_snd (op =)) elems elems', |
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
399 |
params = params, |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
400 |
decls = |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
401 |
(Library.merge (eq_snd (op =)) (decls1, decls1'), |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
402 |
Library.merge (eq_snd (op =)) (decls2, decls2')), |
27681 | 403 |
regs = merge_alists (op =) regs regs', |
25619 | 404 |
intros = intros, |
405 |
dests = dests}; |
|
28991 | 406 |
fun merge _ = NameSpace.join_tables join_locales; |
22846 | 407 |
); |
15801 | 408 |
|
409 |
||
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
410 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
411 |
(** context data : registrations **) |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
412 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
413 |
structure RegistrationsData = GenericDataFun |
22846 | 414 |
( |
415 |
type T = Registrations.T Symtab.table; (*registrations, indexed by locale name*) |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
416 |
val empty = Symtab.empty; |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
417 |
val extend = I; |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
418 |
fun merge _ = Symtab.join (K Registrations.join); |
22846 | 419 |
); |
12289 | 420 |
|
12277 | 421 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
422 |
(** access locales **) |
12277 | 423 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
424 |
val intern = NameSpace.intern o #1 o LocalesData.get; |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
425 |
val extern = NameSpace.extern o #1 o LocalesData.get; |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
426 |
|
27681 | 427 |
fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name; |
428 |
||
429 |
fun the_locale thy name = case get_locale thy name |
|
430 |
of SOME loc => loc |
|
431 |
| NONE => error ("Unknown locale " ^ quote name); |
|
432 |
||
28991 | 433 |
fun register_locale bname loc thy = |
434 |
thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) |
|
435 |
(Binding.name bname, loc) #> snd); |
|
11896 | 436 |
|
18806 | 437 |
fun change_locale name f thy = |
438 |
let |
|
27716 | 439 |
val {axiom, elems, params, decls, regs, intros, dests} = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
440 |
the_locale thy name; |
27716 | 441 |
val (axiom', elems', params', decls', regs', intros', dests') = |
442 |
f (axiom, elems, params, decls, regs, intros, dests); |
|
18806 | 443 |
in |
27681 | 444 |
thy |
445 |
|> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom', |
|
27716 | 446 |
elems = elems', params = params', |
27681 | 447 |
decls = decls', regs = regs', intros = intros', dests = dests'})) |
448 |
end; |
|
449 |
||
450 |
fun print_locales thy = |
|
451 |
let val (space, locs) = LocalesData.get thy in |
|
452 |
Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs))) |
|
453 |
|> Pretty.writeln |
|
18806 | 454 |
end; |
455 |
||
12046 | 456 |
|
15596 | 457 |
(* access registrations *) |
458 |
||
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
459 |
(* retrieve registration from theory or context *) |
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
460 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
461 |
fun get_registrations ctxt name = |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
462 |
case Symtab.lookup (RegistrationsData.get ctxt) name of |
15696 | 463 |
NONE => [] |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
464 |
| SOME reg => Registrations.dest (Context.theory_of ctxt) reg; |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
465 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
466 |
fun get_global_registrations thy = get_registrations (Context.Theory thy); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
467 |
fun get_local_registrations ctxt = get_registrations (Context.Proof ctxt); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
468 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
469 |
|
25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset
|
470 |
fun get_registration ctxt imprt (name, ps) = |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
471 |
case Symtab.lookup (RegistrationsData.get ctxt) name of |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
472 |
NONE => NONE |
25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset
|
473 |
| SOME reg => Registrations.lookup (Context.theory_of ctxt) (reg, (ps, imprt)); |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
474 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
475 |
fun get_global_registration thy = get_registration (Context.Theory thy); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
476 |
fun get_local_registration ctxt = get_registration (Context.Proof ctxt); |
15596 | 477 |
|
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
478 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
479 |
fun test_registration ctxt (name, ps) = |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
480 |
case Symtab.lookup (RegistrationsData.get ctxt) name of |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
481 |
NONE => false |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
482 |
| SOME reg => Registrations.test (Context.theory_of ctxt) (reg, ps); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
483 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
484 |
fun test_global_registration thy = test_registration (Context.Theory thy); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
485 |
fun test_local_registration ctxt = test_registration (Context.Proof ctxt); |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
486 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
487 |
|
15837 | 488 |
(* add registration to theory or context, ignored if subsumed *) |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
489 |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
490 |
fun put_registration (name, ps) prfx morphs ctxt = |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
491 |
RegistrationsData.map (fn regs => |
15837 | 492 |
let |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
493 |
val thy = Context.theory_of ctxt; |
18343 | 494 |
val reg = the_default Registrations.empty (Symtab.lookup regs name); |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
495 |
val (reg', sups) = Registrations.insert thy ps prfx morphs reg; |
15837 | 496 |
val _ = if not (null sups) then warning |
497 |
("Subsumed interpretation(s) of locale " ^ |
|
16458 | 498 |
quote (extern thy name) ^ |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
499 |
"\nwith the following prefix(es):" ^ |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
500 |
commas_quote (map (fn (_, ((_, (_, s)), _)) => s) sups)) |
15837 | 501 |
else (); |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
502 |
in Symtab.update (name, reg') regs end) ctxt; |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
503 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
504 |
fun put_global_registration id prfx morphs = |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
505 |
Context.theory_map (put_registration id prfx morphs); |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
506 |
fun put_local_registration id prfx morphs = |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
507 |
Context.proof_map (put_registration id prfx morphs); |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
508 |
|
18806 | 509 |
fun put_registration_in_locale name id = |
27716 | 510 |
change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => |
511 |
(axiom, elems, params, decls, regs @ [(id, [])], intros, dests)); |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
512 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
513 |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
514 |
(* add witness theorem to registration, ignored if registration not present *) |
15596 | 515 |
|
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
516 |
fun add_witness (name, ps) thm = |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
517 |
RegistrationsData.map (Symtab.map_entry name (Registrations.add_witness ps thm)); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
518 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
519 |
fun add_global_witness id thm = Context.theory_map (add_witness id thm); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
520 |
fun add_local_witness id thm = Context.proof_map (add_witness id thm); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
521 |
|
15596 | 522 |
|
18806 | 523 |
fun add_witness_in_locale name id thm = |
27716 | 524 |
change_locale name (fn (axiom, elems, params, decls, regs, intros, dests) => |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
525 |
let |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
526 |
fun add (id', thms) = |
18806 | 527 |
if id = id' then (id', thm :: thms) else (id', thms); |
27716 | 528 |
in (axiom, elems, params, decls, map add regs, intros, dests) end); |
15596 | 529 |
|
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
530 |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
531 |
(* add equation to registration, ignored if registration not present *) |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
532 |
|
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
533 |
fun add_equation (name, ps) thm = |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
534 |
RegistrationsData.map (Symtab.map_entry name (Registrations.add_equation ps thm)); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
535 |
|
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
536 |
fun add_global_equation id thm = Context.theory_map (add_equation id thm); |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
537 |
fun add_local_equation id thm = Context.proof_map (add_equation id thm); |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
538 |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
539 |
(* |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
540 |
(* update morphism of registration, ignored if registration not present *) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
541 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
542 |
fun update_morph (name, ps) morph = |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
543 |
RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph)); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
544 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
545 |
fun update_global_morph id morph = Context.theory_map (update_morph id morph); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
546 |
fun update_local_morph id morph = Context.proof_map (update_morph id morph); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
547 |
*) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
548 |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
549 |
|
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
550 |
(* printing of registrations *) |
15596 | 551 |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
552 |
fun print_registrations show_wits loc ctxt = |
15596 | 553 |
let |
15703 | 554 |
val thy = ProofContext.theory_of ctxt; |
24920 | 555 |
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
556 |
fun prt_term' t = if !show_types |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
557 |
then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::", |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
558 |
Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)] |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
559 |
else prt_term t; |
23918 | 560 |
val prt_thm = prt_term o prop_of; |
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
561 |
fun prt_inst ts = |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
562 |
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts)); |
28739 | 563 |
fun prt_prfx ((false, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str param_prfx] |
564 |
| prt_prfx ((true, prfx), param_prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str param_prfx]; |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
565 |
fun prt_eqns [] = Pretty.str "no equations." |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
566 |
| prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 :: |
23918 | 567 |
Pretty.breaks (map prt_thm eqns)); |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
568 |
fun prt_core ts eqns = |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
569 |
[prt_inst ts, Pretty.fbrk, prt_eqns (Termtab.dest eqns |> map snd)]; |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
570 |
fun prt_witns [] = Pretty.str "no witnesses." |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
571 |
| prt_witns witns = Pretty.block (Pretty.str "witnesses:" :: Pretty.brk 1 :: |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
572 |
Pretty.breaks (map (Element.pretty_witness ctxt) witns)) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
573 |
fun prt_reg (ts, (_, _, witns, eqns)) = |
17138 | 574 |
if show_wits |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
575 |
then Pretty.block (prt_core ts eqns @ [Pretty.fbrk, prt_witns witns]) |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
576 |
else Pretty.block (prt_core ts eqns) |
15703 | 577 |
|
16458 | 578 |
val loc_int = intern thy loc; |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
579 |
val regs = RegistrationsData.get (Context.Proof ctxt); |
17412 | 580 |
val loc_regs = Symtab.lookup regs loc_int; |
15596 | 581 |
in |
582 |
(case loc_regs of |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
583 |
NONE => Pretty.str ("no interpretations") |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15749
diff
changeset
|
584 |
| SOME r => let |
20069
77a6b62418bb
Witness theorems of interpretations now transfered to current theory.
ballarin
parents:
20059
diff
changeset
|
585 |
val r' = Registrations.dest thy r; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
586 |
val r'' = Library.sort_wrt (fn (_, ((_, (_, prfx)), _, _, _)) => prfx) r'; |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
587 |
in Pretty.big_list ("interpretations:") (map prt_reg r'') end) |
15596 | 588 |
|> Pretty.writeln |
589 |
end; |
|
590 |
||
591 |
||
12277 | 592 |
(* diagnostics *) |
12273 | 593 |
|
12277 | 594 |
fun err_in_locale ctxt msg ids = |
595 |
let |
|
16458 | 596 |
val thy = ProofContext.theory_of ctxt; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
597 |
fun prt_id (name, parms) = |
16458 | 598 |
[Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
599 |
val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
12502 | 600 |
val err_msg = |
28375 | 601 |
if forall (fn (s, _) => s = "") ids then msg |
12502 | 602 |
else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
603 |
(Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
|
18678 | 604 |
in error err_msg end; |
12063 | 605 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
606 |
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids'); |
12277 | 607 |
|
608 |
||
19783 | 609 |
fun pretty_ren NONE = Pretty.str "_" |
610 |
| pretty_ren (SOME (x, NONE)) = Pretty.str x |
|
611 |
| pretty_ren (SOME (x, SOME syn)) = |
|
612 |
Pretty.block [Pretty.str x, Pretty.brk 1, Syntax.pretty_mixfix syn]; |
|
613 |
||
614 |
fun pretty_expr thy (Locale name) = Pretty.str (extern thy name) |
|
615 |
| pretty_expr thy (Rename (expr, xs)) = |
|
616 |
Pretty.block [pretty_expr thy expr, Pretty.brk 1, Pretty.block (map pretty_ren xs |> Pretty.breaks)] |
|
617 |
| pretty_expr thy (Merge es) = |
|
618 |
Pretty.separate "+" (map (pretty_expr thy) es) |> Pretty.block; |
|
619 |
||
620 |
fun err_in_expr _ msg (Merge []) = error msg |
|
621 |
| err_in_expr ctxt msg expr = |
|
622 |
error (msg ^ "\n" ^ Pretty.string_of (Pretty.block |
|
623 |
[Pretty.str "The error(s) above occured in locale expression:", Pretty.brk 1, |
|
624 |
pretty_expr (ProofContext.theory_of ctxt) expr])); |
|
625 |
||
12046 | 626 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
627 |
(** structured contexts: rename + merge + implicit type instantiation **) |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
628 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
629 |
(* parameter types *) |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
630 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
631 |
fun frozen_tvars ctxt Ts = |
19914 | 632 |
#1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt) |
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
633 |
|> map (fn ((xi, S), T) => (xi, (S, T))); |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
634 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
635 |
fun unify_frozen ctxt maxidx Ts Us = |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
636 |
let |
18343 | 637 |
fun paramify NONE i = (NONE, i) |
638 |
| paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
639 |
|
18343 | 640 |
val (Ts', maxidx') = fold_map paramify Ts maxidx; |
641 |
val (Us', maxidx'') = fold_map paramify Us maxidx'; |
|
16947 | 642 |
val thy = ProofContext.theory_of ctxt; |
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
643 |
|
18190 | 644 |
fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env |
645 |
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) |
|
646 |
| unify _ env = env; |
|
647 |
val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); |
|
15570 | 648 |
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; |
29004 | 649 |
val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier; |
15570 | 650 |
in map (Option.map (Envir.norm_type unifier')) Vs end; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
651 |
|
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
652 |
fun params_of elemss = |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
653 |
distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
654 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
655 |
fun params_of' elemss = |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
656 |
distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
657 |
|
28862 | 658 |
fun param_prefix locale_name params = (NameSpace.base locale_name ^ "_locale", space_implode "_" params); |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
659 |
|
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
660 |
|
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
661 |
(* CB: param_types has the following type: |
15531 | 662 |
('a * 'b option) list -> ('a * 'b) list *) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
663 |
fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
664 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
665 |
|
19932 | 666 |
fun merge_syntax ctxt ids ss = Symtab.merge (op = : mixfix * mixfix -> bool) ss |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
667 |
handle Symtab.DUP x => err_in_locale ctxt |
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
668 |
("Conflicting syntax for parameter: " ^ quote x) (map fst ids); |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
669 |
|
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
670 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
671 |
(* Distinction of assumed vs. derived identifiers. |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
672 |
The former may have axioms relating assumptions of the context to |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
673 |
assumptions of the specification fragment (for locales with |
19780 | 674 |
predicates). The latter have witnesses relating assumptions of the |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
675 |
specification fragment to assumptions of other (assumed) specification |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
676 |
fragments. *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
677 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
678 |
datatype 'a mode = Assumed of 'a | Derived of 'a; |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
679 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
680 |
fun map_mode f (Assumed x) = Assumed (f x) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
681 |
| map_mode f (Derived x) = Derived (f x); |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
682 |
|
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
683 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
684 |
(* flatten expressions *) |
11896 | 685 |
|
12510 | 686 |
local |
12502 | 687 |
|
18137 | 688 |
fun unify_parms ctxt fixed_parms raw_parmss = |
12502 | 689 |
let |
16458 | 690 |
val thy = ProofContext.theory_of ctxt; |
12502 | 691 |
val maxidx = length raw_parmss; |
692 |
val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss; |
|
693 |
||
694 |
fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
695 |
fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
696 |
val parms = fixed_parms @ maps varify_parms idx_parmss; |
12502 | 697 |
|
18137 | 698 |
fun unify T U envir = Sign.typ_unify thy (U, T) envir |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
699 |
handle Type.TUNIFY => |
23418 | 700 |
let |
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset
|
701 |
val T' = Envir.norm_type (fst envir) T; |
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset
|
702 |
val U' = Envir.norm_type (fst envir) U; |
26948 | 703 |
val prt = Syntax.string_of_typ ctxt; |
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset
|
704 |
in |
18137 | 705 |
raise TYPE ("unify_parms: failed to unify types " ^ |
22339
0dc6b45e5662
more precise error message in parameter unification
schirmer
parents:
22300
diff
changeset
|
706 |
prt U' ^ " and " ^ prt T', [U', T'], []) |
18137 | 707 |
end; |
708 |
fun unify_list (T :: Us) = fold (unify T) Us |
|
709 |
| unify_list [] = I; |
|
18952 | 710 |
val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_list parms))) |
18137 | 711 |
(Vartab.empty, maxidx); |
12502 | 712 |
|
19061
ffbbac0261c9
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset
|
713 |
val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms); |
29004 | 714 |
val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier; |
12502 | 715 |
|
716 |
fun inst_parms (i, ps) = |
|
29275
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
717 |
List.foldr OldTerm.add_typ_tfrees [] (map_filter snd ps) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
718 |
|> map_filter (fn (a, S) => |
12502 | 719 |
let val T = Envir.norm_type unifier' (TVar ((a, i), S)) |
18137 | 720 |
in if T = TFree (a, S) then NONE else SOME (a, T) end) |
721 |
|> Symtab.make; |
|
722 |
in map inst_parms idx_parmss end; |
|
12502 | 723 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
724 |
in |
12502 | 725 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
726 |
fun unify_elemss _ _ [] = [] |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
727 |
| unify_elemss _ [] [elems] = [elems] |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
728 |
| unify_elemss ctxt fixed_parms elemss = |
12502 | 729 |
let |
18137 | 730 |
val thy = ProofContext.theory_of ctxt; |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
731 |
val phis = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss) |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
732 |
|> map (Element.instT_morphism thy); |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
733 |
fun inst ((((name, ps), mode), elems), phi) = |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
734 |
(((name, map (apsnd (Option.map (Morphism.typ phi))) ps), |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
735 |
map_mode (map (Element.morph_witness phi)) mode), |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
736 |
map (Element.morph_ctxt phi) elems); |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
737 |
in map inst (elemss ~~ phis) end; |
12502 | 738 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
739 |
|
19810 | 740 |
fun renaming xs parms = zip_options parms xs |
741 |
handle Library.UnequalLengths => |
|
742 |
error ("Too many arguments in renaming: " ^ |
|
743 |
commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs)); |
|
744 |
||
745 |
||
19783 | 746 |
(* params_of_expr: |
747 |
Compute parameters (with types and syntax) of locale expression. |
|
748 |
*) |
|
749 |
||
750 |
fun params_of_expr ctxt fixed_params expr (prev_parms, prev_types, prev_syn) = |
|
751 |
let |
|
752 |
val thy = ProofContext.theory_of ctxt; |
|
753 |
||
754 |
fun merge_tenvs fixed tenv1 tenv2 = |
|
755 |
let |
|
756 |
val [env1, env2] = unify_parms ctxt fixed |
|
757 |
[tenv1 |> Symtab.dest |> map (apsnd SOME), |
|
758 |
tenv2 |> Symtab.dest |> map (apsnd SOME)] |
|
759 |
in |
|
760 |
Symtab.merge (op =) (Symtab.map (Element.instT_type env1) tenv1, |
|
761 |
Symtab.map (Element.instT_type env2) tenv2) |
|
762 |
end; |
|
763 |
||
764 |
fun merge_syn expr syn1 syn2 = |
|
19932 | 765 |
Symtab.merge (op = : mixfix * mixfix -> bool) (syn1, syn2) |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
766 |
handle Symtab.DUP x => err_in_expr ctxt |
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
767 |
("Conflicting syntax for parameter: " ^ quote x) expr; |
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
768 |
|
19783 | 769 |
fun params_of (expr as Locale name) = |
770 |
let |
|
27716 | 771 |
val {params, ...} = the_locale thy name; |
772 |
in (map (fst o fst) params, params |> map fst |> Symtab.make, |
|
773 |
params |> map (apfst fst) |> Symtab.make) end |
|
19783 | 774 |
| params_of (expr as Rename (e, xs)) = |
775 |
let |
|
776 |
val (parms', types', syn') = params_of e; |
|
777 |
val ren = renaming xs parms'; |
|
778 |
(* renaming may reduce number of parameters *) |
|
779 |
val new_parms = map (Element.rename ren) parms' |> distinct (op =); |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28053
diff
changeset
|
780 |
val ren_syn = syn' |> Symtab.dest |> map (Element.rename_var_name ren); |
19783 | 781 |
val new_syn = fold (Symtab.insert (op =)) ren_syn Symtab.empty |
782 |
handle Symtab.DUP x => |
|
783 |
err_in_expr ctxt ("Conflicting syntax for parameter: " ^ quote x) expr; |
|
22700 | 784 |
val syn_types = map (apsnd (fn mx => |
785 |
SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (Syntax.mixfixT mx) 0))))) |
|
786 |
(Symtab.dest new_syn); |
|
19783 | 787 |
val ren_types = types' |> Symtab.dest |> map (apfst (Element.rename ren)); |
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
788 |
val (env :: _) = unify_parms ctxt [] |
19783 | 789 |
((ren_types |> map (apsnd SOME)) :: map single syn_types); |
790 |
val new_types = fold (Symtab.insert (op =)) |
|
791 |
(map (apsnd (Element.instT_type env)) ren_types) Symtab.empty; |
|
792 |
in (new_parms, new_types, new_syn) end |
|
793 |
| params_of (Merge es) = |
|
794 |
fold (fn e => fn (parms, types, syn) => |
|
795 |
let |
|
796 |
val (parms', types', syn') = params_of e |
|
797 |
in |
|
27681 | 798 |
(merge_lists (op =) parms parms', merge_tenvs [] types types', |
19783 | 799 |
merge_syn e syn syn') |
800 |
end) |
|
801 |
es ([], Symtab.empty, Symtab.empty) |
|
802 |
||
803 |
val (parms, types, syn) = params_of expr; |
|
804 |
in |
|
27681 | 805 |
(merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types, |
19783 | 806 |
merge_syn expr prev_syn syn) |
807 |
end; |
|
808 |
||
809 |
fun make_params_ids params = [(("", params), ([], Assumed []))]; |
|
810 |
fun make_raw_params_elemss (params, tenv, syn) = |
|
811 |
[((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []), |
|
812 |
Int [Fixes (map (fn p => |
|
28965 | 813 |
(Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])]; |
19783 | 814 |
|
815 |
||
15596 | 816 |
(* flatten_expr: |
817 |
Extend list of identifiers by those new in locale expression expr. |
|
818 |
Compute corresponding list of lists of locale elements (one entry per |
|
819 |
identifier). |
|
820 |
||
821 |
Identifiers represent locale fragments and are in an extended form: |
|
822 |
((name, ps), (ax_ps, axs)) |
|
823 |
(name, ps) is the locale name with all its parameters. |
|
824 |
(ax_ps, axs) is the locale axioms with its parameters; |
|
825 |
axs are always taken from the top level of the locale hierarchy, |
|
826 |
hence axioms may contain additional parameters from later fragments: |
|
827 |
ps subset of ax_ps. axs is either singleton or empty. |
|
828 |
||
829 |
Elements are enriched by identifier-like information: |
|
830 |
(((name, ax_ps), axs), elems) |
|
831 |
The parameters in ax_ps are the axiom parameters, but enriched by type |
|
832 |
info: now each entry is a pair of string and typ option. Axioms are |
|
833 |
type-instantiated. |
|
834 |
||
835 |
*) |
|
836 |
||
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
837 |
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) = |
12014 | 838 |
let |
839 |
val thy = ProofContext.theory_of ctxt; |
|
12263 | 840 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
841 |
fun rename_parms top ren ((name, ps), (parms, mode)) = |
19783 | 842 |
((name, map (Element.rename ren) ps), |
843 |
if top |
|
844 |
then (map (Element.rename ren) parms, |
|
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
845 |
map_mode (map (Element.morph_witness (Element.rename_morphism ren))) mode) |
19783 | 846 |
else (parms, mode)); |
12263 | 847 |
|
27716 | 848 |
(* add (name, pTs) and its registrations, recursively; adjust hyps of witnesses *) |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
849 |
|
20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
850 |
fun add_with_regs ((name, pTs), mode) (wits, ids, visited) = |
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
851 |
if member (fn (a, (b, _)) => a = b) visited (name, map #1 pTs) |
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
852 |
then (wits, ids, visited) |
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
853 |
else |
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
854 |
let |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
855 |
val {params, regs, ...} = the_locale thy name; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
856 |
val pTs' = map #1 params; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
857 |
val ren = map #1 pTs' ~~ map (fn (x, _) => (x, NONE)) pTs; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
858 |
(* dummy syntax, since required by rename *) |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
859 |
val pTs'' = map (fn ((p, _), (_, T)) => (p, T)) (pTs ~~ pTs'); |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
860 |
val [env] = unify_parms ctxt pTs [map (apsnd SOME) pTs'']; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
861 |
(* propagate parameter types, to keep them consistent *) |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
862 |
val regs' = map (fn ((name, ps), wits) => |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
863 |
((name, map (Element.rename ren) ps), |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
864 |
map (Element.transfer_witness thy) wits)) regs; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
865 |
val new_regs = regs'; |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
866 |
val new_ids = map fst new_regs; |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
867 |
val new_idTs = |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
868 |
map (apsnd (map (fn p => (p, (the o AList.lookup (op =) pTs) p)))) new_ids; |
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
869 |
|
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
870 |
val new_wits = new_regs |> map (#2 #> map |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
871 |
(Element.morph_witness |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
872 |
(Element.instT_morphism thy env $> |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
873 |
Element.rename_morphism ren $> |
25669 | 874 |
Element.satisfy_morphism wits) |
875 |
#> Element.close_witness)); |
|
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
876 |
val new_ids' = map (fn (id, wits) => |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
877 |
(id, ([], Derived wits))) (new_ids ~~ new_wits); |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
878 |
val new_idTs' = map (fn ((n, pTs), (_, ([], mode))) => |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
879 |
((n, pTs), mode)) (new_idTs ~~ new_ids'); |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
880 |
val new_id = ((name, map #1 pTs), ([], mode)); |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
881 |
val (wits', ids', visited') = fold add_with_regs new_idTs' |
20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
882 |
(wits @ flat new_wits, ids, visited @ [new_id]); |
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
883 |
in |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
884 |
(wits', ids' @ [new_id], visited') |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
885 |
end; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
886 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
887 |
(* distribute top-level axioms over assumed ids *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
888 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
889 |
fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
890 |
let |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
891 |
val {elems, ...} = the_locale thy name; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
892 |
val ts = maps |
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
893 |
(fn (Assumes asms, _) => maps (map #1 o #2) asms |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
894 |
| _ => []) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
895 |
elems; |
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset
|
896 |
val (axs1, axs2) = chop (length ts) axioms; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
897 |
in (((name, parms), (all_ps, Assumed axs1)), axs2) end |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
898 |
| axiomify all_ps (id, (_, Derived ths)) axioms = |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
899 |
((id, (all_ps, Derived ths)), axioms); |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
900 |
|
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
901 |
(* identifiers of an expression *) |
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
902 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
903 |
fun identify top (Locale name) = |
15596 | 904 |
(* CB: ids_ax is a list of tuples of the form ((name, ps), axs), |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
905 |
where name is a locale name, ps a list of parameter names and axs |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
906 |
a list of axioms relating to the identifier, axs is empty unless |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
907 |
identify at top level (top = true); |
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
908 |
parms is accumulated list of parameters *) |
12289 | 909 |
let |
27716 | 910 |
val {axiom, params, ...} = the_locale thy name; |
19278 | 911 |
val ps = map (#1 o #1) params; |
27716 | 912 |
val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], [], []); |
20167
fe5fd4fd4114
Strict dfs traversal of imported and registered identifiers.
ballarin
parents:
20092
diff
changeset
|
913 |
val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids''; |
27716 | 914 |
in (ids_ax, ps) end |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
915 |
| identify top (Rename (e, xs)) = |
12273 | 916 |
let |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
917 |
val (ids', parms') = identify top e; |
12839 | 918 |
val ren = renaming xs parms' |
18678 | 919 |
handle ERROR msg => err_in_locale' ctxt msg ids'; |
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
920 |
|
19061
ffbbac0261c9
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19025
diff
changeset
|
921 |
val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
922 |
val parms'' = distinct (op =) (maps (#2 o #1) ids''); |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
923 |
in (ids'', parms'') end |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
924 |
| identify top (Merge es) = |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
925 |
fold (fn e => fn (ids, parms) => |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
926 |
let |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
927 |
val (ids', parms') = identify top e |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
928 |
in |
27681 | 929 |
(merge_alists (op =) ids ids', merge_lists (op =) parms parms') |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
930 |
end) |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
931 |
es ([], []); |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
932 |
|
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
933 |
fun inst_wit all_params (t, th) = let |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
934 |
val {hyps, prop, ...} = Thm.rep_thm th; |
16861 | 935 |
val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []); |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
936 |
val [env] = unify_parms ctxt all_params [ps]; |
18137 | 937 |
val t' = Element.instT_term env t; |
938 |
val th' = Element.instT_thm thy env th; |
|
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
939 |
in (t', th') end; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
940 |
|
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
941 |
fun eval all_params tenv syn ((name, params), (locale_params, mode)) = |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
942 |
let |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
943 |
val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
944 |
val elems = map fst elems_stamped; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
945 |
val ps = map fst ps_mx; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
946 |
fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt); |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
947 |
val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
948 |
val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
949 |
val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
950 |
val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps]; |
28862 | 951 |
val (lprfx, pprfx) = param_prefix name params; |
28941 | 952 |
val add_prefices = pprfx <> "" ? Binding.add_prefix false pprfx |
953 |
#> Binding.add_prefix false lprfx; |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
954 |
val elem_morphism = |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
955 |
Element.rename_morphism ren $> |
28965 | 956 |
Morphism.binding_morphism add_prefices $> |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
957 |
Element.instT_morphism thy env; |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
958 |
val elems' = map (Element.morph_ctxt elem_morphism) elems; |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
959 |
in (((name, map (apsnd SOME) locale_params'), mode'), elems') end; |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
960 |
|
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
961 |
(* parameters, their types and syntax *) |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
962 |
val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty); |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
963 |
val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params'; |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
964 |
(* compute identifiers and syntax, merge with previous ones *) |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
965 |
val (ids, _) = identify true expr; |
20951
868120282837
gen_rem(s) abandoned in favour of remove / subtract
haftmann
parents:
20911
diff
changeset
|
966 |
val idents = subtract (eq_fst (op =)) prev_idents ids; |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
967 |
val syntax = merge_syntax ctxt ids (syn, prev_syntax); |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
968 |
(* type-instantiate elements *) |
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
969 |
val final_elemss = map (eval all_params tenv syntax) idents; |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
970 |
in ((prev_idents @ idents, syntax), final_elemss) end; |
12046 | 971 |
|
12510 | 972 |
end; |
973 |
||
12070 | 974 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
975 |
(* activate elements *) |
12273 | 976 |
|
12510 | 977 |
local |
978 |
||
21686 | 979 |
fun axioms_export axs _ As = |
980 |
(Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); |
|
12263 | 981 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
982 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
983 |
(* NB: derived ids contain only facts at this stage *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
984 |
|
27681 | 985 |
fun activate_elem _ _ (Fixes fixes) (ctxt, mode) = |
986 |
([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode)) |
|
987 |
| activate_elem _ _ (Constrains _) (ctxt, mode) = |
|
988 |
([], (ctxt, mode)) |
|
989 |
| activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) = |
|
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset
|
990 |
let |
18728 | 991 |
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
992 |
val ts = maps (map #1 o #2) asms'; |
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset
|
993 |
val (ps, qs) = chop (length ts) axs; |
17856 | 994 |
val (_, ctxt') = |
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21361
diff
changeset
|
995 |
ctxt |> fold Variable.auto_fixes ts |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
996 |
|> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms'; |
27681 | 997 |
in ([], (ctxt', Assumed qs)) end |
998 |
| activate_elem _ _ (Assumes asms) (ctxt, Derived ths) = |
|
999 |
([], (ctxt, Derived ths)) |
|
1000 |
| activate_elem _ _ (Defines defs) (ctxt, Assumed axs) = |
|
15596 | 1001 |
let |
18728 | 1002 |
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; |
19732 | 1003 |
val asms = defs' |> map (fn ((name, atts), (t, ps)) => |
1004 |
let val ((c, _), t') = LocalDefs.cert_def ctxt t |
|
28965 | 1005 |
in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end); |
17856 | 1006 |
val (_, ctxt') = |
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21361
diff
changeset
|
1007 |
ctxt |> fold (Variable.auto_fixes o #1) asms |
19732 | 1008 |
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); |
27681 | 1009 |
in ([], (ctxt', Assumed axs)) end |
1010 |
| activate_elem _ _ (Defines defs) (ctxt, Derived ths) = |
|
1011 |
([], (ctxt, Derived ths)) |
|
1012 |
| activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) = |
|
15596 | 1013 |
let |
18728 | 1014 |
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; |
28940 | 1015 |
val (res, ctxt') = ctxt |> local_note_qualified kind facts'; |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28053
diff
changeset
|
1016 |
in (if is_ext then (map (#1 o #1) facts' ~~ map #2 res) else [], (ctxt', mode)) end; |
12502 | 1017 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1018 |
fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt = |
17033 | 1019 |
let |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
1020 |
val thy = ProofContext.theory_of ctxt; |
27681 | 1021 |
val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = "")) |
1022 |
elems (ProofContext.qualified_names ctxt, mode) |
|
21441 | 1023 |
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]; |
15696 | 1024 |
val ctxt'' = if name = "" then ctxt' |
1025 |
else let |
|
1026 |
val ps' = map (fn (n, SOME T) => Free (n, T)) ps; |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1027 |
in if test_local_registration ctxt' (name, ps') then ctxt' |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1028 |
else let |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1029 |
val ctxt'' = put_local_registration (name, ps') (I, (NameSpace.base name, "")) |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1030 |
(Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt' |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1031 |
in case mode of |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1032 |
Assumed axs => |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1033 |
fold (add_local_witness (name, ps') o |
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1034 |
Element.assume_witness thy o Element.witness_prop) axs ctxt'' |
25669 | 1035 |
| Derived ths => |
1036 |
fold (add_local_witness (name, ps')) ths ctxt'' |
|
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
1037 |
end |
15696 | 1038 |
end |
16144 | 1039 |
in (ProofContext.restore_naming ctxt ctxt'', res) end; |
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset
|
1040 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1041 |
fun activate_elemss ax_in_ctxt prep_facts = |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1042 |
fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1043 |
let |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1044 |
val elems = map (prep_facts ctxt) raw_elems; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1045 |
val (ctxt', res) = apsnd flat |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1046 |
(activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt); |
21530 | 1047 |
val elems' = elems |> map (Element.map_ctxt_attrib Args.closure); |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1048 |
in (((((name, ps), mode), elems'), res), ctxt') end); |
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset
|
1049 |
|
12546 | 1050 |
in |
1051 |
||
27681 | 1052 |
(* CB: activate_facts prep_facts elemss ctxt, |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1053 |
where elemss is a list of pairs consisting of identifiers and |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1054 |
context elements, extends ctxt by the context elements yielding |
27681 | 1055 |
ctxt' and returns ((elemss', facts), ctxt'). |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1056 |
Identifiers in the argument are of the form ((name, ps), axs) and |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1057 |
assumptions use the axioms in the identifiers to set up exporters |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1058 |
in ctxt'. elemss' does not contain identifiers and is obtained |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1059 |
from elemss and the intermediate context with prep_facts. |
15703 | 1060 |
If read_facts or cert_facts is used for prep_facts, these also remove |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1061 |
the internal/external markers from elemss. *) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1062 |
|
27681 | 1063 |
fun activate_facts ax_in_ctxt prep_facts args = |
1064 |
activate_elemss ax_in_ctxt prep_facts args |
|
1065 |
#>> (apsnd flat o split_list); |
|
15703 | 1066 |
|
12510 | 1067 |
end; |
1068 |
||
12307 | 1069 |
|
15696 | 1070 |
|
18137 | 1071 |
(** prepare locale elements **) |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1072 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1073 |
(* expressions *) |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1074 |
|
16458 | 1075 |
fun intern_expr thy (Locale xname) = Locale (intern thy xname) |
1076 |
| intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs) |
|
1077 |
| intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs); |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1078 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1079 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1080 |
(* propositions and bindings *) |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1081 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1082 |
(* flatten (ctxt, prep_expr) ((ids, syn), expr) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1083 |
normalises expr (which is either a locale |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1084 |
expression or a single context element) wrt. |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1085 |
to the list ids of already accumulated identifiers. |
19783 | 1086 |
It returns ((ids', syn'), elemss) where ids' is an extension of ids |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1087 |
with identifiers generated for expr, and elemss is the list of |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1088 |
context elements generated from expr. |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1089 |
syn and syn' are symtabs mapping parameter names to their syntax. syn' |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1090 |
is an extension of syn. |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1091 |
For details, see flatten_expr. |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1092 |
|
15596 | 1093 |
Additionally, for a locale expression, the elems are grouped into a single |
1094 |
Int; individual context elements are marked Ext. In this case, the |
|
1095 |
identifier-like information of the element is as follows: |
|
1096 |
- for Fixes: (("", ps), []) where the ps have type info NONE |
|
1097 |
- for other elements: (("", []), []). |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1098 |
The implementation of activate_facts relies on identifier names being |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1099 |
empty strings for external elements. |
15596 | 1100 |
*) |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1101 |
|
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1102 |
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let |
29004 | 1103 |
val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))] |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1104 |
in |
18137 | 1105 |
((ids', |
1106 |
merge_syntax ctxt ids' |
|
29004 | 1107 |
(syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes)) |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
1108 |
handle Symtab.DUP x => err_in_locale ctxt |
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23591
diff
changeset
|
1109 |
("Conflicting syntax for parameter: " ^ quote x) |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1110 |
(map #1 ids')), |
29004 | 1111 |
[((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))]) |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1112 |
end |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1113 |
| flatten _ ((ids, syn), Elem elem) = |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1114 |
((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)]) |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1115 |
| flatten (ctxt, prep_expr) ((ids, syn), Expr expr) = |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16028
diff
changeset
|
1116 |
apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr)); |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1117 |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1118 |
local |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1119 |
|
12839 | 1120 |
local |
1121 |
||
27681 | 1122 |
fun declare_int_elem (Fixes fixes) ctxt = |
1123 |
([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) => |
|
1124 |
(x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd) |
|
1125 |
| declare_int_elem _ ctxt = ([], ctxt); |
|
1126 |
||
1127 |
fun declare_ext_elem prep_vars (Fixes fixes) ctxt = |
|
18671 | 1128 |
let val (vars, _) = prep_vars fixes ctxt |
27681 | 1129 |
in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end |
1130 |
| declare_ext_elem prep_vars (Constrains csts) ctxt = |
|
28965 | 1131 |
let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt |
27681 | 1132 |
in ([], ctxt') end |
1133 |
| declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt) |
|
1134 |
| declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt) |
|
1135 |
| declare_ext_elem _ (Notes _) ctxt = ([], ctxt); |
|
1136 |
||
1137 |
fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems |
|
1138 |
of Int es => fold_map declare_int_elem es ctxt |
|
1139 |
| Ext e => declare_ext_elem prep_vars e ctxt |>> single) |
|
1140 |
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]) |
|
1141 |
| declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt); |
|
12727 | 1142 |
|
12839 | 1143 |
in |
1144 |
||
18671 | 1145 |
fun declare_elemss prep_vars fixed_params raw_elemss ctxt = |
12727 | 1146 |
let |
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1147 |
(* CB: fix of type bug of goal in target with context elements. |
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1148 |
Parameters new in context elements must receive types that are |
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1149 |
distinct from types of parameters in target (fixed_params). *) |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1150 |
val ctxt_with_fixed = |
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
1151 |
fold Variable.declare_term (map Free fixed_params) ctxt; |
12727 | 1152 |
val int_elemss = |
1153 |
raw_elemss |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1154 |
|> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE) |
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1155 |
|> unify_elemss ctxt_with_fixed fixed_params; |
27681 | 1156 |
val (raw_elemss', _) = |
1157 |
fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x)) |
|
1158 |
raw_elemss int_elemss; |
|
1159 |
in fold_map (declare_elems prep_vars) raw_elemss' ctxt end; |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1160 |
|
12839 | 1161 |
end; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1162 |
|
12839 | 1163 |
local |
1164 |
||
1165 |
val norm_term = Envir.beta_norm oo Term.subst_atomic; |
|
1166 |
||
16458 | 1167 |
fun abstract_thm thy eq = |
1168 |
Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; |
|
12502 | 1169 |
|
18190 | 1170 |
fun bind_def ctxt (name, ps) eq (xs, env, ths) = |
12839 | 1171 |
let |
18831 | 1172 |
val ((y, T), b) = LocalDefs.abs_def eq; |
13308 | 1173 |
val b' = norm_term env b; |
16458 | 1174 |
val th = abstract_thm (ProofContext.theory_of ctxt) eq; |
13308 | 1175 |
fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)]; |
12839 | 1176 |
in |
28375 | 1177 |
exists (fn (x, _) => x = y) xs andalso |
21962 | 1178 |
err "Attempt to define previously specified variable"; |
1179 |
exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso |
|
1180 |
err "Attempt to redefine variable"; |
|
16861 | 1181 |
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) |
12839 | 1182 |
end; |
12575 | 1183 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1184 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1185 |
(* CB: for finish_elems (Int and Ext), |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1186 |
extracts specification, only of assumed elements *) |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1187 |
|
18190 | 1188 |
fun eval_text _ _ _ (Fixes _) text = text |
1189 |
| eval_text _ _ _ (Constrains _) text = text |
|
1190 |
| eval_text _ (_, Assumed _) is_ext (Assumes asms) |
|
1191 |
(((exts, exts'), (ints, ints')), (xs, env, defs)) = |
|
13394 | 1192 |
let |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1193 |
val ts = maps (map #1 o #2) asms; |
13394 | 1194 |
val ts' = map (norm_term env) ts; |
1195 |
val spec' = |
|
1196 |
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) |
|
1197 |
else ((exts, exts'), (ints @ ts, ints' @ ts')); |
|
16861 | 1198 |
in (spec', (fold Term.add_frees ts' xs, env, defs)) end |
18190 | 1199 |
| eval_text _ (_, Derived _) _ (Assumes _) text = text |
1200 |
| eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) = |
|
1201 |
(spec, fold (bind_def ctxt id o #1 o #2) defs binds) |
|
1202 |
| eval_text _ (_, Derived _) _ (Defines _) text = text |
|
1203 |
| eval_text _ _ _ (Notes _) text = text; |
|
13308 | 1204 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1205 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1206 |
(* for finish_elems (Int), |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1207 |
remove redundant elements of derived identifiers, |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1208 |
turn assumptions and definitions into facts, |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1209 |
satisfy hypotheses of facts *) |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1210 |
|
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1211 |
fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes) |
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1212 |
| finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts) |
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1213 |
| finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms) |
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1214 |
| finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs) |
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1215 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1216 |
| finish_derived _ _ (Derived _) (Fixes _) = NONE |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1217 |
| finish_derived _ _ (Derived _) (Constrains _) = NONE |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1218 |
| finish_derived sign satisfy (Derived _) (Assumes asms) = asms |
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1219 |
|> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], [])))) |
21441 | 1220 |
|> pair Thm.assumptionK |> Notes |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1221 |
|> Element.morph_ctxt satisfy |> SOME |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1222 |
| finish_derived sign satisfy (Derived _) (Defines defs) = defs |
17096
8327b71282ce
Improved generation of witnesses in interpretation.
ballarin
parents:
17033
diff
changeset
|
1223 |
|> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])])) |
21441 | 1224 |
|> pair Thm.definitionK |> Notes |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1225 |
|> Element.morph_ctxt satisfy |> SOME |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1226 |
|
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1227 |
| finish_derived _ satisfy _ (Notes facts) = Notes facts |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1228 |
|> Element.morph_ctxt satisfy |> SOME; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1229 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1230 |
(* CB: for finish_elems (Ext) *) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1231 |
|
13308 | 1232 |
fun closeup _ false elem = elem |
1233 |
| closeup ctxt true elem = |
|
12839 | 1234 |
let |
13308 | 1235 |
fun close_frees t = |
26206 | 1236 |
let |
1237 |
val rev_frees = |
|
1238 |
Term.fold_aterms (fn Free (x, T) => |
|
1239 |
if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t []; |
|
26299
2f387f5c0f52
closeup: recover original order of free variables!
wenzelm
parents:
26206
diff
changeset
|
1240 |
in Term.list_all_free (rev rev_frees, t) end; |
13308 | 1241 |
|
1242 |
fun no_binds [] = [] |
|
18678 | 1243 |
| no_binds _ = error "Illegal term bindings in locale element"; |
13308 | 1244 |
in |
1245 |
(case elem of |
|
1246 |
Assumes asms => Assumes (asms |> map (fn (a, propps) => |
|
19585 | 1247 |
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) |
13308 | 1248 |
| Defines defs => Defines (defs |> map (fn (a, (t, ps)) => |
18831 | 1249 |
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) |
13308 | 1250 |
| e => e) |
1251 |
end; |
|
12839 | 1252 |
|
12502 | 1253 |
|
28862 | 1254 |
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) => |
29004 | 1255 |
let val x = Binding.base_name b |
28862 | 1256 |
in (b, AList.lookup (op =) parms x, mx) end) fixes) |
18899
a8e913c93578
theorem(_in_locale): Element.statement, Obtain.statement;
wenzelm
parents:
18890
diff
changeset
|
1257 |
| finish_ext_elem parms _ (Constrains _, _) = Constrains [] |
12839 | 1258 |
| finish_ext_elem _ close (Assumes asms, propp) = |
1259 |
close (Assumes (map #1 asms ~~ propp)) |
|
1260 |
| finish_ext_elem _ close (Defines defs, propp) = |
|
19585 | 1261 |
close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp)) |
12839 | 1262 |
| finish_ext_elem _ _ (Notes facts, _) = Notes facts; |
1263 |
||
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1264 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1265 |
(* CB: finish_parms introduces type info from parms to identifiers *) |
15531 | 1266 |
(* CB: only needed for types that have been NONE so far??? |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1267 |
If so, which are these??? *) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1268 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1269 |
fun finish_parms parms (((name, ps), mode), elems) = |
19932 | 1270 |
(((name, map (fn (x, _) => (x, AList.lookup (op = : string * string -> bool) parms x)) ps), mode), elems); |
12839 | 1271 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1272 |
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) = |
12839 | 1273 |
let |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1274 |
val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1275 |
val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; |
18190 | 1276 |
val text' = fold (eval_text ctxt id' false) es text; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1277 |
val es' = map_filter |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1278 |
(finish_derived (ProofContext.theory_of ctxt) (Element.satisfy_morphism wits') mode) es; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1279 |
in ((text', wits'), (id', map Int es')) end |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1280 |
| finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = |
13308 | 1281 |
let |
1282 |
val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp); |
|
18190 | 1283 |
val text' = eval_text ctxt id true e' text; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1284 |
in ((text', wits), (id, [Ext e'])) end |
12839 | 1285 |
|
1286 |
in |
|
12510 | 1287 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1288 |
(* CB: only called by prep_elemss *) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1289 |
|
13375 | 1290 |
fun finish_elemss ctxt parms do_close = |
1291 |
foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close); |
|
12839 | 1292 |
|
1293 |
end; |
|
1294 |
||
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1295 |
|
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1296 |
(* Remove duplicate Defines elements: temporary workaround to fix Afp/Category. *) |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1297 |
|
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1298 |
fun defs_ord (defs1, defs2) = |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1299 |
list_ord (fn ((_, (d1, _)), (_, (d2, _))) => |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29004
diff
changeset
|
1300 |
TermOrd.fast_term_ord (d1, d2)) (defs1, defs2); |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1301 |
structure Defstab = |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
1302 |
TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord); |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1303 |
|
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1304 |
fun rem_dup_defs es ds = |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1305 |
fold_map (fn e as (Defines defs) => (fn ds => |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1306 |
if Defstab.defined ds defs |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1307 |
then (Defines [], ds) |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1308 |
else (e, Defstab.update (defs, ()) ds)) |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1309 |
| e => (fn ds => (e, ds))) es ds; |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1310 |
fun rem_dup_elemss (Int es) ds = apfst Int (rem_dup_defs es ds) |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1311 |
| rem_dup_elemss (Ext e) ds = (Ext e, ds); |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1312 |
fun rem_dup_defines raw_elemss = |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1313 |
fold_map (fn (id as (_, (Assumed _)), es) => (fn ds => |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1314 |
apfst (pair id) (rem_dup_elemss es ds)) |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1315 |
| (id as (_, (Derived _)), es) => (fn ds => |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1316 |
((id, es), ds))) raw_elemss Defstab.empty |> #1; |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1317 |
|
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1318 |
(* CB: type inference and consistency checks for locales. |
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1319 |
|
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1320 |
Works by building a context (through declare_elemss), extracting the |
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1321 |
required information and adjusting the context elements (finish_elemss). |
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1322 |
Can also universally close free vars in assms and defs. This is only |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1323 |
needed for Ext elements and controlled by parameter do_close. |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1324 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1325 |
Only elements of assumed identifiers are considered. |
16736
1e792b32abef
Preparations for interpretation of locales in locales.
ballarin
parents:
16620
diff
changeset
|
1326 |
*) |
15127 | 1327 |
|
18671 | 1328 |
fun prep_elemss prep_vars prepp do_close context fixed_params raw_elemss raw_concl = |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1329 |
let |
15127 | 1330 |
(* CB: contexts computed in the course of this function are discarded. |
1331 |
They are used for type inference and consistency checks only. *) |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1332 |
(* CB: fixed_params are the parameters (with types) of the target locale, |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1333 |
empty list if there is no target. *) |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1334 |
(* CB: raw_elemss are list of pairs consisting of identifiers and |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1335 |
context elements, the latter marked as internal or external. *) |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1336 |
val raw_elemss = rem_dup_defines raw_elemss; |
27681 | 1337 |
val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context; |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1338 |
(* CB: raw_ctxt is context with additional fixed variables derived from |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1339 |
the fixes elements in raw_elemss, |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1340 |
raw_proppss contains assumptions and definitions from the |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1341 |
external elements in raw_elemss. *) |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1342 |
fun prep_prop raw_propp (raw_ctxt, raw_concl) = |
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1343 |
let |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1344 |
(* CB: add type information from fixed_params to context (declare_term) *) |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1345 |
(* CB: process patterns (conclusion and external elements only) *) |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1346 |
val (ctxt, all_propp) = |
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
1347 |
prepp (fold Variable.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); |
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1348 |
(* CB: add type information from conclusion and external elements to context *) |
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
1349 |
val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt; |
18450
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1350 |
(* CB: resolve schematic variables (patterns) in conclusion and external elements. *) |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1351 |
val all_propp' = map2 (curry (op ~~)) |
e57731ba01dd
discontinued unflat in favour of burrow and burrow_split
haftmann
parents:
18421
diff
changeset
|
1352 |
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); |
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset
|
1353 |
val (concl, propp) = chop (length raw_concl) all_propp'; |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1354 |
in (propp, (ctxt, concl)) end |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1355 |
|
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1356 |
val (proppss, (ctxt, concl)) = |
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1357 |
(fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl); |
12502 | 1358 |
|
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1359 |
(* CB: obtain all parameters from identifier part of raw_elemss *) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1360 |
val xs = map #1 (params_of' raw_elemss); |
12727 | 1361 |
val typing = unify_frozen ctxt 0 |
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
1362 |
(map (Variable.default_type raw_ctxt) xs) |
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19873
diff
changeset
|
1363 |
(map (Variable.default_type ctxt) xs); |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1364 |
val parms = param_types (xs ~~ typing); |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1365 |
(* CB: parms are the parameters from raw_elemss, with correct typing. *) |
12273 | 1366 |
|
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1367 |
(* CB: extract information from assumes and defines elements |
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
1368 |
(fixes, constrains and notes in raw_elemss don't have an effect on |
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
1369 |
text and elemss), compute final form of context elements. *) |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1370 |
val ((text, _), elemss) = finish_elemss ctxt parms do_close |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1371 |
((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss); |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1372 |
(* CB: text has the following structure: |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1373 |
(((exts, exts'), (ints, ints')), (xs, env, defs)) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1374 |
where |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1375 |
exts: external assumptions (terms in external assumes elements) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1376 |
exts': dito, normalised wrt. env |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1377 |
ints: internal assumptions (terms in internal assumes elements) |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1378 |
ints': dito, normalised wrt. env |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1379 |
xs: the free variables in exts' and ints' and rhss of definitions, |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1380 |
this includes parameters except defined parameters |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1381 |
env: list of term pairs encoding substitutions, where the first term |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1382 |
is a free variable; substitutions represent defines elements and |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1383 |
the rhs is normalised wrt. the previous env |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1384 |
defs: theorems representing the substitutions from defines elements |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1385 |
(thms are normalised wrt. env). |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1386 |
elemss is an updated version of raw_elemss: |
16169
b59202511b8a
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16144
diff
changeset
|
1387 |
- type info added to Fixes and modified in Constrains |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1388 |
- axiom and definition statement replaced by corresponding one |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1389 |
from proppss in Assumes and Defines |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1390 |
- Facts unchanged |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1391 |
*) |
13308 | 1392 |
in ((parms, elemss, concl), text) end; |
12502 | 1393 |
|
1394 |
in |
|
1395 |
||
18671 | 1396 |
fun read_elemss x = prep_elemss ProofContext.read_vars ProofContext.read_propp_schematic x; |
1397 |
fun cert_elemss x = prep_elemss ProofContext.cert_vars ProofContext.cert_propp_schematic x; |
|
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1398 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1399 |
end; |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1400 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1401 |
|
15703 | 1402 |
(* facts and attributes *) |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1403 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1404 |
local |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1405 |
|
20965 | 1406 |
fun check_name name = |
18678 | 1407 |
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) |
15703 | 1408 |
else name; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1409 |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
1410 |
fun prep_facts _ _ _ ctxt (Int elem) = elem |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
1411 |
|> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt))) |
20965 | 1412 |
| prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt |
15703 | 1413 |
{var = I, typ = I, term = I, |
28965 | 1414 |
binding = Binding.map_base prep_name, |
15703 | 1415 |
fact = get ctxt, |
16458 | 1416 |
attrib = Args.assignable o intern (ProofContext.theory_of ctxt)}; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1417 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1418 |
in |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1419 |
|
26345
f70620a4cf81
renamed former get_thms(_silent) to get_fact(_silent);
wenzelm
parents:
26299
diff
changeset
|
1420 |
fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x; |
20965 | 1421 |
fun cert_facts x = prep_facts I (K I) (K I) x; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1422 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1423 |
end; |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1424 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1425 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1426 |
(* Get the specification of a locale *) |
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1427 |
|
19780 | 1428 |
(*The global specification is made from the parameters and global |
1429 |
assumptions, the local specification from the parameters and the |
|
1430 |
local assumptions.*) |
|
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1431 |
|
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1432 |
local |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1433 |
|
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1434 |
fun gen_asms_of get thy name = |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1435 |
let |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1436 |
val ctxt = ProofContext.init thy; |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1437 |
val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name)); |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1438 |
val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss []; |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1439 |
in |
18890 | 1440 |
elemss |> get |
19780 | 1441 |
|> maps (fn (_, es) => map (fn Int e => e) es) |
1442 |
|> maps (fn Assumes asms => asms | _ => []) |
|
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1443 |
|> map (apsnd (map fst)) |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1444 |
end; |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1445 |
|
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1446 |
in |
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1447 |
|
25619 | 1448 |
fun parameters_of thy = #params o the_locale thy; |
1449 |
||
1450 |
fun intros thy = #intros o the_locale thy; |
|
1451 |
(*returns introduction rule for delta predicate and locale predicate |
|
1452 |
as a pair of singleton lists*) |
|
1453 |
||
1454 |
fun dests thy = #dests o the_locale thy; |
|
1455 |
||
27709 | 1456 |
fun facts_of thy = map_filter (fn (Element.Notes (_, facts), _) => SOME facts |
1457 |
| _ => NONE) o #elems o the_locale thy; |
|
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1458 |
|
19276 | 1459 |
fun parameters_of_expr thy expr = |
1460 |
let |
|
1461 |
val ctxt = ProofContext.init thy; |
|
19783 | 1462 |
val pts = params_of_expr ctxt [] (intern_expr thy expr) |
1463 |
([], Symtab.empty, Symtab.empty); |
|
1464 |
val raw_params_elemss = make_raw_params_elemss pts; |
|
19276 | 1465 |
val ((_, syn), raw_elemss) = flatten (ctxt, intern_expr thy) |
1466 |
(([], Symtab.empty), Expr expr); |
|
19783 | 1467 |
val ((parms, _, _), _) = |
1468 |
read_elemss false ctxt [] (raw_params_elemss @ raw_elemss) []; |
|
19276 | 1469 |
in map (fn p as (n, _) => (p, Symtab.lookup syn n |> the)) parms end; |
1470 |
||
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1471 |
fun local_asms_of thy name = |
18890 | 1472 |
gen_asms_of (single o Library.last_elem) thy name; |
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1473 |
|
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1474 |
fun global_asms_of thy name = |
18890 | 1475 |
gen_asms_of I thy name; |
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1476 |
|
19780 | 1477 |
end; |
18795
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1478 |
|
303793f49b0f
Interface to access the specification of a named locale.
ballarin
parents:
18782
diff
changeset
|
1479 |
|
22573 | 1480 |
(* full context statements: imports + elements + conclusion *) |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1481 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1482 |
local |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1483 |
|
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1484 |
fun prep_context_statement prep_expr prep_elemss prep_facts |
22573 | 1485 |
do_close fixed_params imports elements raw_concl context = |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1486 |
let |
16458 | 1487 |
val thy = ProofContext.theory_of context; |
13375 | 1488 |
|
19783 | 1489 |
val (import_params, import_tenv, import_syn) = |
22573 | 1490 |
params_of_expr context fixed_params (prep_expr thy imports) |
19783 | 1491 |
([], Symtab.empty, Symtab.empty); |
1492 |
val includes = map_filter (fn Expr e => SOME e | Elem _ => NONE) elements; |
|
1493 |
val (incl_params, incl_tenv, incl_syn) = fold (params_of_expr context fixed_params) |
|
1494 |
(map (prep_expr thy) includes) (import_params, import_tenv, import_syn); |
|
1495 |
||
1496 |
val ((import_ids, _), raw_import_elemss) = |
|
22573 | 1497 |
flatten (context, prep_expr thy) (([], Symtab.empty), Expr imports); |
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1498 |
(* CB: normalise "includes" among elements *) |
16458 | 1499 |
val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy)) |
19783 | 1500 |
((import_ids, incl_syn), elements); |
15696 | 1501 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1502 |
val raw_elemss = flat raw_elemsss; |
14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1503 |
(* CB: raw_import_elemss @ raw_elemss is the normalised list of |
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14446
diff
changeset
|
1504 |
context elements obtained from import and elements. *) |
19783 | 1505 |
(* Now additional elements for parameters are inserted. *) |
1506 |
val import_params_ids = make_params_ids import_params; |
|
1507 |
val incl_params_ids = |
|
1508 |
make_params_ids (incl_params \\ import_params); |
|
1509 |
val raw_import_params_elemss = |
|
1510 |
make_raw_params_elemss (import_params, incl_tenv, incl_syn); |
|
1511 |
val raw_incl_params_elemss = |
|
1512 |
make_raw_params_elemss (incl_params \\ import_params, incl_tenv, incl_syn); |
|
13375 | 1513 |
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close |
19783 | 1514 |
context fixed_params |
1515 |
(raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl; |
|
1516 |
||
15696 | 1517 |
(* replace extended ids (for axioms) by ids *) |
19783 | 1518 |
val (import_ids', incl_ids) = chop (length import_ids) ids; |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
1519 |
val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1520 |
val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) => |
17485 | 1521 |
(((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems)) |
20035
80c79876d2de
Internal restructuring: identify no longer computes syntax.
ballarin
parents:
20032
diff
changeset
|
1522 |
(all_ids ~~ all_elemss); |
19783 | 1523 |
(* CB: all_elemss and parms contain the correct parameter types *) |
15696 | 1524 |
|
19783 | 1525 |
val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss'; |
27681 | 1526 |
val ((import_elemss, _), import_ctxt) = |
1527 |
activate_facts false prep_facts ps context; |
|
1528 |
||
1529 |
val ((elemss, _), ctxt) = |
|
1530 |
activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt); |
|
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset
|
1531 |
in |
19783 | 1532 |
((((import_ctxt, import_elemss), (ctxt, elemss, syn)), |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
1533 |
(parms, spec, defs)), concl) |
12834
e5bec3268932
added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents:
12806
diff
changeset
|
1534 |
end; |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1535 |
|
18806 | 1536 |
fun prep_statement prep_locale prep_ctxt raw_locale elems concl ctxt = |
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1537 |
let |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1538 |
val thy = ProofContext.theory_of ctxt; |
16458 | 1539 |
val locale = Option.map (prep_locale thy) raw_locale; |
22573 | 1540 |
val (fixed_params, imports) = |
18806 | 1541 |
(case locale of |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1542 |
NONE => ([], empty) |
15531 | 1543 |
| SOME name => |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1544 |
let val {params = ps, ...} = the_locale thy name |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1545 |
in (map fst ps, Locale name) end); |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
1546 |
val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') = |
28710 | 1547 |
prep_ctxt false fixed_params imports (map Elem elems) concl ctxt; |
19991
0c9650664d47
Locales no longer generate views. The following functions have changed
ballarin
parents:
19984
diff
changeset
|
1548 |
in (locale, locale_ctxt, elems_ctxt, concl') end; |
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset
|
1549 |
|
22573 | 1550 |
fun prep_expr prep imports body ctxt = |
19780 | 1551 |
let |
22573 | 1552 |
val (((_, import_elemss), (ctxt', elemss, _)), _) = prep imports body ctxt; |
19780 | 1553 |
val all_elems = maps snd (import_elemss @ elemss); |
1554 |
in (all_elems, ctxt') end; |
|
1555 |
||
12529
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1556 |
in |
d99716a53f59
simultaneous type-inference of complete context/statement specifications;
wenzelm
parents:
12514
diff
changeset
|
1557 |
|
18806 | 1558 |
val read_ctxt = prep_context_statement intern_expr read_elemss read_facts; |
1559 |
val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts; |
|
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13629
diff
changeset
|
1560 |
|
22573 | 1561 |
fun read_context imports body ctxt = #1 (read_ctxt true [] imports (map Elem body) [] ctxt); |
1562 |
fun cert_context imports body ctxt = #1 (cert_ctxt true [] imports (map Elem body) [] ctxt); |
|
12502 | 1563 |
|
19780 | 1564 |
val read_expr = prep_expr read_context; |
1565 |
val cert_expr = prep_expr cert_context; |
|
1566 |
||
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1567 |
fun read_context_statement loc = prep_statement (K I) read_ctxt loc; |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1568 |
fun read_context_statement_cmd loc = prep_statement intern read_ctxt loc; |
21035 | 1569 |
fun cert_context_statement loc = prep_statement (K I) cert_ctxt loc; |
18806 | 1570 |
|
12502 | 1571 |
end; |
11896 | 1572 |
|
1573 |
||
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1574 |
(* init *) |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1575 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1576 |
fun init loc = |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1577 |
ProofContext.init |
25669 | 1578 |
#> #2 o cert_context_statement (SOME loc) [] []; |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1579 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1580 |
|
13336 | 1581 |
(* print locale *) |
12070 | 1582 |
|
22573 | 1583 |
fun print_locale thy show_facts imports body = |
1584 |
let val (all_elems, ctxt) = read_expr imports body (ProofContext.init thy) in |
|
18137 | 1585 |
Pretty.big_list "locale elements:" (all_elems |
17316 | 1586 |
|> (if show_facts then I else filter (fn Notes _ => false | _ => true)) |
21701 | 1587 |
|> map (Element.pretty_ctxt ctxt) |> filter_out null |
1588 |
|> map Pretty.chunks) |
|
13336 | 1589 |
|> Pretty.writeln |
12277 | 1590 |
end; |
12070 | 1591 |
|
1592 |
||
12706 | 1593 |
|
16144 | 1594 |
(** store results **) |
12702 | 1595 |
|
23918 | 1596 |
(* join equations of an id with already accumulated ones *) |
1597 |
||
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1598 |
fun join_eqns get_reg id eqns = |
23918 | 1599 |
let |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1600 |
val eqns' = case get_reg id |
23918 | 1601 |
of NONE => eqns |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1602 |
| SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns') |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1603 |
(* prefer equations from eqns' *) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1604 |
in ((id, eqns'), eqns') end; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1605 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1606 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1607 |
(* collect witnesses and equations up to a particular target for a |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
1608 |
registration; requires parameters and flattened list of identifiers |
17138 | 1609 |
instead of recomputing it from the target *) |
1610 |
||
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1611 |
fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1612 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1613 |
val thy = ProofContext.theory_of ctxt; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1614 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1615 |
val ts = map (var_inst_term (impT, imp)) ext_ts; |
17138 | 1616 |
val (parms, parmTs) = split_list parms; |
19810 | 1617 |
val parmvTs = map Logic.varifyT parmTs; |
17138 | 1618 |
val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty; |
1619 |
val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) |
|
18137 | 1620 |
|> Symtab.make; |
17138 | 1621 |
val inst = Symtab.make (parms ~~ ts); |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1622 |
|
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1623 |
(* instantiate parameter names in ids *) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1624 |
val ext_inst = Symtab.make (parms ~~ ext_ts); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1625 |
fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1626 |
val inst_ids = map (apfst (apsnd ext_inst_names)) ids; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1627 |
val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1628 |
val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids; |
23918 | 1629 |
val eqns = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1630 |
fold_map (join_eqns (get_local_registration ctxt imprt)) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1631 |
(map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd; |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1632 |
in ((tinst, inst), wits, eqns) end; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1633 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1634 |
|
28739 | 1635 |
(* compute and apply morphism *) |
1636 |
||
28862 | 1637 |
fun name_morph phi_name (lprfx, pprfx) b = |
1638 |
b |
|
28965 | 1639 |
|> (if not (Binding.is_empty b) andalso pprfx <> "" |
28941 | 1640 |
then Binding.add_prefix false pprfx else I) |
28965 | 1641 |
|> (if not (Binding.is_empty b) |
28941 | 1642 |
then Binding.add_prefix false lprfx else I) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1643 |
|> phi_name; |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1644 |
|
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1645 |
fun inst_morph thy phi_name param_prfx insts prems eqns export = |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1646 |
let |
28259 | 1647 |
(* standardise export morphism *) |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1648 |
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1649 |
val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1650 |
(* FIXME sync with exp_fact *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1651 |
val exp_typ = Logic.type_map exp_term; |
28259 | 1652 |
val export' = |
28965 | 1653 |
Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
28259 | 1654 |
in |
28965 | 1655 |
Morphism.binding_morphism (name_morph phi_name param_prfx) $> |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1656 |
Element.inst_morphism thy insts $> |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1657 |
Element.satisfy_morphism prems $> |
28259 | 1658 |
Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $> |
1659 |
Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns) $> |
|
1660 |
export' |
|
1661 |
end; |
|
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
1662 |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1663 |
fun activate_note thy phi_name param_prfx attrib insts prems eqns exp = |
28739 | 1664 |
(Element.facts_map o Element.morph_ctxt) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1665 |
(inst_morph thy phi_name param_prfx insts prems eqns exp) |
28792 | 1666 |
#> Attrib.map_facts attrib; |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
1667 |
|
28259 | 1668 |
|
1669 |
(* public interface to interpretation morphism *) |
|
1670 |
||
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1671 |
fun get_interpret_morph thy phi_name param_prfx (exp, imp) target ext_ts = |
28259 | 1672 |
let |
1673 |
val parms = the_locale thy target |> #params |> map fst; |
|
1674 |
val ids = flatten (ProofContext.init thy, intern_expr thy) |
|
1675 |
(([], Symtab.empty), Expr (Locale target)) |> fst |> fst; |
|
1676 |
val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
|
1677 |
in |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1678 |
inst_morph thy phi_name param_prfx insts prems eqns exp |
28259 | 1679 |
end; |
17138 | 1680 |
|
15696 | 1681 |
(* store instantiations of args for all registered interpretations |
1682 |
of the theory *) |
|
1683 |
||
21441 | 1684 |
fun note_thmss_registrations target (kind, args) thy = |
15596 | 1685 |
let |
19278 | 1686 |
val parms = the_locale thy target |> #params |> map fst; |
16458 | 1687 |
val ids = flatten (ProofContext.init thy, intern_expr thy) |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
1688 |
(([], Symtab.empty), Expr (Locale target)) |> fst |> fst; |
15696 | 1689 |
|
1690 |
val regs = get_global_registrations thy target; |
|
1691 |
(* add args to thy for all registrations *) |
|
15596 | 1692 |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1693 |
fun activate (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = |
15696 | 1694 |
let |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
1695 |
val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts; |
28053 | 1696 |
val args' = args |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
1697 |
|> activate_note thy phi_name param_prfx |
28739 | 1698 |
(Attrib.attribute_i thy) insts prems eqns exp; |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
1699 |
in |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
1700 |
thy |
28940 | 1701 |
|> global_note_qualified kind args' |
1702 |
|> snd |
|
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
1703 |
end; |
18190 | 1704 |
in fold activate regs thy end; |
15596 | 1705 |
|
1706 |
||
20911 | 1707 |
(* locale results *) |
12958 | 1708 |
|
21441 | 1709 |
fun add_thmss loc kind args ctxt = |
12706 | 1710 |
let |
27681 | 1711 |
val (([(_, [Notes args'])], _), ctxt') = |
21441 | 1712 |
activate_facts true cert_facts |
27681 | 1713 |
[((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt; |
20911 | 1714 |
val ctxt'' = ctxt' |> ProofContext.theory |
1715 |
(change_locale loc |
|
27716 | 1716 |
(fn (axiom, elems, params, decls, regs, intros, dests) => |
1717 |
(axiom, elems @ [(Notes args', stamp ())], |
|
1718 |
params, decls, regs, intros, dests)) |
|
21441 | 1719 |
#> note_thmss_registrations loc args'); |
21582 | 1720 |
in ctxt'' end; |
15703 | 1721 |
|
11896 | 1722 |
|
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1723 |
(* declarations *) |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1724 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1725 |
local |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1726 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1727 |
fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi)); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1728 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1729 |
fun add_decls add loc decl = |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1730 |
ProofContext.theory (change_locale loc |
27716 | 1731 |
(fn (axiom, elems, params, decls, regs, intros, dests) => |
1732 |
(axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #> |
|
24006 | 1733 |
add_thmss loc Thm.internalK |
28965 | 1734 |
[((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])]; |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1735 |
|
23418 | 1736 |
in |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1737 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1738 |
val add_type_syntax = add_decls (apfst o cons); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1739 |
val add_term_syntax = add_decls (apsnd o cons); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1740 |
val add_declaration = add_decls (K I); |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1741 |
|
28691 | 1742 |
fun declarations_of thy loc = |
1743 |
the_locale thy loc |> #decls |> apfst (map fst) |> apsnd (map fst); |
|
1744 |
||
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1745 |
end; |
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1746 |
|
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1747 |
|
18137 | 1748 |
|
1749 |
(** define locales **) |
|
1750 |
||
13336 | 1751 |
(* predicate text *) |
15596 | 1752 |
(* CB: generate locale predicates and delta predicates *) |
13336 | 1753 |
|
13375 | 1754 |
local |
1755 |
||
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1756 |
(* introN: name of theorems for introduction rules of locale and |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1757 |
delta predicates; |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1758 |
axiomsN: name of theorem set with destruct rules for locale predicates, |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1759 |
also name suffix of delta predicates. *) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1760 |
|
13375 | 1761 |
val introN = "intro"; |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1762 |
val axiomsN = "axioms"; |
13375 | 1763 |
|
16458 | 1764 |
fun atomize_spec thy ts = |
13375 | 1765 |
let |
23418 | 1766 |
val t = Logic.mk_conjunction_balanced ts; |
16458 | 1767 |
val body = ObjectLogic.atomize_term thy t; |
13375 | 1768 |
val bodyT = Term.fastype_of body; |
1769 |
in |
|
16458 | 1770 |
if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) |
23591 | 1771 |
else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t)) |
13375 | 1772 |
end; |
1773 |
||
25073
13db30d367d2
locale pred: authentic syntax, tuned aprop_tr' accordingly;
wenzelm
parents:
25067
diff
changeset
|
1774 |
fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => |
13db30d367d2
locale pred: authentic syntax, tuned aprop_tr' accordingly;
wenzelm
parents:
25067
diff
changeset
|
1775 |
if length args = n then |
13db30d367d2
locale pred: authentic syntax, tuned aprop_tr' accordingly;
wenzelm
parents:
25067
diff
changeset
|
1776 |
Syntax.const "_aprop" $ |
13db30d367d2
locale pred: authentic syntax, tuned aprop_tr' accordingly;
wenzelm
parents:
25067
diff
changeset
|
1777 |
Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) |
13394 | 1778 |
else raise Match); |
13336 | 1779 |
|
15104 | 1780 |
(* CB: define one predicate including its intro rule and axioms |
1781 |
- bname: predicate name |
|
1782 |
- parms: locale parameters |
|
1783 |
- defs: thms representing substitutions from defines elements |
|
1784 |
- ts: terms representing locale assumptions (not normalised wrt. defs) |
|
1785 |
- norm_ts: terms representing locale assumptions (normalised wrt. defs) |
|
1786 |
- thy: the theory |
|
1787 |
*) |
|
1788 |
||
13420 | 1789 |
fun def_pred bname parms defs ts norm_ts thy = |
13375 | 1790 |
let |
28965 | 1791 |
val name = Sign.full_bname thy bname; |
13375 | 1792 |
|
16458 | 1793 |
val (body, bodyT, body_eq) = atomize_spec thy norm_ts; |
29275
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
1794 |
val env = Term.add_free_names body []; |
20664 | 1795 |
val xs = filter (member (op =) env o #1) parms; |
13394 | 1796 |
val Ts = map #2 xs; |
29275
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
1797 |
val extraTs = |
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
1798 |
(Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts []) |
13394 | 1799 |
|> Library.sort_wrt #1 |> map TFree; |
13399
c136276dc847
support locale ``views'' (for cumulative predicates);
wenzelm
parents:
13394
diff
changeset
|
1800 |
val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; |
13336 | 1801 |
|
13394 | 1802 |
val args = map Logic.mk_type extraTs @ map Free xs; |
1803 |
val head = Term.list_comb (Const (name, predT), args); |
|
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
1804 |
val statement = ObjectLogic.ensure_propT thy head; |
13375 | 1805 |
|
18358 | 1806 |
val ([pred_def], defs_thy) = |
13375 | 1807 |
thy |
25073
13db30d367d2
locale pred: authentic syntax, tuned aprop_tr' accordingly;
wenzelm
parents:
25067
diff
changeset
|
1808 |
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |
28965 | 1809 |
|> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd |
27692 | 1810 |
|> PureThy.add_defs false |
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27761
diff
changeset
|
1811 |
[((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; |
20059 | 1812 |
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; |
13394 | 1813 |
|
16458 | 1814 |
val cert = Thm.cterm_of defs_thy; |
13375 | 1815 |
|
20059 | 1816 |
val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
21708 | 1817 |
MetaSimplifier.rewrite_goals_tac [pred_def] THEN |
13375 | 1818 |
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
23418 | 1819 |
Tactic.compose_tac (false, |
1820 |
Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
|
13375 | 1821 |
|
1822 |
val conjuncts = |
|
19423 | 1823 |
(Drule.equal_elim_rule2 OF [body_eq, |
21708 | 1824 |
MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
23418 | 1825 |
|> Conjunction.elim_balanced (length ts); |
17257
0ab67cb765da
introduced binding priority 1 for linear combinators etc.
haftmann
parents:
17228
diff
changeset
|
1826 |
val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
20059 | 1827 |
Element.prove_witness defs_ctxt t |
21708 | 1828 |
(MetaSimplifier.rewrite_goals_tac defs THEN |
13375 | 1829 |
Tactic.compose_tac (false, ax, 0) 1)); |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1830 |
in ((statement, intro, axioms), defs_thy) end; |
13375 | 1831 |
|
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1832 |
fun assumes_to_notes (Assumes asms) axms = |
21441 | 1833 |
fold_map (fn (a, spec) => fn axs => |
1834 |
let val (ps, qs) = chop (length spec) axs |
|
1835 |
in ((a, [(ps, [])]), qs) end) asms axms |
|
1836 |
|> apfst (curry Notes Thm.assumptionK) |
|
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1837 |
| assumes_to_notes e axms = (e, axms); |
13394 | 1838 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1839 |
(* CB: the following two change only "new" elems, these have identifier ("", _). *) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1840 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1841 |
(* turn Assumes into Notes elements *) |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1842 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1843 |
fun change_assumes_elemss axioms elemss = |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1844 |
let |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1845 |
val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1846 |
fun change (id as ("", _), es) = |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1847 |
fold_map assumes_to_notes (map satisfy es) |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1848 |
#-> (fn es' => pair (id, es')) |
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1849 |
| change e = pair e; |
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1850 |
in |
19780 | 1851 |
fst (fold_map change elemss (map Element.conclude_witness axioms)) |
18550
59b89f625d68
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents:
18546
diff
changeset
|
1852 |
end; |
13394 | 1853 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1854 |
(* adjust hyps of Notes elements *) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1855 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1856 |
fun change_elemss_hyps axioms elemss = |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1857 |
let |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1858 |
val satisfy = Element.morph_ctxt (Element.satisfy_morphism axioms); |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
1859 |
fun change (id as ("", _), es) = (id, map (fn e as Notes _ => satisfy e | e => e) es) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1860 |
| change e = e; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1861 |
in map change elemss end; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1862 |
|
13394 | 1863 |
in |
13375 | 1864 |
|
15104 | 1865 |
(* CB: main predicate definition function *) |
1866 |
||
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1867 |
fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = |
13394 | 1868 |
let |
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1869 |
val ((elemss', more_ts), a_elem, a_intro, thy'') = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1870 |
if null exts then ((elemss, []), [], [], thy) |
13394 | 1871 |
else |
1872 |
let |
|
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1873 |
val aname = if null ints then pname else pname ^ "_" ^ axiomsN; |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1874 |
val ((statement, intro, axioms), thy') = |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1875 |
thy |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1876 |
|> def_pred aname parms defs exts exts'; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1877 |
val elemss' = change_assumes_elemss axioms elemss; |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28053
diff
changeset
|
1878 |
val a_elem = [(("", []), |
28965 | 1879 |
[Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; |
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1880 |
val (_, thy'') = |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1881 |
thy' |
27692 | 1882 |
|> Sign.add_path aname |
1883 |
|> Sign.no_base_names |
|
28965 | 1884 |
|> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])] |
27692 | 1885 |
||> Sign.restore_naming thy'; |
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1886 |
in ((elemss', [statement]), a_elem, [intro], thy'') end; |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1887 |
val (predicate, stmt', elemss'', b_intro, thy'''') = |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1888 |
if null ints then (([], []), more_ts, elemss' @ a_elem, [], thy'') |
13394 | 1889 |
else |
1890 |
let |
|
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1891 |
val ((statement, intro, axioms), thy''') = |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1892 |
thy'' |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1893 |
|> def_pred pname parms defs (ints @ more_ts) (ints' @ more_ts); |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1894 |
val cstatement = Thm.cterm_of thy''' statement; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1895 |
val elemss'' = change_elemss_hyps axioms elemss'; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1896 |
val b_elem = [(("", []), |
28965 | 1897 |
[Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])]; |
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1898 |
val (_, thy'''') = |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1899 |
thy''' |
27692 | 1900 |
|> Sign.add_path pname |
1901 |
|> Sign.no_base_names |
|
1902 |
|> PureThy.note_thmss Thm.internalK |
|
28965 | 1903 |
[((Binding.name introN, []), [([intro], [])]), |
1904 |
((Binding.name axiomsN, []), |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28053
diff
changeset
|
1905 |
[(map (Drule.standard o Element.conclude_witness) axioms, [])])] |
27692 | 1906 |
||> Sign.restore_naming thy'''; |
22351
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1907 |
in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end; |
587845efb4cf
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
haftmann
parents:
22339
diff
changeset
|
1908 |
in (((elemss'', predicate, stmt'), (a_intro, b_intro)), thy'''') end; |
13375 | 1909 |
|
1910 |
end; |
|
13336 | 1911 |
|
1912 |
||
13297 | 1913 |
(* add_locale(_i) *) |
1914 |
||
1915 |
local |
|
1916 |
||
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1917 |
(* turn Defines into Notes elements, accumulate definition terms *) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1918 |
|
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1919 |
fun defines_to_notes is_ext thy (Defines defs) defns = |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1920 |
let |
28965 | 1921 |
val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1922 |
val notes = map (fn (a, (def, _)) => |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1923 |
(a, [([assume (cterm_of thy def)], [])])) defs |
21441 | 1924 |
in |
1925 |
(if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs']) |
|
1926 |
end |
|
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1927 |
| defines_to_notes _ _ e defns = (SOME e, defns); |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1928 |
|
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1929 |
fun change_defines_elemss thy elemss defns = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1930 |
let |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1931 |
fun change (id as (n, _), es) defns = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1932 |
let |
19942
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1933 |
val (es', defns') = fold_map (defines_to_notes (n="") thy) es defns |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1934 |
in ((id, map_filter I es'), defns') end |
dc92e3aebc71
Improved handling of defines imported in duplicate.
ballarin
parents:
19932
diff
changeset
|
1935 |
in fold_map change elemss defns end; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1936 |
|
18343 | 1937 |
fun gen_add_locale prep_ctxt prep_expr |
22573 | 1938 |
predicate_name bname raw_imports raw_body thy = |
27681 | 1939 |
(* predicate_name: "" - locale with predicate named as locale |
1940 |
"name" - locale with predicate named "name" *) |
|
13297 | 1941 |
let |
27681 | 1942 |
val thy_ctxt = ProofContext.init thy; |
28965 | 1943 |
val name = Sign.full_bname thy bname; |
21962 | 1944 |
val _ = is_some (get_locale thy name) andalso |
1945 |
error ("Duplicate definition of locale " ^ quote name); |
|
13297 | 1946 |
|
17228 | 1947 |
val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)), |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1948 |
text as (parms, ((_, exts'), _), defs)) = |
27681 | 1949 |
prep_ctxt raw_imports raw_body thy_ctxt; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1950 |
val elemss = import_elemss @ body_elemss |> |
27681 | 1951 |
map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE); |
13297 | 1952 |
|
29275
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
1953 |
val extraTs = List.foldr OldTerm.add_term_tfrees [] exts' \\ |
9fa69e3858d6
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
1954 |
List.foldr OldTerm.add_typ_tfrees [] (map snd parms); |
17228 | 1955 |
val _ = if null extraTs then () |
17437 | 1956 |
else warning ("Additional type variable(s) in locale specification " ^ quote bname); |
17228 | 1957 |
|
27681 | 1958 |
val predicate_name' = case predicate_name of "" => bname | _ => predicate_name; |
27692 | 1959 |
val (elemss', defns) = change_defines_elemss thy elemss []; |
1960 |
val elemss'' = elemss' @ [(("", []), defns)]; |
|
1961 |
val (((elemss''', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') = |
|
1962 |
define_preds predicate_name' text elemss'' thy; |
|
1963 |
val regs = pred_axioms |
|
1964 |
|> fold_map (fn (id, elems) => fn wts => let |
|
1965 |
val ts = flat (map_filter (fn (Assumes asms) => |
|
1966 |
SOME (maps (map #1 o #2) asms) | _ => NONE) elems); |
|
1967 |
val (wts1, wts2) = chop (length ts) wts; |
|
1968 |
in ((apsnd (map fst) id, wts1), wts2) end) elemss''' |
|
1969 |
|> fst |
|
27681 | 1970 |
|> map_filter (fn (("", _), _) => NONE | e => SOME e); |
18137 | 1971 |
fun axiomify axioms elemss = |
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
15127
diff
changeset
|
1972 |
(axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1973 |
val ts = flat (map_filter (fn (Assumes asms) => |
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
1974 |
SOME (maps (map #1 o #2) asms) | _ => NONE) elems); |
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset
|
1975 |
val (axs1, axs2) = chop (length ts) axs; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
1976 |
in (axs2, ((id, Assumed axs1), elems)) end) |
27692 | 1977 |
|> snd; |
27681 | 1978 |
val ((_, facts), ctxt) = activate_facts true (K I) |
27692 | 1979 |
(axiomify pred_axioms elemss''') (ProofContext.init thy'); |
27681 | 1980 |
val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt; |
26634
149f80f27c84
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26463
diff
changeset
|
1981 |
val export = Thm.close_derivation o Goal.norm_result o |
21602 | 1982 |
singleton (ProofContext.export view_ctxt thy_ctxt); |
13420 | 1983 |
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); |
28375 | 1984 |
val elems' = maps #2 (filter (fn ((s, _), _) => s = "") elemss'''); |
19783 | 1985 |
val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems'; |
27681 | 1986 |
val axs' = map (Element.assume_witness thy') stmt'; |
1987 |
val loc_ctxt = thy' |
|
27692 | 1988 |
|> Sign.add_path bname |
1989 |
|> Sign.no_base_names |
|
1990 |
|> PureThy.note_thmss Thm.assumptionK facts' |> snd |
|
1991 |
|> Sign.restore_naming thy' |
|
28991 | 1992 |
|> register_locale bname {axiom = axs', |
19783 | 1993 |
elems = map (fn e => (e, stamp ())) elems'', |
27692 | 1994 |
params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))), |
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
1995 |
decls = ([], []), |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
1996 |
regs = regs, |
25619 | 1997 |
intros = intros, |
27681 | 1998 |
dests = map Element.conclude_witness pred_axioms} |
21393
c648e24fd7ee
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
wenzelm
parents:
21370
diff
changeset
|
1999 |
|> init name; |
c648e24fd7ee
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
wenzelm
parents:
21370
diff
changeset
|
2000 |
in (name, loc_ctxt) end; |
13297 | 2001 |
|
2002 |
in |
|
2003 |
||
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2004 |
val add_locale = gen_add_locale cert_context (K I); |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2005 |
val add_locale_cmd = gen_add_locale read_context intern_expr ""; |
13297 | 2006 |
|
2007 |
end; |
|
2008 |
||
26463 | 2009 |
val _ = Context.>> (Context.map_theory |
28965 | 2010 |
(add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #> |
20965 | 2011 |
snd #> ProofContext.theory_of #> |
28965 | 2012 |
add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #> |
26463 | 2013 |
snd #> ProofContext.theory_of)); |
15801 | 2014 |
|
13297 | 2015 |
|
12730 | 2016 |
|
17355 | 2017 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2018 |
(** Normalisation of locale statements --- |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2019 |
discharges goals implied by interpretations **) |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2020 |
|
28893 | 2021 |
local |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2022 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2023 |
fun locale_assm_intros thy = |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2024 |
Symtab.fold (fn (_, {intros = (a, _), ...}) => fn intros => (a @ intros)) |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
2025 |
(#2 (LocalesData.get thy)) []; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2026 |
fun locale_base_intros thy = |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2027 |
Symtab.fold (fn (_, {intros = (_, b), ...}) => fn intros => (b @ intros)) |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
2028 |
(#2 (LocalesData.get thy)) []; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2029 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2030 |
fun all_witnesses ctxt = |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2031 |
let |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2032 |
val thy = ProofContext.theory_of ctxt; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2033 |
fun get registrations = Symtab.fold (fn (_, regs) => fn thms => |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2034 |
(Registrations.dest thy regs |> map (fn (_, (_, (exp, _), wits, _)) => |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2035 |
map (Element.conclude_witness #> Morphism.thm exp) wits) |> flat) @ thms) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2036 |
registrations []; |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
2037 |
in get (RegistrationsData.get (Context.Proof ctxt)) end; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2038 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2039 |
in |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2040 |
|
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19942
diff
changeset
|
2041 |
fun intro_locales_tac eager ctxt facts st = |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2042 |
let |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2043 |
val wits = all_witnesses ctxt; |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2044 |
val thy = ProofContext.theory_of ctxt; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2045 |
val intros = locale_base_intros thy @ (if eager then locale_assm_intros thy else []); |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2046 |
in |
25270 | 2047 |
Method.intros_tac (wits @ intros) facts st |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2048 |
end; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2049 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2050 |
end; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2051 |
|
19780 | 2052 |
|
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
2053 |
(** Interpretation commands **) |
15596 | 2054 |
|
2055 |
local |
|
2056 |
||
2057 |
(* extract proof obligations (assms and defs) from elements *) |
|
2058 |
||
19780 | 2059 |
fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems) |
17138 | 2060 |
| extract_asms_elems ((id, Derived _), _) = (id, []); |
15596 | 2061 |
|
2062 |
||
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
2063 |
(* activate instantiated facts in theory or context *) |
15596 | 2064 |
|
28739 | 2065 |
fun gen_activate_facts_elemss mk_ctxt note attrib put_reg add_wit add_eqn |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2066 |
phi_name all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt = |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2067 |
let |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2068 |
val ctxt = mk_ctxt thy_ctxt; |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2069 |
fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2070 |
fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2071 |
|
28005 | 2072 |
val (all_propss, eq_props) = chop (length all_elemss) propss; |
2073 |
val (all_thmss, eq_thms) = chop (length all_elemss) thmss; |
|
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2074 |
|
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2075 |
(* Filter out fragments already registered. *) |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2076 |
|
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2077 |
val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) => |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2078 |
test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss)))); |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2079 |
val (new_pss, ys) = split_list xs; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2080 |
val (new_propss, new_thmss) = split_list ys; |
17033 | 2081 |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2082 |
val thy_ctxt' = thy_ctxt |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2083 |
(* add registrations *) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2084 |
|> fold2 (fn ((id as (loc, _), _), _) => fn ps => put_reg id (phi_name, param_prefix loc ps) (exp, imp)) |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2085 |
new_elemss new_pss |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2086 |
(* add witnesses of Assumed elements (only those generate proof obligations) *) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2087 |
|> fold2 (fn (id, _) => fold (add_wit id)) new_propss new_thmss |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2088 |
(* add equations *) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2089 |
|> fold2 (fn (id, _) => fold (add_eqn id)) eq_props |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2090 |
((map o map) (Drule.abs_def o LocalDefs.meta_rewrite_rule ctxt o |
23918 | 2091 |
Element.conclude_witness) eq_thms); |
15596 | 2092 |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2093 |
val prems = flat (map_filter |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2094 |
(fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id) |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2095 |
| ((_, Derived _), _) => NONE) all_elemss); |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2096 |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2097 |
val thy_ctxt'' = thy_ctxt' |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2098 |
(* add witnesses of Derived elements *) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2099 |
|> fold (fn (id, thms) => fold |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2100 |
(add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms) |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2101 |
(map_filter (fn ((_, Assumed _), _) => NONE |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2102 |
| ((id, Derived thms), _) => SOME (id, thms)) new_elemss) |
19780 | 2103 |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2104 |
fun activate_elem phi_name param_prfx insts prems eqns exp (Notes (kind, facts)) thy_ctxt = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2105 |
let |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2106 |
val ctxt = mk_ctxt thy_ctxt; |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2107 |
val thy = ProofContext.theory_of ctxt; |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2108 |
val facts' = facts |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2109 |
|> activate_note thy phi_name param_prfx |
28739 | 2110 |
(attrib thy_ctxt) insts prems eqns exp; |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2111 |
in |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2112 |
thy_ctxt |
28940 | 2113 |
|> note kind facts' |
2114 |
|> snd |
|
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2115 |
end |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2116 |
| activate_elem _ _ _ _ _ _ _ thy_ctxt = thy_ctxt; |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2117 |
|
28739 | 2118 |
fun activate_elems (((loc, ext_ts), _), _) ps thy_ctxt = |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2119 |
let |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2120 |
val ctxt = mk_ctxt thy_ctxt; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2121 |
val thy = ProofContext.theory_of ctxt; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2122 |
val {params, elems, ...} = the_locale thy loc; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2123 |
val parms = map fst params; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2124 |
val param_prfx = param_prefix loc ps; |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2125 |
val ids = flatten (ProofContext.init thy, intern_expr thy) |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2126 |
(([], Symtab.empty), Expr (Locale loc)) |> fst |> fst; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2127 |
val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts; |
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2128 |
in |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2129 |
thy_ctxt |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2130 |
|> fold (activate_elem phi_name param_prfx insts prems eqns exp o fst) elems |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2131 |
end; |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2132 |
|
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2133 |
in |
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2134 |
thy_ctxt'' |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2135 |
(* add equations as lemmas to context *) |
28940 | 2136 |
|> (fold2 o fold2) (fn attn => fn thm => snd o yield_singleton (note Thm.lemmaK) |
28739 | 2137 |
((apsnd o map) (attrib thy_ctxt'') attn, [([Element.conclude_witness thm], [])])) |
2138 |
(unflat eq_thms eq_attns) eq_thms |
|
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2139 |
(* add interpreted facts *) |
28739 | 2140 |
|> fold2 activate_elems new_elemss new_pss |
21499
fbd6422a847a
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm
parents:
21483
diff
changeset
|
2141 |
end; |
15596 | 2142 |
|
17355 | 2143 |
fun global_activate_facts_elemss x = gen_activate_facts_elemss |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2144 |
ProofContext.init |
28865 | 2145 |
global_note_qualified |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2146 |
Attrib.attribute_i |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2147 |
put_global_registration |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2148 |
add_global_witness |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2149 |
add_global_equation |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2150 |
x; |
17355 | 2151 |
|
2152 |
fun local_activate_facts_elemss x = gen_activate_facts_elemss |
|
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2153 |
I |
28865 | 2154 |
local_note_qualified |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2155 |
(Attrib.attribute_i o ProofContext.theory_of) |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2156 |
put_local_registration |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2157 |
add_local_witness |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2158 |
add_local_equation |
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2159 |
x; |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2160 |
|
25067
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2161 |
fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) = |
15596 | 2162 |
let |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2163 |
(* parameters *) |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2164 |
val (parm_names, parm_types) = parms |> split_list |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2165 |
||> map (TypeInfer.paramify_vars o Logic.varifyT); |
25038 | 2166 |
val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar); |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2167 |
val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst; |
22772
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2168 |
|
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2169 |
(* parameter instantiations *) |
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2170 |
val d = length parms - length insts; |
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2171 |
val insts = |
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2172 |
if d < 0 then error "More arguments than parameters in instantiation." |
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2173 |
else insts @ replicate d NONE; |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2174 |
val (given_ps, given_insts) = |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2175 |
((parm_names ~~ parm_types) ~~ insts) |> map_filter |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2176 |
(fn (_, NONE) => NONE |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2177 |
| ((n, T), SOME inst) => SOME ((n, T), inst)) |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2178 |
|> split_list; |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2179 |
val (given_parm_names, given_parm_types) = given_ps |> split_list; |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2180 |
|
25067
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2181 |
(* parse insts / eqns *) |
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2182 |
val given_insts' = map (parse_term ctxt) given_insts; |
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2183 |
val eqns' = map (parse_prop ctxt) eqns; |
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2184 |
|
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2185 |
(* type inference and contexts *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2186 |
val arg = type_parms @ map2 TypeInfer.constrain given_parm_types given_insts' @ eqns'; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2187 |
val res = Syntax.check_terms ctxt arg; |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2188 |
val ctxt' = ctxt |> fold Variable.auto_fixes res; |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2189 |
|
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2190 |
(* instantiation *) |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2191 |
val (type_parms'', res') = chop (length type_parms) res; |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2192 |
val (given_insts'', eqns'') = chop (length given_insts) res'; |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2193 |
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); |
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2194 |
val inst = Symtab.make (given_parm_names ~~ given_insts''); |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2195 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2196 |
(* export from eigencontext *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2197 |
val export = Variable.export_morphism ctxt' ctxt; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2198 |
|
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2199 |
(* import, its inverse *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2200 |
val domT = fold Term.add_tfrees res [] |> map TFree; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2201 |
val importT = domT |> map (fn x => (Morphism.typ export x, x)) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2202 |
|> map_filter (fn (TFree _, _) => NONE (* fixed point of export *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2203 |
| (TVar y, x) => SOME (fst y, x) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2204 |
| _ => error "internal: illegal export in interpretation") |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2205 |
|> Vartab.make; |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2206 |
val dom = fold Term.add_frees res [] |> map Free; |
25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset
|
2207 |
val imprt = dom |> map (fn x => (Morphism.term export x, x)) |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2208 |
|> map_filter (fn (Free _, _) => NONE (* fixed point of export *) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2209 |
| (Var y, x) => SOME (fst y, x) |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2210 |
| _ => error "internal: illegal export in interpretation") |
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2211 |
|> Vartab.make; |
25357
6ea18fd11058
avoid "import" as identifier, which is a keyword in Alice;
wenzelm
parents:
25286
diff
changeset
|
2212 |
in (((instT, inst), eqns''), (export, ((importT, domT), (imprt, dom)))) end; |
24941
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2213 |
|
9ab032df81c8
Prepare proper interface of interpretation_i, interpret_i.
ballarin
parents:
24920
diff
changeset
|
2214 |
val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop; |
25067
0f19e65ac0b6
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
wenzelm
parents:
25038
diff
changeset
|
2215 |
val check_instantiations = prep_instantiations (K I) (K I); |
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
2216 |
|
22772
e0788ff2e811
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
wenzelm
parents:
22756
diff
changeset
|
2217 |
fun gen_prep_registration mk_ctxt test_reg activate |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2218 |
prep_attr prep_expr prep_insts |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2219 |
thy_ctxt phi_name raw_expr raw_insts = |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2220 |
let |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2221 |
val ctxt = mk_ctxt thy_ctxt; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2222 |
val thy = ProofContext.theory_of ctxt; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2223 |
val ctxt' = ProofContext.init thy; |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2224 |
fun prep_attn attn = (apsnd o map) |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2225 |
(Attrib.crude_closure ctxt o Args.assignable o prep_attr thy) attn; |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2226 |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2227 |
val expr = prep_expr thy raw_expr; |
15596 | 2228 |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2229 |
val pts = params_of_expr ctxt' [] expr ([], Symtab.empty, Symtab.empty); |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2230 |
val params_ids = make_params_ids (#1 pts); |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2231 |
val raw_params_elemss = make_raw_params_elemss pts; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2232 |
val ((ids, _), raw_elemss) = flatten (ctxt', I) (([], Symtab.empty), Expr expr); |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2233 |
val ((parms, all_elemss, _), (_, (_, defs, _))) = |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2234 |
read_elemss false ctxt' [] (raw_params_elemss @ raw_elemss) []; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2235 |
|
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2236 |
(** compute instantiation **) |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2237 |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2238 |
(* consistency check: equations need to be stored in a particular locale, |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2239 |
therefore if equations are present locale expression must be a name *) |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2240 |
|
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2241 |
val _ = case (expr, snd raw_insts) of |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2242 |
(Locale _, _) => () | (_, []) => () |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2243 |
| (_, _) => error "Interpretations with `where' only permitted if locale expression is a name."; |
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2244 |
|
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2245 |
(* read or certify instantiation *) |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2246 |
val (raw_insts', raw_eqns) = raw_insts; |
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2247 |
val (raw_eq_attns, raw_eqns') = split_list raw_eqns; |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2248 |
val (((instT, inst1), eqns), morphs) = prep_insts ctxt parms (raw_insts', raw_eqns'); |
25095
ea8307dac208
Interpretation equations may have name and/or attribute;
ballarin
parents:
25073
diff
changeset
|
2249 |
val eq_attns = map prep_attn raw_eq_attns; |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2250 |
|
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2251 |
(* defined params without given instantiation *) |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2252 |
val not_given = filter_out (Symtab.defined inst1 o fst) parms; |
18137 | 2253 |
fun add_def (p, pT) inst = |
15596 | 2254 |
let |
2255 |
val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of |
|
2256 |
NONE => error ("Instance missing for parameter " ^ quote p) |
|
2257 |
| SOME (Free (_, T), t) => (t, T); |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2258 |
val d = Element.inst_term (instT, inst) t; |
18137 | 2259 |
in Symtab.update_new (p, d) inst end; |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2260 |
val inst2 = fold add_def not_given inst1; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2261 |
val inst_morphism = Element.inst_morphism thy (instT, inst2); |
18137 | 2262 |
(* Note: insts contain no vars. *) |
15596 | 2263 |
|
2264 |
(** compute proof obligations **) |
|
2265 |
||
15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15596
diff
changeset
|
2266 |
(* restore "small" ids *) |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2267 |
val ids' = map (fn ((n, ps), (_, mode)) => |
19783 | 2268 |
((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2269 |
ids; |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2270 |
val (_, all_elemss') = chop (length raw_params_elemss) all_elemss |
15596 | 2271 |
(* instantiate ids and elements *) |
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19914
diff
changeset
|
2272 |
val inst_elemss = (ids' ~~ all_elemss') |> map (fn (((n, ps), _), ((_, mode), elems)) => |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2273 |
((n, map (Morphism.term (inst_morphism $> fst morphs)) ps), |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
2274 |
map (fn Int e => Element.morph_ctxt inst_morphism e) elems) |
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
2275 |
|> apfst (fn id => (id, map_mode (map (Element.morph_witness inst_morphism)) mode))); |
28053 | 2276 |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2277 |
(* equations *) |
23918 | 2278 |
val eqn_elems = if null eqns then [] |
2279 |
else [(Library.last_elem inst_elemss |> fst |> fst, eqns)]; |
|
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22573
diff
changeset
|
2280 |
|
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2281 |
val propss = map extract_asms_elems inst_elemss @ eqn_elems; |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27716
diff
changeset
|
2282 |
|
28259 | 2283 |
in |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2284 |
(propss, activate phi_name inst_elemss (map (snd o fst) ids) propss eq_attns morphs, morphs) |
28259 | 2285 |
end; |
15596 | 2286 |
|
22756 | 2287 |
fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2288 |
test_global_registration |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2289 |
global_activate_facts_elemss mk_ctxt; |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
2290 |
|
22756 | 2291 |
fun gen_prep_local_registration mk_ctxt = gen_prep_registration I |
24787
df56433cc059
Theory/context data restructured; simplified interface for printing of interpretations.
ballarin
parents:
24751
diff
changeset
|
2292 |
test_local_registration |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2293 |
local_activate_facts_elemss mk_ctxt; |
15624
484178635bd8
Further work on interpretation commands. New command `interpret' for
ballarin
parents:
15623
diff
changeset
|
2294 |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2295 |
val prep_global_registration = gen_prep_global_registration |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2296 |
(K I) (K I) check_instantiations; |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2297 |
val prep_global_registration_cmd = gen_prep_global_registration |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2298 |
Attrib.intern_src intern_expr read_instantiations; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2299 |
|
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2300 |
val prep_local_registration = gen_prep_local_registration |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2301 |
(K I) (K I) check_instantiations; |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2302 |
val prep_local_registration_cmd = gen_prep_local_registration |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2303 |
Attrib.intern_src intern_expr read_instantiations; |
15596 | 2304 |
|
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2305 |
fun prep_registration_in_locale target expr thy = |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2306 |
(* target already in internal form *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2307 |
let |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2308 |
val ctxt = ProofContext.init thy; |
17138 | 2309 |
val ((raw_target_ids, target_syn), _) = flatten (ctxt, I) |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2310 |
(([], Symtab.empty), Expr (Locale target)); |
19278 | 2311 |
val fixed = the_locale thy target |> #params |> map #1; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2312 |
val ((all_ids, syn), raw_elemss) = flatten (ctxt, intern_expr thy) |
17138 | 2313 |
((raw_target_ids, target_syn), Expr expr); |
19018
88b4979193d8
added abbreviations: activated by init, no expressions yet;
wenzelm
parents:
18964
diff
changeset
|
2314 |
val (target_ids, ids) = chop (length raw_target_ids) all_ids; |
17138 | 2315 |
val ((parms, elemss, _), _) = read_elemss false ctxt fixed raw_elemss []; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2316 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2317 |
(** compute proof obligations **) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2318 |
|
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2319 |
(* restore "small" ids, with mode *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2320 |
val ids' = map (apsnd snd) ids; |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2321 |
(* remove Int markers *) |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2322 |
val elemss' = map (fn (_, es) => |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2323 |
map (fn Int e => e) es) elemss |
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2324 |
(* extract assumptions and defs *) |
17138 | 2325 |
val ids_elemss = ids' ~~ elemss'; |
19780 | 2326 |
val propss = map extract_asms_elems ids_elemss; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2327 |
|
17138 | 2328 |
(** activation function: |
2329 |
- add registrations to the target locale |
|
2330 |
- add induced registrations for all global registrations of |
|
2331 |
the target, unless already present |
|
2332 |
- add facts of induced registrations to theory **) |
|
2333 |
||
28739 | 2334 |
fun activate thmss thy = |
2335 |
let |
|
19780 | 2336 |
val satisfy = Element.satisfy_thm (flat thmss); |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2337 |
val ids_elemss_thmss = ids_elemss ~~ thmss; |
17138 | 2338 |
val regs = get_global_registrations thy target; |
2339 |
||
2340 |
fun activate_id (((id, Assumed _), _), thms) thy = |
|
17033 | 2341 |
thy |> put_registration_in_locale target id |
17138 | 2342 |
|> fold (add_witness_in_locale target id) thms |
2343 |
| activate_id _ thy = thy; |
|
2344 |
||
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2345 |
fun activate_reg (ext_ts, ((phi_name, param_prfx), (exp, imp), _, _)) thy = |
21483
e4be91feca50
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm
parents:
21441
diff
changeset
|
2346 |
let |
28236
c447b60d67f5
Clearer separation of interpretation frontend and backend.
ballarin
parents:
28110
diff
changeset
|
2347 |
val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts; |
28739 | 2348 |
val inst_parms = map (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)); |
19780 | 2349 |
val disch = Element.satisfy_thm wits; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19423
diff
changeset
|
2350 |
val new_elemss = filter (fn (((name, ps), _), _) => |
17138 | 2351 |
not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); |
2352 |
fun activate_assumed_id (((_, Derived _), _), _) thy = thy |
|
2353 |
| activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let |
|
2354 |
val ps' = inst_parms ps; |
|
2355 |
in |
|
2356 |
if test_global_registration thy (name, ps') |
|
2357 |
then thy |
|
2358 |
else thy |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2359 |
|> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) |
19780 | 2360 |
|> fold (fn witn => fn thy => add_global_witness (name, ps') |
25286
35e954ff67f8
Use of export rather than standard in interpretation.
ballarin
parents:
25270
diff
changeset
|
2361 |
(Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms |
17138 | 2362 |
end; |
2363 |
||
2364 |
fun activate_derived_id ((_, Assumed _), _) thy = thy |
|
2365 |
| activate_derived_id (((name, ps), Derived ths), _) thy = let |
|
2366 |
val ps' = inst_parms ps; |
|
2367 |
in |
|
2368 |
if test_global_registration thy (name, ps') |
|
2369 |
then thy |
|
2370 |
else thy |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2371 |
|> put_global_registration (name, ps') (phi_name, param_prefix name ps) (exp, imp) |
19780 | 2372 |
|> fold (fn witn => fn thy => add_global_witness (name, ps') |
2373 |
(witn |> Element.map_witness (fn (t, th) => (* FIXME *) |
|
18137 | 2374 |
(Element.inst_term insts t, |
19780 | 2375 |
disch (Element.inst_thm thy insts (satisfy th))))) thy) ths |
17138 | 2376 |
end; |
2377 |
||
26645
e114be97befe
Changed naming scheme for theorems generated by interpretations.
ballarin
parents:
26634
diff
changeset
|
2378 |
fun activate_elem (loc, ps) (Notes (kind, facts)) thy = |
17138 | 2379 |
let |
21523 | 2380 |
val att_morphism = |
28965 | 2381 |
Morphism.binding_morphism (name_morph phi_name param_prfx) $> |
21523 | 2382 |
Morphism.thm_morphism satisfy $> |
2383 |
Element.inst_morphism thy insts $> |
|
2384 |
Morphism.thm_morphism disch; |
|
17138 | 2385 |
val facts' = facts |
21523 | 2386 |
|> Attrib.map_facts (Attrib.attribute_i thy o Args.morph_values att_morphism) |
28734
19277c7a160c
restruced naming code in anticipation of introduction of name morphisms
haftmann
parents:
28726
diff
changeset
|
2387 |
|> (map o apsnd o map o apfst o map) (disch o Element.inst_thm thy insts o satisfy) |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2388 |
|> (map o apfst o apfst) (name_morph phi_name param_prfx); |
17138 | 2389 |
in |
18377 | 2390 |
thy |
28940 | 2391 |
|> global_note_qualified kind facts' |
2392 |
|> snd |
|
17138 | 2393 |
end |
26645
e114be97befe
Changed naming scheme for theorems generated by interpretations.
ballarin
parents:
26634
diff
changeset
|
2394 |
| activate_elem _ _ thy = thy; |
e114be97befe
Changed naming scheme for theorems generated by interpretations.
ballarin
parents:
26634
diff
changeset
|
2395 |
|
e114be97befe
Changed naming scheme for theorems generated by interpretations.
ballarin
parents:
26634
diff
changeset
|
2396 |
fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy; |
17138 | 2397 |
|
2398 |
in thy |> fold activate_assumed_id ids_elemss_thmss |
|
2399 |
|> fold activate_derived_id ids_elemss |
|
2400 |
|> fold activate_elems new_elemss end; |
|
17033 | 2401 |
in |
17138 | 2402 |
thy |> fold activate_id ids_elemss_thmss |
2403 |
|> fold activate_reg regs |
|
17033 | 2404 |
end; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2405 |
|
17033 | 2406 |
in (propss, activate) end; |
17000
552df70f52c2
First version of interpretation in locales. Not yet fully functional.
ballarin
parents:
16947
diff
changeset
|
2407 |
|
21005 | 2408 |
fun prep_propp propss = propss |> map (fn (_, props) => |
21361 | 2409 |
map (rpair [] o Element.mark_witness) props); |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2410 |
|
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2411 |
fun prep_result propps thmss = |
19780 | 2412 |
ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss); |
17437 | 2413 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28084
diff
changeset
|
2414 |
fun gen_interpretation prep_registration after_qed prfx raw_expr raw_insts thy = |
17355 | 2415 |
let |
28259 | 2416 |
val (propss, activate, morphs) = prep_registration thy prfx raw_expr raw_insts; |
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2417 |
fun after_qed' results = |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2418 |
ProofContext.theory (activate (prep_result propss results)) |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2419 |
#> after_qed; |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2420 |
in |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2421 |
thy |
23418 | 2422 |
|> ProofContext.init |
21441 | 2423 |
|> Proof.theorem_i NONE after_qed' (prep_propp propss) |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2424 |
|> Element.refine_witness |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2425 |
|> Seq.hd |
28259 | 2426 |
|> pair morphs |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2427 |
end; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2428 |
|
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2429 |
fun gen_interpret prep_registration after_qed name_morph expr insts int state = |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2430 |
let |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2431 |
val _ = Proof.assert_forward_or_chain state; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2432 |
val ctxt = Proof.context_of state; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2433 |
val (propss, activate, morphs) = prep_registration ctxt name_morph expr insts; |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2434 |
fun after_qed' results = |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2435 |
Proof.map_context (K (ctxt |> activate (prep_result propss results))) |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2436 |
#> Proof.put_facts NONE |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2437 |
#> after_qed; |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2438 |
in |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2439 |
state |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2440 |
|> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i |
28965 | 2441 |
"interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss)) |
19810 | 2442 |
|> Element.refine_witness |> Seq.hd |
28259 | 2443 |
|> pair morphs |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2444 |
end; |
17355 | 2445 |
|
28862 | 2446 |
fun standard_name_morph interp_prfx b = |
28965 | 2447 |
if Binding.is_empty b then b |
28941 | 2448 |
else Binding.map_prefix (fn ((lprfx, _) :: pprfx) => |
2449 |
fold (Binding.add_prefix false o fst) pprfx |
|
2450 |
#> interp_prfx <> "" ? Binding.add_prefix true interp_prfx |
|
2451 |
#> Binding.add_prefix false lprfx |
|
28862 | 2452 |
) b; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2453 |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2454 |
in |
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2455 |
|
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2456 |
val interpretation = gen_interpretation prep_global_registration; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2457 |
fun interpretation_cmd interp_prfx = snd ooo gen_interpretation prep_global_registration_cmd |
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2458 |
I (standard_name_morph interp_prfx); |
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2459 |
|
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2460 |
fun interpretation_in_locale after_qed (raw_target, expr) thy = |
17355 | 2461 |
let |
2462 |
val target = intern thy raw_target; |
|
2463 |
val (propss, activate) = prep_registration_in_locale target expr thy; |
|
21361 | 2464 |
val raw_propp = prep_propp propss; |
21005 | 2465 |
|
2466 |
val (_, _, goal_ctxt, propp) = thy |
|
21665
ba07e24dc941
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
wenzelm
parents:
21602
diff
changeset
|
2467 |
|> ProofContext.init |
21361 | 2468 |
|> cert_context_statement (SOME target) [] raw_propp; |
21005 | 2469 |
|
2470 |
fun after_qed' results = |
|
20366
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2471 |
ProofContext.theory (activate (prep_result propss results)) |
867696dc64fc
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20317
diff
changeset
|
2472 |
#> after_qed; |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2473 |
in |
21005 | 2474 |
goal_ctxt |
21441 | 2475 |
|> Proof.theorem_i NONE after_qed' propp |
19810 | 2476 |
|> Element.refine_witness |> Seq.hd |
18123
1bb572e8cee9
avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents:
18038
diff
changeset
|
2477 |
end; |
17449
429ca1e21289
interpretation: use goal commands without target -- no storing of results;
wenzelm
parents:
17438
diff
changeset
|
2478 |
|
22300
596f49b70c70
internal interfaces for interpretation and interpret
haftmann
parents:
22241
diff
changeset
|
2479 |
val interpret = gen_interpret prep_local_registration; |
28822
7ca11ecbc4fb
explicit name morphism function for locale interpretation
haftmann
parents:
28794
diff
changeset
|
2480 |
fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd |
29383 | 2481 |
I (standard_name_morph interp_prfx); |
15596 | 2482 |
|
11896 | 2483 |
end; |
17355 | 2484 |
|
2485 |
end; |