ballarin@28697
|
1 |
(* Title: Pure/Isar/expression.ML
|
ballarin@28697
|
2 |
Author: Clemens Ballarin, TU Muenchen
|
ballarin@28697
|
3 |
|
ballarin@32784
|
4 |
Locale expressions and user interface layer of locales.
|
ballarin@28697
|
5 |
*)
|
ballarin@28697
|
6 |
|
ballarin@28697
|
7 |
signature EXPRESSION =
|
ballarin@28697
|
8 |
sig
|
haftmann@29501
|
9 |
(* Locale expressions *)
|
haftmann@29501
|
10 |
datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
|
wneuper@59451
|
11 |
type 'term rewrites = (Attrib.binding * 'term) list
|
wneuper@59451
|
12 |
type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list
|
wenzelm@47804
|
13 |
type expression_i = (string, term) expr * (binding * typ option * mixfix) list
|
wenzelm@47804
|
14 |
type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
|
ballarin@28697
|
15 |
|
ballarin@28898
|
16 |
(* Processing of context statements *)
|
wneuper@59324
|
17 |
val cert_statement: Element.context_i list -> Element.statement_i ->
|
wneuper@59324
|
18 |
Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
|
wneuper@59324
|
19 |
val read_statement: Element.context list -> Element.statement ->
|
wneuper@59324
|
20 |
Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
|
ballarin@28879
|
21 |
|
ballarin@28795
|
22 |
(* Declaring locales *)
|
wenzelm@56981
|
23 |
val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
|
wenzelm@56981
|
24 |
Element.context_i list ->
|
wenzelm@30762
|
25 |
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
|
wenzelm@48185
|
26 |
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
|
wenzelm@56981
|
27 |
val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) ->
|
wenzelm@56981
|
28 |
Element.context list ->
|
wenzelm@30762
|
29 |
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
|
wenzelm@48185
|
30 |
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
|
haftmann@29501
|
31 |
(*FIXME*)
|
haftmann@29702
|
32 |
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
|
wenzelm@30762
|
33 |
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
|
wenzelm@48185
|
34 |
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
|
haftmann@58523
|
35 |
val add_locale: binding -> binding ->
|
wenzelm@41833
|
36 |
expression_i -> Element.context_i list -> theory -> string * local_theory
|
haftmann@58523
|
37 |
val add_locale_cmd: binding -> binding ->
|
wenzelm@41833
|
38 |
expression -> Element.context list -> theory -> string * local_theory
|
ballarin@28885
|
39 |
|
wneuper@59324
|
40 |
(* Processing of locale expressions *)
|
haftmann@29439
|
41 |
val cert_goal_expression: expression_i -> Proof.context ->
|
wneuper@59451
|
42 |
(term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
|
haftmann@29496
|
43 |
val read_goal_expression: expression -> Proof.context ->
|
wneuper@59451
|
44 |
(term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
|
ballarin@28697
|
45 |
end;
|
ballarin@28697
|
46 |
|
walther@60138
|
47 |
structure Expression (**): EXPRESSION(**) =
|
ballarin@28697
|
48 |
struct
|
ballarin@28697
|
49 |
|
ballarin@28795
|
50 |
datatype ctxt = datatype Element.ctxt;
|
ballarin@28795
|
51 |
|
ballarin@28795
|
52 |
|
ballarin@28795
|
53 |
(*** Expressions ***)
|
ballarin@28697
|
54 |
|
ballarin@28872
|
55 |
datatype 'term map =
|
ballarin@28872
|
56 |
Positional of 'term option list |
|
ballarin@28872
|
57 |
Named of (string * 'term) list;
|
ballarin@28697
|
58 |
|
wneuper@59451
|
59 |
type 'term rewrites = (Attrib.binding * 'term) list;
|
wneuper@59451
|
60 |
|
wneuper@59451
|
61 |
type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list;
|
ballarin@28697
|
62 |
|
wenzelm@47804
|
63 |
type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
|
wenzelm@47804
|
64 |
type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
|
ballarin@28795
|
65 |
|
ballarin@28697
|
66 |
|
ballarin@28859
|
67 |
(** Internalise locale names in expr **)
|
ballarin@28697
|
68 |
|
wenzelm@47804
|
69 |
fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
|
ballarin@28697
|
70 |
|
ballarin@28795
|
71 |
|
wenzelm@30783
|
72 |
(** Parameters of expression **)
|
ballarin@28697
|
73 |
|
wenzelm@30783
|
74 |
(*Sanity check of instantiations and extraction of implicit parameters.
|
wenzelm@30783
|
75 |
The latter only occurs iff strict = false.
|
wenzelm@30783
|
76 |
Positional instantiations are extended to match full length of parameter list
|
wenzelm@30783
|
77 |
of instantiated locale.*)
|
ballarin@28895
|
78 |
|
ballarin@28895
|
79 |
fun parameters_of thy strict (expr, fixed) =
|
ballarin@28697
|
80 |
let
|
wenzelm@54178
|
81 |
val ctxt = Proof_Context.init_global thy;
|
wenzelm@54178
|
82 |
|
ballarin@28697
|
83 |
fun reject_dups message xs =
|
wenzelm@30762
|
84 |
(case duplicates (op =) xs of
|
wenzelm@30762
|
85 |
[] => ()
|
wenzelm@30762
|
86 |
| dups => error (message ^ commas dups));
|
ballarin@28697
|
87 |
|
wneuper@59324
|
88 |
fun parm_eq ((p1, mx1), (p2, mx2)) =
|
wneuper@59324
|
89 |
p1 = p2 andalso
|
wneuper@59324
|
90 |
(Mixfix.equal (mx1, mx2) orelse
|
wneuper@59324
|
91 |
error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^
|
wneuper@59324
|
92 |
Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
|
wenzelm@30350
|
93 |
|
wenzelm@30762
|
94 |
fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
|
wneuper@59451
|
95 |
fun params_inst (loc, (prfx, (Positional insts, eqns))) =
|
ballarin@28697
|
96 |
let
|
wenzelm@30762
|
97 |
val ps = params_loc loc;
|
haftmann@29358
|
98 |
val d = length ps - length insts;
|
haftmann@29358
|
99 |
val insts' =
|
wenzelm@54178
|
100 |
if d < 0 then
|
wenzelm@54178
|
101 |
error ("More arguments than parameters in instantiation of locale " ^
|
wenzelm@54178
|
102 |
quote (Locale.markup_name ctxt loc))
|
haftmann@29358
|
103 |
else insts @ replicate d NONE;
|
ballarin@28697
|
104 |
val ps' = (ps ~~ insts') |>
|
ballarin@28697
|
105 |
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
|
wneuper@59451
|
106 |
in (ps', (loc, (prfx, (Positional insts', eqns)))) end
|
wneuper@59451
|
107 |
| params_inst (loc, (prfx, (Named insts, eqns))) =
|
ballarin@28697
|
108 |
let
|
wenzelm@54178
|
109 |
val _ =
|
wenzelm@54178
|
110 |
reject_dups "Duplicate instantiation of the following parameter(s): "
|
wenzelm@54178
|
111 |
(map fst insts);
|
wenzelm@30783
|
112 |
val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
|
wenzelm@30762
|
113 |
if AList.defined (op =) ps p then AList.delete (op =) p ps
|
wenzelm@30783
|
114 |
else error (quote p ^ " not a parameter of instantiated expression"));
|
wneuper@59451
|
115 |
in (ps', (loc, (prfx, (Named insts, eqns)))) end;
|
ballarin@28885
|
116 |
fun params_expr is =
|
wenzelm@30783
|
117 |
let
|
wenzelm@30783
|
118 |
val (is', ps') = fold_map (fn i => fn ps =>
|
ballarin@28697
|
119 |
let
|
wenzelm@30783
|
120 |
val (ps', i') = params_inst i;
|
wenzelm@30783
|
121 |
val ps'' = distinct parm_eq (ps @ ps');
|
wenzelm@30783
|
122 |
in (i', ps'') end) is []
|
wenzelm@30783
|
123 |
in (ps', is') end;
|
ballarin@28697
|
124 |
|
ballarin@28895
|
125 |
val (implicit, expr') = params_expr expr;
|
ballarin@28697
|
126 |
|
wenzelm@30762
|
127 |
val implicit' = map #1 implicit;
|
wenzelm@43366
|
128 |
val fixed' = map (Variable.check_name o #1) fixed;
|
ballarin@28697
|
129 |
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
|
wenzelm@30350
|
130 |
val implicit'' =
|
wenzelm@30350
|
131 |
if strict then []
|
wenzelm@30350
|
132 |
else
|
wenzelm@56981
|
133 |
let
|
wenzelm@56981
|
134 |
val _ =
|
wenzelm@56981
|
135 |
reject_dups
|
wenzelm@56981
|
136 |
"Parameter(s) declared simultaneously in expression and for clause: "
|
wenzelm@56981
|
137 |
(implicit' @ fixed');
|
wenzelm@30762
|
138 |
in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
|
ballarin@28697
|
139 |
|
ballarin@28895
|
140 |
in (expr', implicit'' @ fixed) end;
|
ballarin@28697
|
141 |
|
ballarin@28795
|
142 |
|
ballarin@28795
|
143 |
(** Read instantiation **)
|
ballarin@28795
|
144 |
|
ballarin@28872
|
145 |
(* Parse positional or named instantiation *)
|
ballarin@28872
|
146 |
|
ballarin@28859
|
147 |
local
|
ballarin@28859
|
148 |
|
haftmann@29734
|
149 |
fun prep_inst prep_term ctxt parms (Positional insts) =
|
wenzelm@50832
|
150 |
(insts ~~ parms) |> map
|
wenzelm@50832
|
151 |
(fn (NONE, p) => Free (p, dummyT)
|
wenzelm@50832
|
152 |
| (SOME t, _) => prep_term ctxt t)
|
haftmann@29734
|
153 |
| prep_inst prep_term ctxt parms (Named insts) =
|
wenzelm@50832
|
154 |
parms |> map (fn p =>
|
wenzelm@50832
|
155 |
(case AList.lookup (op =) insts p of
|
wenzelm@50832
|
156 |
SOME t => prep_term ctxt t |
|
wenzelm@50832
|
157 |
NONE => Free (p, dummyT)));
|
ballarin@28872
|
158 |
|
ballarin@28872
|
159 |
in
|
ballarin@28872
|
160 |
|
ballarin@28872
|
161 |
fun parse_inst x = prep_inst Syntax.parse_term x;
|
ballarin@28872
|
162 |
fun make_inst x = prep_inst (K I) x;
|
ballarin@28872
|
163 |
|
ballarin@28872
|
164 |
end;
|
ballarin@28872
|
165 |
|
ballarin@28872
|
166 |
|
ballarin@28872
|
167 |
(* Instantiation morphism *)
|
ballarin@28872
|
168 |
|
walther@60138
|
169 |
(*val inst_morphism: (string * typ) list -> (string * bool) * term list -> Proof.context ->
|
walther@60138
|
170 |
morphism * Proof.context*)
|
wneuper@59451
|
171 |
fun inst_morphism params ((prfx, mandatory), insts') ctxt =
|
ballarin@28795
|
172 |
let
|
walther@60138
|
173 |
val _ = writeln "#### Expression.inst_morphism";
|
ballarin@28795
|
174 |
(* parameters *)
|
walther@60138
|
175 |
val parm_types = map #2 (params: (string * typ) list);
|
wneuper@59451
|
176 |
val type_parms = fold Term.add_tfreesT parm_types [];
|
ballarin@28795
|
177 |
|
wneuper@59451
|
178 |
(* type inference *)
|
wenzelm@37153
|
179 |
val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
|
wneuper@59451
|
180 |
val type_parms' = fold Term.add_tvarsT parm_types' [];
|
wneuper@59451
|
181 |
val checked =
|
wneuper@59451
|
182 |
(map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts')
|
wneuper@59451
|
183 |
|> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
|
wneuper@59451
|
184 |
val (type_parms'', insts'') = chop (length type_parms') checked;
|
wneuper@59451
|
185 |
|
wneuper@59451
|
186 |
(* context *)
|
walther@60065
|
187 |
val ctxt' = fold Proof_Context.augment checked ctxt;
|
wneuper@59451
|
188 |
val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
|
wneuper@59451
|
189 |
val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
|
wenzelm@30350
|
190 |
|
ballarin@28795
|
191 |
(* instantiation *)
|
wneuper@59451
|
192 |
val instT =
|
wneuper@59451
|
193 |
(type_parms ~~ map Logic.dest_type type_parms'')
|
wneuper@59451
|
194 |
|> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
|
wneuper@59451
|
195 |
val cert_inst =
|
wneuper@59451
|
196 |
((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
|
wneuper@59451
|
197 |
|> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
|
ballarin@28795
|
198 |
in
|
wneuper@59451
|
199 |
(Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
|
wenzelm@56082
|
200 |
Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
|
ballarin@28795
|
201 |
end;
|
ballarin@28859
|
202 |
|
ballarin@28697
|
203 |
|
ballarin@28795
|
204 |
(*** Locale processing ***)
|
ballarin@28795
|
205 |
|
ballarin@28852
|
206 |
(** Parsing **)
|
ballarin@28852
|
207 |
|
wenzelm@29604
|
208 |
fun parse_elem prep_typ prep_term ctxt =
|
wenzelm@29604
|
209 |
Element.map_ctxt
|
wenzelm@29604
|
210 |
{binding = I,
|
wenzelm@29604
|
211 |
typ = prep_typ ctxt,
|
wenzelm@43231
|
212 |
term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt),
|
wenzelm@43231
|
213 |
pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt),
|
wenzelm@29604
|
214 |
fact = I,
|
wenzelm@29604
|
215 |
attrib = I};
|
ballarin@28852
|
216 |
|
wneuper@59324
|
217 |
fun prepare_stmt prep_prop prep_obtains ctxt stmt =
|
wneuper@59324
|
218 |
(case stmt of
|
wneuper@59324
|
219 |
Element.Shows raw_shows =>
|
wneuper@59324
|
220 |
raw_shows |> (map o apsnd o map) (fn (t, ps) =>
|
wneuper@59324
|
221 |
(prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t,
|
wneuper@59324
|
222 |
map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps))
|
wneuper@59324
|
223 |
| Element.Obtains raw_obtains =>
|
wneuper@59324
|
224 |
let
|
wneuper@59324
|
225 |
val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt;
|
wneuper@59324
|
226 |
val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
|
wneuper@59324
|
227 |
in map (fn (b, t) => ((b, []), [(t, [])])) obtains end);
|
ballarin@28852
|
228 |
|
ballarin@28852
|
229 |
|
wneuper@59324
|
230 |
(** Simultaneous type inference: instantiations + elements + statement **)
|
ballarin@28852
|
231 |
|
walther@60138
|
232 |
(**)local(**)
|
ballarin@28885
|
233 |
|
ballarin@28885
|
234 |
fun mk_type T = (Logic.mk_type T, []);
|
ballarin@28885
|
235 |
fun mk_term t = (t, []);
|
wenzelm@39541
|
236 |
fun mk_propp (p, pats) = (Type.constraint propT p, pats);
|
ballarin@28885
|
237 |
|
ballarin@28885
|
238 |
fun dest_type (T, []) = Logic.dest_type T;
|
ballarin@28885
|
239 |
fun dest_term (t, []) = t;
|
ballarin@28885
|
240 |
fun dest_propp (p, pats) = (p, pats);
|
ballarin@28885
|
241 |
|
ballarin@28885
|
242 |
fun extract_inst (_, (_, ts)) = map mk_term ts;
|
ballarin@28885
|
243 |
fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs));
|
ballarin@28885
|
244 |
|
wneuper@59451
|
245 |
fun extract_eqns es = map (mk_term o snd) es;
|
wneuper@59451
|
246 |
fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs;
|
wneuper@59451
|
247 |
|
ballarin@28885
|
248 |
fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes
|
ballarin@28885
|
249 |
| extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts
|
ballarin@28885
|
250 |
| extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms
|
ballarin@28885
|
251 |
| extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs
|
wneuper@59451
|
252 |
| extract_elem (Notes _) = []
|
wneuper@59451
|
253 |
| extract_elem (Lazy_Notes _) = [];
|
ballarin@28852
|
254 |
|
ballarin@28885
|
255 |
fun restore_elem (Fixes fixes, css) =
|
ballarin@28885
|
256 |
(fixes ~~ css) |> map (fn ((x, _, mx), cs) =>
|
ballarin@28885
|
257 |
(x, cs |> map dest_type |> try hd, mx)) |> Fixes
|
ballarin@28885
|
258 |
| restore_elem (Constrains csts, css) =
|
ballarin@28885
|
259 |
(csts ~~ css) |> map (fn ((x, _), cs) =>
|
ballarin@28885
|
260 |
(x, cs |> map dest_type |> hd)) |> Constrains
|
ballarin@28885
|
261 |
| restore_elem (Assumes asms, css) =
|
ballarin@28885
|
262 |
(asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes
|
ballarin@28885
|
263 |
| restore_elem (Defines defs, css) =
|
ballarin@28885
|
264 |
(defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
|
wneuper@59451
|
265 |
| restore_elem (elem as Notes _, _) = elem
|
wneuper@59451
|
266 |
| restore_elem (elem as Lazy_Notes _, _) = elem;
|
ballarin@28852
|
267 |
|
wneuper@59324
|
268 |
fun prep (_, pats) (ctxt, t :: ts) =
|
walther@60065
|
269 |
let val ctxt' = Proof_Context.augment t ctxt
|
wneuper@59324
|
270 |
in
|
wneuper@59324
|
271 |
((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
|
wneuper@59324
|
272 |
(ctxt', ts))
|
wneuper@59324
|
273 |
end;
|
wneuper@59324
|
274 |
|
walther@60138
|
275 |
(*WN*)
|
walther@60138
|
276 |
|
walther@60138
|
277 |
(*WN*)
|
walther@60138
|
278 |
(* val check: (term * term list) list -> Proof.context ->
|
walther@60138
|
279 |
(term * term list) list * Proof.context *)
|
wneuper@59324
|
280 |
fun check cs ctxt =
|
ballarin@28885
|
281 |
let
|
wneuper@59324
|
282 |
val (cs', (ctxt', _)) = fold_map prep cs
|
wneuper@59324
|
283 |
(ctxt, Syntax.check_terms
|
wneuper@59324
|
284 |
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
|
wneuper@59324
|
285 |
in (cs', ctxt') end;
|
ballarin@28885
|
286 |
|
walther@60138
|
287 |
(**)in(**)
|
ballarin@28885
|
288 |
|
wneuper@59451
|
289 |
fun check_autofix insts eqnss elems concl ctxt =
|
ballarin@28852
|
290 |
let
|
walther@60138
|
291 |
val _ = writeln "#### Expression.check_autofix";
|
ballarin@28885
|
292 |
val inst_cs = map extract_inst insts;
|
wneuper@59451
|
293 |
val eqns_cs = map extract_eqns eqnss;
|
ballarin@28885
|
294 |
val elem_css = map extract_elem elems;
|
wneuper@59324
|
295 |
val concl_cs = (map o map) mk_propp (map snd concl);
|
ballarin@28885
|
296 |
(* Type inference *)
|
wneuper@59451
|
297 |
val (inst_cs' :: eqns_cs' :: css', ctxt') =
|
wneuper@59451
|
298 |
(fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt;
|
ballarin@28934
|
299 |
val (elem_css', [concl_cs']) = chop (length elem_css) css';
|
ballarin@28885
|
300 |
in
|
wneuper@59324
|
301 |
((map restore_inst (insts ~~ inst_cs'),
|
wneuper@59451
|
302 |
map restore_eqns (eqnss ~~ eqns_cs'),
|
wenzelm@30781
|
303 |
map restore_elem (elems ~~ elem_css'),
|
wneuper@59324
|
304 |
map fst concl ~~ concl_cs'), ctxt')
|
ballarin@28885
|
305 |
end;
|
ballarin@28885
|
306 |
|
walther@60138
|
307 |
(**)end;(**)
|
ballarin@28852
|
308 |
|
ballarin@28852
|
309 |
|
ballarin@28795
|
310 |
(** Prepare locale elements **)
|
ballarin@28795
|
311 |
|
wneuper@59324
|
312 |
fun declare_elem prep_var (Fixes fixes) ctxt =
|
wneuper@59324
|
313 |
let val (vars, _) = fold_map prep_var fixes ctxt
|
wenzelm@43231
|
314 |
in ctxt |> Proof_Context.add_fixes vars |> snd end
|
wneuper@59324
|
315 |
| declare_elem prep_var (Constrains csts) ctxt =
|
wneuper@59324
|
316 |
ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd
|
ballarin@28872
|
317 |
| declare_elem _ (Assumes _) ctxt = ctxt
|
ballarin@28872
|
318 |
| declare_elem _ (Defines _) ctxt = ctxt
|
wneuper@59451
|
319 |
| declare_elem _ (Notes _) ctxt = ctxt
|
wneuper@59451
|
320 |
| declare_elem _ (Lazy_Notes _) ctxt = ctxt;
|
ballarin@28795
|
321 |
|
wenzelm@30781
|
322 |
|
ballarin@29221
|
323 |
(** Finish locale elements **)
|
ballarin@28795
|
324 |
|
wenzelm@50834
|
325 |
fun finish_inst ctxt (loc, (prfx, inst)) =
|
wenzelm@50834
|
326 |
let
|
wenzelm@50834
|
327 |
val thy = Proof_Context.theory_of ctxt;
|
wneuper@59451
|
328 |
val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt;
|
wenzelm@50834
|
329 |
in (loc, morph) end;
|
wenzelm@50834
|
330 |
|
wenzelm@50833
|
331 |
fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
|
wenzelm@50833
|
332 |
let val x = Binding.name_of binding
|
wenzelm@50833
|
333 |
in (binding, AList.lookup (op =) parms x, mx) end);
|
wenzelm@50832
|
334 |
|
wenzelm@50832
|
335 |
local
|
wenzelm@50832
|
336 |
|
ballarin@28852
|
337 |
fun closeup _ _ false elem = elem
|
wenzelm@50834
|
338 |
| closeup (outer_ctxt, ctxt) parms true elem =
|
ballarin@28795
|
339 |
let
|
wenzelm@30728
|
340 |
(* FIXME consider closing in syntactic phase -- before type checking *)
|
ballarin@28795
|
341 |
fun close_frees t =
|
ballarin@28795
|
342 |
let
|
ballarin@28795
|
343 |
val rev_frees =
|
ballarin@28795
|
344 |
Term.fold_aterms (fn Free (x, T) =>
|
wenzelm@50834
|
345 |
if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I
|
wenzelm@50834
|
346 |
else insert (op =) (x, T) | _ => I) t [];
|
wenzelm@30728
|
347 |
in fold (Logic.all o Free) rev_frees t end;
|
ballarin@28795
|
348 |
|
ballarin@28795
|
349 |
fun no_binds [] = []
|
ballarin@28852
|
350 |
| no_binds _ = error "Illegal term bindings in context element";
|
ballarin@28795
|
351 |
in
|
ballarin@28795
|
352 |
(case elem of
|
ballarin@28795
|
353 |
Assumes asms => Assumes (asms |> map (fn (a, propps) =>
|
ballarin@28795
|
354 |
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
|
ballarin@29022
|
355 |
| Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
|
wneuper@59324
|
356 |
let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t)
|
wenzelm@30448
|
357 |
in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
|
ballarin@28795
|
358 |
| e => e)
|
ballarin@28795
|
359 |
end;
|
ballarin@28795
|
360 |
|
wenzelm@50834
|
361 |
in
|
wenzelm@50834
|
362 |
|
wenzelm@50833
|
363 |
fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes)
|
wenzelm@50833
|
364 |
| finish_elem _ _ _ (Constrains _) = Constrains []
|
wenzelm@50834
|
365 |
| finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms)
|
wenzelm@50834
|
366 |
| finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs)
|
wneuper@59451
|
367 |
| finish_elem _ _ _ (elem as Notes _) = elem
|
wneuper@59451
|
368 |
| finish_elem _ _ _ (elem as Lazy_Notes _) = elem;
|
ballarin@28872
|
369 |
|
wenzelm@50832
|
370 |
end;
|
wenzelm@50832
|
371 |
|
ballarin@28795
|
372 |
|
wneuper@59324
|
373 |
(** Process full context statement: instantiations + elements + statement **)
|
ballarin@28895
|
374 |
|
ballarin@28895
|
375 |
(* Interleave incremental parsing and type inference over entire parsed stretch. *)
|
ballarin@28895
|
376 |
|
ballarin@28795
|
377 |
local
|
ballarin@28795
|
378 |
|
wneuper@59451
|
379 |
fun abs_def ctxt =
|
wneuper@59451
|
380 |
Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of;
|
wneuper@59451
|
381 |
|
wenzelm@47804
|
382 |
fun prep_full_context_statement
|
wneuper@59451
|
383 |
parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr
|
wneuper@59324
|
384 |
{strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
|
ballarin@28795
|
385 |
let
|
wenzelm@43231
|
386 |
val thy = Proof_Context.theory_of ctxt1;
|
ballarin@28872
|
387 |
|
ballarin@28895
|
388 |
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
|
ballarin@28895
|
389 |
|
wneuper@59451
|
390 |
fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
|
ballarin@28872
|
391 |
let
|
wneuper@59451
|
392 |
val params = map #1 (Locale.params_of thy loc);
|
wneuper@59451
|
393 |
val inst' = prep_inst ctxt (map #1 params) inst;
|
wneuper@59451
|
394 |
val parm_types' =
|
wneuper@59451
|
395 |
params |> map (#2 #> Logic.varifyT_global #>
|
wneuper@59451
|
396 |
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
|
wneuper@59451
|
397 |
Type_Infer.paramify_vars);
|
wenzelm@39541
|
398 |
val inst'' = map2 Type.constraint parm_types' inst';
|
ballarin@28872
|
399 |
val insts' = insts @ [(loc, (prfx, inst''))];
|
wneuper@59451
|
400 |
val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
|
ballarin@28872
|
401 |
val inst''' = insts'' |> List.last |> snd |> snd;
|
wneuper@59451
|
402 |
val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
|
wneuper@59451
|
403 |
val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
|
wneuper@59451
|
404 |
handle ERROR msg => if null eqns then error msg else
|
walther@60065
|
405 |
(Locale.tracing ctxt1
|
walther@60065
|
406 |
(msg ^ "\nFalling back to reading rewrites clause before activation.");
|
walther@60065
|
407 |
ctxt2);
|
wneuper@59451
|
408 |
|
wneuper@59451
|
409 |
val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
|
wneuper@59451
|
410 |
val eqns' = (prep_eqns ctxt' o map snd) eqns;
|
wneuper@59451
|
411 |
val eqnss' = [attrss ~~ eqns'];
|
wneuper@59451
|
412 |
val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt';
|
wneuper@59451
|
413 |
val rewrite_morph = eqns'
|
wneuper@59451
|
414 |
|> map (abs_def ctxt')
|
wneuper@59451
|
415 |
|> Variable.export_terms ctxt' ctxt
|
wneuper@59451
|
416 |
|> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
|
wneuper@59451
|
417 |
|> the_default Morphism.identity;
|
wneuper@59451
|
418 |
val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
|
wneuper@59451
|
419 |
val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
|
wneuper@59451
|
420 |
in (i + 1, insts', eqnss', ctxt'') end;
|
wenzelm@30350
|
421 |
|
haftmann@52866
|
422 |
fun prep_elem raw_elem ctxt =
|
ballarin@28852
|
423 |
let
|
wenzelm@48189
|
424 |
val ctxt' = ctxt
|
wenzelm@48189
|
425 |
|> Context_Position.set_visible false
|
wneuper@59324
|
426 |
|> declare_elem prep_var_elem raw_elem
|
wenzelm@48189
|
427 |
|> Context_Position.restore_visible ctxt;
|
wenzelm@48189
|
428 |
val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
|
haftmann@29501
|
429 |
in (elems', ctxt') end;
|
ballarin@28795
|
430 |
|
wneuper@59324
|
431 |
val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
|
wenzelm@43231
|
432 |
val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
|
wneuper@59451
|
433 |
val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2);
|
wenzelm@30793
|
434 |
|
wneuper@59324
|
435 |
fun prep_stmt elems ctxt =
|
wneuper@59451
|
436 |
check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
|
wneuper@59324
|
437 |
|
wenzelm@30793
|
438 |
val _ =
|
wenzelm@30793
|
439 |
if fixed_frees then ()
|
wenzelm@30793
|
440 |
else
|
wenzelm@43353
|
441 |
(case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of
|
wenzelm@30793
|
442 |
[] => ()
|
wenzelm@30793
|
443 |
| frees => error ("Illegal free variables in expression: " ^
|
wenzelm@30793
|
444 |
commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
|
wenzelm@30793
|
445 |
|
wneuper@59451
|
446 |
val ((insts, _, elems', concl), ctxt4) = ctxt3
|
wneuper@59324
|
447 |
|> init_body
|
wneuper@59324
|
448 |
|> fold_map prep_elem raw_elems
|
wneuper@59324
|
449 |
|-> prep_stmt;
|
ballarin@28795
|
450 |
|
wneuper@59324
|
451 |
|
wneuper@59324
|
452 |
(* parameters from expression and elements *)
|
wneuper@59324
|
453 |
|
haftmann@56220
|
454 |
val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
|
haftmann@56220
|
455 |
(Fixes fors :: elems');
|
wneuper@59324
|
456 |
val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4;
|
ballarin@28795
|
457 |
|
wenzelm@50833
|
458 |
val fors' = finish_fixes parms fors;
|
wenzelm@30762
|
459 |
val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
|
wneuper@59324
|
460 |
val deps = map (finish_inst ctxt5) insts;
|
wneuper@59324
|
461 |
val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
|
ballarin@28852
|
462 |
|
wneuper@59451
|
463 |
in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end;
|
ballarin@28795
|
464 |
|
ballarin@28795
|
465 |
in
|
ballarin@28795
|
466 |
|
haftmann@29501
|
467 |
fun cert_full_context_statement x =
|
wneuper@59324
|
468 |
prep_full_context_statement (K I) (K I) Obtain.cert_obtains
|
wneuper@59451
|
469 |
Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
|
wenzelm@30781
|
470 |
|
haftmann@29501
|
471 |
fun cert_read_full_context_statement x =
|
wneuper@59324
|
472 |
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
|
wneuper@59451
|
473 |
Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
|
wenzelm@30781
|
474 |
|
ballarin@28895
|
475 |
fun read_full_context_statement x =
|
wneuper@59324
|
476 |
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
|
wneuper@59451
|
477 |
Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x;
|
ballarin@28795
|
478 |
|
ballarin@28795
|
479 |
end;
|
ballarin@28795
|
480 |
|
ballarin@28795
|
481 |
|
wneuper@59324
|
482 |
(* Context statement: elements + statement *)
|
ballarin@28795
|
483 |
|
ballarin@28795
|
484 |
local
|
ballarin@28795
|
485 |
|
wneuper@59324
|
486 |
fun prep_statement prep activate raw_elems raw_stmt ctxt =
|
ballarin@28898
|
487 |
let
|
wneuper@59451
|
488 |
val ((_, _, _, elems, concl), _) =
|
wenzelm@50832
|
489 |
prep {strict = true, do_close = false, fixed_frees = true}
|
wneuper@59324
|
490 |
([], []) I raw_elems raw_stmt ctxt;
|
wneuper@59324
|
491 |
val ctxt' = ctxt
|
wenzelm@50832
|
492 |
|> Proof_Context.set_stmt true
|
wneuper@59324
|
493 |
|> fold_map activate elems |> #2
|
wneuper@59324
|
494 |
|> Proof_Context.restore_stmt ctxt;
|
wneuper@59324
|
495 |
in (concl, ctxt') end;
|
ballarin@28898
|
496 |
|
ballarin@28898
|
497 |
in
|
ballarin@28898
|
498 |
|
haftmann@29501
|
499 |
fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
|
ballarin@28898
|
500 |
fun read_statement x = prep_statement read_full_context_statement Element.activate x;
|
ballarin@28898
|
501 |
|
ballarin@28898
|
502 |
end;
|
ballarin@28898
|
503 |
|
ballarin@28898
|
504 |
|
ballarin@28898
|
505 |
(* Locale declaration: import + elements *)
|
ballarin@28898
|
506 |
|
wenzelm@30762
|
507 |
fun fix_params params =
|
wenzelm@43231
|
508 |
Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
|
wenzelm@30762
|
509 |
|
ballarin@28898
|
510 |
local
|
ballarin@28898
|
511 |
|
wneuper@59324
|
512 |
fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
|
ballarin@28795
|
513 |
let
|
wneuper@59451
|
514 |
val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) =
|
wenzelm@30793
|
515 |
prep {strict = false, do_close = true, fixed_frees = false}
|
wneuper@59324
|
516 |
raw_import init_body raw_elems (Element.Shows []) ctxt;
|
wneuper@59451
|
517 |
val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale";
|
ballarin@28898
|
518 |
(* Declare parameters and imported facts *)
|
wneuper@59324
|
519 |
val ctxt' = ctxt
|
wneuper@59324
|
520 |
|> fix_params fixed
|
wneuper@59324
|
521 |
|> fold (Context.proof_map o Locale.activate_facts NONE) deps;
|
wneuper@59324
|
522 |
val (elems', ctxt'') = ctxt'
|
wneuper@59324
|
523 |
|> Proof_Context.set_stmt true
|
wneuper@59324
|
524 |
|> fold_map activate elems
|
wneuper@59324
|
525 |
||> Proof_Context.restore_stmt ctxt';
|
wneuper@59324
|
526 |
in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
|
ballarin@28795
|
527 |
|
ballarin@28795
|
528 |
in
|
ballarin@28795
|
529 |
|
haftmann@29501
|
530 |
fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
|
haftmann@29501
|
531 |
fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x;
|
ballarin@28898
|
532 |
fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
|
ballarin@28879
|
533 |
|
ballarin@28898
|
534 |
end;
|
ballarin@28898
|
535 |
|
ballarin@28898
|
536 |
|
ballarin@28898
|
537 |
(* Locale expression to set up a goal *)
|
ballarin@28898
|
538 |
|
ballarin@28898
|
539 |
local
|
ballarin@28898
|
540 |
|
ballarin@28898
|
541 |
fun props_of thy (name, morph) =
|
walther@59606
|
542 |
let val (asm, defs) = Locale.specification_of thy name
|
walther@59606
|
543 |
in map (Morphism.term morph) (the_list asm @ defs) end;
|
ballarin@28898
|
544 |
|
wneuper@59324
|
545 |
fun prep_goal_expression prep expression ctxt =
|
ballarin@28898
|
546 |
let
|
wneuper@59324
|
547 |
val thy = Proof_Context.theory_of ctxt;
|
ballarin@28898
|
548 |
|
wneuper@59451
|
549 |
val ((fixed, deps, eqnss, _, _), _) =
|
wneuper@59324
|
550 |
prep {strict = true, do_close = true, fixed_frees = true} expression I []
|
wneuper@59324
|
551 |
(Element.Shows []) ctxt;
|
ballarin@28898
|
552 |
(* proof obligations *)
|
ballarin@28898
|
553 |
val propss = map (props_of thy) deps;
|
wneuper@59451
|
554 |
val eq_propss = (map o map) snd eqnss;
|
ballarin@28898
|
555 |
|
wneuper@59324
|
556 |
val goal_ctxt = ctxt
|
wneuper@59324
|
557 |
|> fix_params fixed
|
walther@60065
|
558 |
|> (fold o fold) Proof_Context.augment (propss @ eq_propss);
|
ballarin@28898
|
559 |
|
walther@60065
|
560 |
val export = Proof_Context.export_morphism goal_ctxt ctxt;
|
ballarin@28898
|
561 |
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
|
wenzelm@31979
|
562 |
val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
|
ballarin@28898
|
563 |
val exp_typ = Logic.type_map exp_term;
|
wenzelm@46160
|
564 |
val export' =
|
wenzelm@56082
|
565 |
Morphism.morphism "Expression.prep_goal"
|
wenzelm@56082
|
566 |
{binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
|
wneuper@59451
|
567 |
in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
|
wenzelm@30350
|
568 |
|
ballarin@28898
|
569 |
in
|
ballarin@28898
|
570 |
|
haftmann@29501
|
571 |
fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
|
ballarin@28898
|
572 |
fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
|
ballarin@28879
|
573 |
|
ballarin@28795
|
574 |
end;
|
ballarin@28795
|
575 |
|
ballarin@28795
|
576 |
|
ballarin@28795
|
577 |
(*** Locale declarations ***)
|
ballarin@28795
|
578 |
|
ballarin@29221
|
579 |
(* extract specification text *)
|
ballarin@29221
|
580 |
|
ballarin@29221
|
581 |
val norm_term = Envir.beta_norm oo Term.subst_atomic;
|
ballarin@29221
|
582 |
|
ballarin@29221
|
583 |
fun bind_def ctxt eq (xs, env, eqs) =
|
ballarin@29221
|
584 |
let
|
wneuper@59324
|
585 |
val _ = Local_Defs.cert_def ctxt (K []) eq;
|
wenzelm@35624
|
586 |
val ((y, T), b) = Local_Defs.abs_def eq;
|
ballarin@29221
|
587 |
val b' = norm_term env b;
|
ballarin@29221
|
588 |
fun err msg = error (msg ^ ": " ^ quote y);
|
ballarin@29221
|
589 |
in
|
wenzelm@50764
|
590 |
(case filter (fn (Free (y', _), _) => y = y' | _ => false) env of
|
wenzelm@50764
|
591 |
[] => (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
|
wenzelm@50764
|
592 |
| dups =>
|
wenzelm@50764
|
593 |
if forall (fn (_, b'') => b' aconv b'') dups then (xs, env, eqs)
|
wenzelm@50764
|
594 |
else err "Attempt to redefine variable")
|
ballarin@29221
|
595 |
end;
|
ballarin@29221
|
596 |
|
ballarin@29221
|
597 |
(* text has the following structure:
|
ballarin@29221
|
598 |
(((exts, exts'), (ints, ints')), (xs, env, defs))
|
ballarin@29221
|
599 |
where
|
ballarin@29221
|
600 |
exts: external assumptions (terms in assumes elements)
|
ballarin@29221
|
601 |
exts': dito, normalised wrt. env
|
ballarin@29221
|
602 |
ints: internal assumptions (terms in assumptions from insts)
|
ballarin@29221
|
603 |
ints': dito, normalised wrt. env
|
ballarin@29221
|
604 |
xs: the free variables in exts' and ints' and rhss of definitions,
|
ballarin@29221
|
605 |
this includes parameters except defined parameters
|
ballarin@29221
|
606 |
env: list of term pairs encoding substitutions, where the first term
|
ballarin@29221
|
607 |
is a free variable; substitutions represent defines elements and
|
ballarin@29221
|
608 |
the rhs is normalised wrt. the previous env
|
ballarin@29221
|
609 |
defs: the equations from the defines elements
|
ballarin@29221
|
610 |
*)
|
ballarin@29221
|
611 |
|
ballarin@29221
|
612 |
fun eval_text _ _ (Fixes _) text = text
|
ballarin@29221
|
613 |
| eval_text _ _ (Constrains _) text = text
|
ballarin@29221
|
614 |
| eval_text _ is_ext (Assumes asms)
|
ballarin@29221
|
615 |
(((exts, exts'), (ints, ints')), (xs, env, defs)) =
|
ballarin@29221
|
616 |
let
|
ballarin@29221
|
617 |
val ts = maps (map #1 o #2) asms;
|
ballarin@29221
|
618 |
val ts' = map (norm_term env) ts;
|
ballarin@29221
|
619 |
val spec' =
|
ballarin@29221
|
620 |
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
|
ballarin@29221
|
621 |
else ((exts, exts'), (ints @ ts, ints' @ ts'));
|
ballarin@29221
|
622 |
in (spec', (fold Term.add_frees ts' xs, env, defs)) end
|
ballarin@29221
|
623 |
| eval_text ctxt _ (Defines defs) (spec, binds) =
|
ballarin@29221
|
624 |
(spec, fold (bind_def ctxt o #1 o #2) defs binds)
|
wneuper@59451
|
625 |
| eval_text _ _ (Notes _) text = text
|
wneuper@59451
|
626 |
| eval_text _ _ (Lazy_Notes _) text = text;
|
ballarin@29221
|
627 |
|
ballarin@29221
|
628 |
fun eval_inst ctxt (loc, morph) text =
|
ballarin@29221
|
629 |
let
|
wenzelm@43231
|
630 |
val thy = Proof_Context.theory_of ctxt;
|
haftmann@29360
|
631 |
val (asm, defs) = Locale.specification_of thy loc;
|
ballarin@29221
|
632 |
val asm' = Option.map (Morphism.term morph) asm;
|
ballarin@29221
|
633 |
val defs' = map (Morphism.term morph) defs;
|
wenzelm@56981
|
634 |
val text' =
|
wenzelm@56981
|
635 |
text |>
|
wenzelm@56981
|
636 |
(if is_some asm then
|
wneuper@59324
|
637 |
eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])])
|
ballarin@29221
|
638 |
else I) |>
|
wenzelm@56981
|
639 |
(if not (null defs) then
|
wneuper@59324
|
640 |
eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs'))
|
ballarin@29221
|
641 |
else I)
|
haftmann@29360
|
642 |
(* FIXME clone from locale.ML *)
|
ballarin@29221
|
643 |
in text' end;
|
ballarin@29221
|
644 |
|
ballarin@29221
|
645 |
fun eval_elem ctxt elem text =
|
wenzelm@30728
|
646 |
eval_text ctxt true elem text;
|
ballarin@29221
|
647 |
|
ballarin@29221
|
648 |
fun eval ctxt deps elems =
|
ballarin@29221
|
649 |
let
|
ballarin@29221
|
650 |
val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [], []));
|
ballarin@29221
|
651 |
val ((spec, (_, _, defs))) = fold (eval_elem ctxt) elems text';
|
ballarin@29221
|
652 |
in (spec, defs) end;
|
ballarin@29221
|
653 |
|
ballarin@28903
|
654 |
(* axiomsN: name of theorem set with destruct rules for locale predicates,
|
ballarin@28903
|
655 |
also name suffix of delta predicates and assumptions. *)
|
ballarin@28903
|
656 |
|
ballarin@28903
|
657 |
val axiomsN = "axioms";
|
ballarin@28903
|
658 |
|
ballarin@28795
|
659 |
local
|
ballarin@28795
|
660 |
|
ballarin@28795
|
661 |
(* introN: name of theorems for introduction rules of locale and
|
ballarin@28903
|
662 |
delta predicates *)
|
ballarin@28795
|
663 |
|
ballarin@28795
|
664 |
val introN = "intro";
|
ballarin@28795
|
665 |
|
wneuper@59180
|
666 |
fun atomize_spec ctxt ts =
|
ballarin@28795
|
667 |
let
|
ballarin@28795
|
668 |
val t = Logic.mk_conjunction_balanced ts;
|
wneuper@59180
|
669 |
val body = Object_Logic.atomize_term ctxt t;
|
ballarin@28795
|
670 |
val bodyT = Term.fastype_of body;
|
ballarin@28795
|
671 |
in
|
wenzelm@56981
|
672 |
if bodyT = propT
|
wneuper@59180
|
673 |
then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t))
|
wneuper@59180
|
674 |
else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t))
|
ballarin@28795
|
675 |
end;
|
ballarin@28795
|
676 |
|
ballarin@28795
|
677 |
(* achieve plain syntax for locale predicates (without "PROP") *)
|
ballarin@28795
|
678 |
|
wenzelm@50835
|
679 |
fun aprop_tr' n c =
|
wenzelm@50835
|
680 |
let
|
wenzelm@50835
|
681 |
val c' = Lexicon.mark_const c;
|
wenzelm@53280
|
682 |
fun tr' (_: Proof.context) T args =
|
wenzelm@50835
|
683 |
if T <> dummyT andalso length args = n
|
wenzelm@50835
|
684 |
then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args)
|
wenzelm@50835
|
685 |
else raise Match;
|
wenzelm@50835
|
686 |
in (c', tr') end;
|
ballarin@28795
|
687 |
|
ballarin@28898
|
688 |
(* define one predicate including its intro rule and axioms
|
haftmann@33360
|
689 |
- binding: predicate name
|
ballarin@28795
|
690 |
- parms: locale parameters
|
ballarin@28795
|
691 |
- defs: thms representing substitutions from defines elements
|
ballarin@28795
|
692 |
- ts: terms representing locale assumptions (not normalised wrt. defs)
|
ballarin@28795
|
693 |
- norm_ts: terms representing locale assumptions (normalised wrt. defs)
|
ballarin@28795
|
694 |
- thy: the theory
|
ballarin@28795
|
695 |
*)
|
ballarin@28795
|
696 |
|
haftmann@33360
|
697 |
fun def_pred binding parms defs ts norm_ts thy =
|
ballarin@28795
|
698 |
let
|
haftmann@33360
|
699 |
val name = Sign.full_name thy binding;
|
ballarin@28795
|
700 |
|
wneuper@59180
|
701 |
val thy_ctxt = Proof_Context.init_global thy;
|
wneuper@59180
|
702 |
|
wneuper@59180
|
703 |
val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts;
|
wenzelm@29272
|
704 |
val env = Term.add_free_names body [];
|
ballarin@28795
|
705 |
val xs = filter (member (op =) env o #1) parms;
|
ballarin@28795
|
706 |
val Ts = map #2 xs;
|
wenzelm@29272
|
707 |
val extraTs =
|
haftmann@33040
|
708 |
(subtract (op =) (fold Term.add_tfreesT Ts []) (Term.add_tfrees body []))
|
wneuper@59324
|
709 |
|> sort_by #1 |> map TFree;
|
ballarin@28795
|
710 |
val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
|
ballarin@28795
|
711 |
|
ballarin@28795
|
712 |
val args = map Logic.mk_type extraTs @ map Free xs;
|
ballarin@28795
|
713 |
val head = Term.list_comb (Const (name, predT), args);
|
wneuper@59180
|
714 |
val statement = Object_Logic.ensure_propT thy_ctxt head;
|
ballarin@28795
|
715 |
|
ballarin@28795
|
716 |
val ([pred_def], defs_thy) =
|
ballarin@28795
|
717 |
thy
|
wenzelm@53280
|
718 |
|> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
|
wneuper@59324
|
719 |
|> Sign.declare_const_global ((binding, predT), NoSyn) |> snd
|
wneuper@59324
|
720 |
|> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])];
|
wenzelm@43231
|
721 |
val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
|
ballarin@28795
|
722 |
|
wenzelm@56084
|
723 |
val intro = Goal.prove_global defs_thy [] norm_ts statement
|
wenzelm@56084
|
724 |
(fn {context = ctxt, ...} =>
|
wenzelm@56084
|
725 |
rewrite_goals_tac ctxt [pred_def] THEN
|
wneuper@59180
|
726 |
compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
|
wneuper@59180
|
727 |
compose_tac defs_ctxt
|
wneuper@59180
|
728 |
(false,
|
wneuper@59180
|
729 |
Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
|
ballarin@28795
|
730 |
|
ballarin@28795
|
731 |
val conjuncts =
|
wenzelm@56084
|
732 |
(Drule.equal_elim_rule2 OF
|
wneuper@59180
|
733 |
[body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))])
|
ballarin@28795
|
734 |
|> Conjunction.elim_balanced (length ts);
|
wenzelm@55939
|
735 |
|
wenzelm@55939
|
736 |
val (_, axioms_ctxt) = defs_ctxt
|
wneuper@59324
|
737 |
|> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts));
|
ballarin@28795
|
738 |
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
|
wenzelm@55939
|
739 |
Element.prove_witness axioms_ctxt t
|
wneuper@59180
|
740 |
(rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
|
ballarin@28795
|
741 |
in ((statement, intro, axioms), defs_thy) end;
|
ballarin@28795
|
742 |
|
ballarin@28795
|
743 |
in
|
ballarin@28795
|
744 |
|
wenzelm@30350
|
745 |
(* main predicate definition function *)
|
ballarin@28795
|
746 |
|
haftmann@33360
|
747 |
fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
|
ballarin@28795
|
748 |
let
|
wenzelm@56225
|
749 |
val ctxt = Proof_Context.init_global thy;
|
wneuper@59180
|
750 |
val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs;
|
ballarin@29031
|
751 |
|
ballarin@28795
|
752 |
val (a_pred, a_intro, a_axioms, thy'') =
|
ballarin@28795
|
753 |
if null exts then (NONE, NONE, [], thy)
|
ballarin@28795
|
754 |
else
|
ballarin@28795
|
755 |
let
|
wenzelm@56981
|
756 |
val abinding =
|
wenzelm@56981
|
757 |
if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
|
ballarin@28795
|
758 |
val ((statement, intro, axioms), thy') =
|
ballarin@28795
|
759 |
thy
|
haftmann@33360
|
760 |
|> def_pred abinding parms defs' exts exts';
|
walther@60065
|
761 |
val ((_, [intro']), thy'') =
|
ballarin@28795
|
762 |
thy'
|
wenzelm@35215
|
763 |
|> Sign.qualified_path true abinding
|
wneuper@59451
|
764 |
|> Global_Theory.note_thms ""
|
wneuper@59451
|
765 |
((Binding.name introN, []), [([intro], [Locale.unfold_add])])
|
ballarin@28795
|
766 |
||> Sign.restore_naming thy';
|
walther@60065
|
767 |
in (SOME statement, SOME intro', axioms, thy'') end;
|
ballarin@28795
|
768 |
val (b_pred, b_intro, b_axioms, thy'''') =
|
ballarin@28795
|
769 |
if null ints then (NONE, NONE, [], thy'')
|
ballarin@28795
|
770 |
else
|
ballarin@28795
|
771 |
let
|
ballarin@28795
|
772 |
val ((statement, intro, axioms), thy''') =
|
ballarin@28795
|
773 |
thy''
|
haftmann@33360
|
774 |
|> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
|
wenzelm@56225
|
775 |
val ctxt''' = Proof_Context.init_global thy''';
|
walther@60065
|
776 |
val ([(_, [intro']), _], thy'''') =
|
ballarin@28795
|
777 |
thy'''
|
wenzelm@35215
|
778 |
|> Sign.qualified_path true binding
|
wenzelm@39814
|
779 |
|> Global_Theory.note_thmss ""
|
wneuper@59324
|
780 |
[((Binding.name introN, []), [([intro], [Locale.intro_add])]),
|
wneuper@59324
|
781 |
((Binding.name axiomsN, []),
|
wenzelm@56225
|
782 |
[(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
|
wenzelm@56225
|
783 |
[])])]
|
ballarin@28795
|
784 |
||> Sign.restore_naming thy''';
|
walther@60065
|
785 |
in (SOME statement, SOME intro', axioms, thy'''') end;
|
ballarin@28795
|
786 |
in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
|
ballarin@28795
|
787 |
|
ballarin@28795
|
788 |
end;
|
ballarin@28795
|
789 |
|
ballarin@28795
|
790 |
|
ballarin@28795
|
791 |
local
|
ballarin@28795
|
792 |
|
ballarin@28795
|
793 |
fun assumes_to_notes (Assumes asms) axms =
|
ballarin@28795
|
794 |
fold_map (fn (a, spec) => fn axs =>
|
ballarin@28795
|
795 |
let val (ps, qs) = chop (length spec) axs
|
ballarin@28795
|
796 |
in ((a, [(ps, [])]), qs) end) asms axms
|
wenzelm@33644
|
797 |
|> apfst (curry Notes "")
|
ballarin@28795
|
798 |
| assumes_to_notes e axms = (e, axms);
|
ballarin@28795
|
799 |
|
wenzelm@56225
|
800 |
fun defines_to_notes ctxt (Defines defs) =
|
wenzelm@43311
|
801 |
Notes ("", map (fn (a, (def, _)) =>
|
wneuper@59180
|
802 |
(a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
|
wenzelm@30728
|
803 |
[(Attrib.internal o K) Locale.witness_add])])) defs)
|
ballarin@29031
|
804 |
| defines_to_notes _ e = e;
|
ballarin@28795
|
805 |
|
wneuper@59451
|
806 |
val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
|
wneuper@59180
|
807 |
|
ballarin@28898
|
808 |
fun gen_add_locale prep_decl
|
haftmann@58523
|
809 |
binding raw_predicate_binding raw_import raw_body thy =
|
ballarin@28795
|
810 |
let
|
haftmann@33360
|
811 |
val name = Sign.full_name thy binding;
|
haftmann@29389
|
812 |
val _ = Locale.defined thy name andalso
|
ballarin@28795
|
813 |
error ("Duplicate definition of locale " ^ quote name);
|
ballarin@28795
|
814 |
|
wenzelm@48185
|
815 |
val ((fixed, deps, body_elems, _), (parms, ctxt')) =
|
wenzelm@43231
|
816 |
prep_decl raw_import I raw_body (Proof_Context.init_global thy);
|
ballarin@29221
|
817 |
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
|
ballarin@29221
|
818 |
|
wenzelm@37331
|
819 |
val extraTs =
|
wenzelm@56981
|
820 |
subtract (op =)
|
wenzelm@56981
|
821 |
(fold Term.add_tfreesT (map snd parms) [])
|
wenzelm@56981
|
822 |
(fold Term.add_tfrees exts' []);
|
wenzelm@37331
|
823 |
val _ =
|
wenzelm@37331
|
824 |
if null extraTs then ()
|
wenzelm@37331
|
825 |
else warning ("Additional type variable(s) in locale specification " ^
|
wenzelm@43252
|
826 |
Binding.print binding ^ ": " ^
|
wneuper@59324
|
827 |
commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs)));
|
wenzelm@37331
|
828 |
|
haftmann@33360
|
829 |
val predicate_binding =
|
haftmann@33360
|
830 |
if Binding.is_empty raw_predicate_binding then binding
|
haftmann@33360
|
831 |
else raw_predicate_binding;
|
ballarin@28872
|
832 |
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
|
haftmann@33360
|
833 |
define_preds predicate_binding parms text thy;
|
wenzelm@56225
|
834 |
val pred_ctxt = Proof_Context.init_global thy';
|
ballarin@28795
|
835 |
|
ballarin@29035
|
836 |
val a_satisfy = Element.satisfy_morphism a_axioms;
|
ballarin@29035
|
837 |
val b_satisfy = Element.satisfy_morphism b_axioms;
|
ballarin@28903
|
838 |
|
ballarin@28895
|
839 |
val params = fixed @
|
wenzelm@30762
|
840 |
maps (fn Fixes fixes =>
|
wenzelm@30762
|
841 |
map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
|
ballarin@28903
|
842 |
val asm = if is_some b_statement then b_statement else a_statement;
|
ballarin@29028
|
843 |
|
wneuper@59180
|
844 |
val hyp_spec = filter is_hyp body_elems;
|
wneuper@59180
|
845 |
|
ballarin@29028
|
846 |
val notes =
|
wenzelm@33278
|
847 |
if is_some asm then
|
wneuper@59324
|
848 |
[("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
|
wneuper@59180
|
849 |
[([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
|
wenzelm@33278
|
850 |
[(Attrib.internal o K) Locale.witness_add])])])]
|
wenzelm@30728
|
851 |
else [];
|
ballarin@28795
|
852 |
|
wenzelm@56981
|
853 |
val notes' =
|
wenzelm@56981
|
854 |
body_elems
|
wenzelm@56981
|
855 |
|> map (defines_to_notes pred_ctxt)
|
wenzelm@56981
|
856 |
|> map (Element.transform_ctxt a_satisfy)
|
wenzelm@56981
|
857 |
|> (fn elems =>
|
wenzelm@56981
|
858 |
fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms))
|
wenzelm@56981
|
859 |
|> fst
|
wenzelm@56981
|
860 |
|> map (Element.transform_ctxt b_satisfy)
|
wenzelm@56981
|
861 |
|> map_filter (fn Notes notes => SOME notes | _ => NONE);
|
ballarin@29035
|
862 |
|
ballarin@29035
|
863 |
val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
|
wenzelm@56225
|
864 |
val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
|
ballarin@28872
|
865 |
|
haftmann@29358
|
866 |
val loc_ctxt = thy'
|
haftmann@33360
|
867 |
|> Locale.register_locale binding (extraTs, params)
|
wneuper@59180
|
868 |
(asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
|
haftmann@58523
|
869 |
|> Named_Target.init name
|
wenzelm@33673
|
870 |
|> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
|
ballarin@29028
|
871 |
|
haftmann@29358
|
872 |
in (name, loc_ctxt) end;
|
ballarin@28795
|
873 |
|
ballarin@28795
|
874 |
in
|
ballarin@28795
|
875 |
|
haftmann@29501
|
876 |
val add_locale = gen_add_locale cert_declaration;
|
ballarin@28902
|
877 |
val add_locale_cmd = gen_add_locale read_declaration;
|
ballarin@28795
|
878 |
|
ballarin@28795
|
879 |
end;
|
ballarin@28795
|
880 |
|
ballarin@28993
|
881 |
end;
|