5 New locale development --- experimental. |
5 New locale development --- experimental. |
6 *) |
6 *) |
7 |
7 |
8 signature EXPRESSION = |
8 signature EXPRESSION = |
9 sig |
9 sig |
10 type map |
10 type 'term map |
11 type 'morph expr |
11 type 'morph expr |
12 |
12 |
13 val empty_expr: 'morph expr |
13 val empty_expr: 'morph expr |
14 |
14 |
15 type expression = (string * map) expr * (Name.binding * string option * mixfix) list |
15 type expression = (string * string map) expr * (Name.binding * string option * mixfix) list |
16 type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list |
16 (* type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *) |
17 |
17 |
18 (* Declaring locales *) |
18 (* Declaring locales *) |
19 val add_locale: string -> bstring -> expression -> Element.context list -> theory -> |
19 val add_locale: string -> bstring -> expression -> Element.context list -> theory -> |
20 string * Proof.context |
20 string * Proof.context |
21 (* |
21 (* |
22 val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory -> |
22 val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory -> |
23 string * Proof.context |
23 string * Proof.context |
24 *) |
24 *) |
25 |
|
26 (* Debugging and development *) |
25 (* Debugging and development *) |
27 val parse_expression: OuterParse.token list -> expression * OuterParse.token list |
26 val parse_expression: OuterParse.token list -> expression * OuterParse.token list |
28 val debug_parameters: expression -> Proof.context -> Proof.context |
|
29 val debug_context: expression -> Proof.context -> Proof.context |
|
30 |
|
31 end; |
27 end; |
32 |
28 |
33 |
29 |
34 structure Expression: EXPRESSION = |
30 structure Expression: EXPRESSION = |
35 struct |
31 struct |
182 in (expr', (map (fn (b, mx) => (b, NONE, mx)) parms @ fixed)) end; |
177 in (expr', (map (fn (b, mx) => (b, NONE, mx)) parms @ fixed)) end; |
183 |
178 |
184 |
179 |
185 (** Read instantiation **) |
180 (** Read instantiation **) |
186 |
181 |
|
182 (* Parse positional or named instantiation *) |
|
183 |
187 local |
184 local |
188 |
185 |
189 fun prep_inst parse_term parms (prfx, insts) ctxt = |
186 fun prep_inst parse_term parms (Positional insts) ctxt = |
|
187 (insts ~~ parms) |> map (fn |
|
188 (NONE, p) => Syntax.parse_term ctxt p | |
|
189 (SOME t, _) => parse_term ctxt t) |
|
190 | prep_inst parse_term parms (Named insts) ctxt = |
|
191 parms |> map (fn p => case AList.lookup (op =) insts p of |
|
192 SOME t => parse_term ctxt t | |
|
193 NONE => Syntax.parse_term ctxt p); |
|
194 |
|
195 in |
|
196 |
|
197 fun parse_inst x = prep_inst Syntax.parse_term x; |
|
198 fun make_inst x = prep_inst (K I) x; |
|
199 |
|
200 end; |
|
201 |
|
202 (* Prepare type inference problem for Syntax.check_terms *) |
|
203 |
|
204 fun varify_indexT i ty = ty |> Term.map_atyps |
|
205 (fn TFree (a, S) => TVar ((a, i), S) |
|
206 | TVar (ai, _) => raise TYPE ("Illegal schematic variable: " ^ |
|
207 quote (Term.string_of_vname ai), [ty], [])); |
|
208 |
|
209 (* Instantiation morphism *) |
|
210 |
|
211 fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt = |
190 let |
212 let |
191 (* parameters *) |
213 (* parameters *) |
192 val (parm_names, parm_types) = split_list parms; |
|
193 val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; |
214 val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; |
194 |
|
195 (* parameter instantiations *) |
|
196 val insts' = case insts of |
|
197 Positional insts => (insts ~~ parm_names) |> map (fn |
|
198 (NONE, p) => parse_term ctxt p | |
|
199 (SOME t, _) => parse_term ctxt t) | |
|
200 Named insts => parm_names |> map (fn |
|
201 p => case AList.lookup (op =) insts p of |
|
202 SOME t => parse_term ctxt t | |
|
203 NONE => parse_term ctxt p); |
|
204 |
215 |
205 (* type inference and contexts *) |
216 (* type inference and contexts *) |
206 val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; |
217 val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; |
207 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); |
218 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); |
208 val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; |
219 val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; |
209 val res = Syntax.check_terms ctxt arg; |
220 val res = Syntax.check_terms ctxt arg; |
210 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
221 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
211 |
222 |
212 (* instantiation *) |
223 (* instantiation *) |
213 val (type_parms'', res') = chop (length type_parms) res; |
224 val (type_parms'', res') = chop (length type_parms) res; |
214 val insts'' = (parm_names ~~ res') |> map_filter |
225 val insts'' = (parm_names ~~ res') |> map_filter |
215 (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | |
226 (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | |
216 inst => SOME inst); |
227 inst => SOME inst); |
219 in |
230 in |
220 (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $> |
231 (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $> |
221 Morphism.name_morphism (Name.qualified prfx), ctxt') |
232 Morphism.name_morphism (Name.qualified prfx), ctxt') |
222 end; |
233 end; |
223 |
234 |
224 in |
|
225 |
|
226 fun read_inst x = prep_inst Syntax.parse_term x; |
|
227 (* fun cert_inst x = prep_inst (K I) x; *) |
|
228 |
|
229 end; |
|
230 |
|
231 |
|
232 (** Test code **) |
|
233 |
|
234 fun debug_parameters raw_expr ctxt = |
|
235 let |
|
236 val thy = ProofContext.theory_of ctxt; |
|
237 val expr = apfst (intern thy) raw_expr; |
|
238 val (expr', fixed) = parameters_of thy expr; |
|
239 in ctxt end; |
|
240 |
|
241 |
|
242 fun debug_context (raw_expr, fixed) ctxt = |
|
243 let |
|
244 val thy = ProofContext.theory_of ctxt; |
|
245 val expr = intern thy raw_expr; |
|
246 val (expr', fixed) = parameters_of thy (expr, fixed); |
|
247 |
|
248 fun declare_parameters fixed ctxt = |
|
249 let |
|
250 val (fixed', ctxt') = ProofContext.add_fixes fixed ctxt; |
|
251 in |
|
252 (fixed', ctxt') |
|
253 end; |
|
254 |
|
255 fun rough_inst loc prfx insts ctxt = |
|
256 let |
|
257 (* locale data *) |
|
258 val (parm_names, parm_types) = loc |> NewLocale.params_of thy |> |
|
259 map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list; |
|
260 |
|
261 (* type parameters *) |
|
262 val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; |
|
263 |
|
264 (* parameter instantiations *) |
|
265 val insts' = case insts of |
|
266 Positional insts => (insts ~~ parm_names) |> map (fn |
|
267 (NONE, p) => Syntax.parse_term ctxt p | |
|
268 (SOME t, _) => Syntax.parse_term ctxt t) | |
|
269 Named insts => parm_names |> map (fn |
|
270 p => case AList.lookup (op =) insts p of |
|
271 SOME t => Syntax.parse_term ctxt t | |
|
272 NONE => Syntax.parse_term ctxt p); |
|
273 |
|
274 (* type inference and contexts *) |
|
275 val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; |
|
276 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar); |
|
277 val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; |
|
278 val res = Syntax.check_terms ctxt arg; |
|
279 val ctxt' = ctxt |> fold Variable.auto_fixes res; |
|
280 |
|
281 (* instantiation *) |
|
282 val (type_parms'', res') = chop (length type_parms) res; |
|
283 val insts'' = (parm_names ~~ res') |> map_filter |
|
284 (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | |
|
285 inst => SOME inst); |
|
286 val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); |
|
287 val inst = Symtab.make insts''; |
|
288 in |
|
289 (Element.inst_morphism thy (instT, inst) $> |
|
290 Morphism.name_morphism (Name.qualified prfx), ctxt') |
|
291 end; |
|
292 |
|
293 fun add_declarations loc morph ctxt = |
|
294 let |
|
295 (* locale data *) |
|
296 val parms = loc |> NewLocale.params_of thy |> |
|
297 map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx)); |
|
298 val (typ_decls, term_decls) = NewLocale.declarations_of thy loc; |
|
299 |
|
300 (* declarations from locale *) |
|
301 val ctxt'' = ctxt |> |
|
302 fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls |> |
|
303 fold_rev (fn decl => Context.proof_map (decl morph)) term_decls; |
|
304 in |
|
305 ctxt'' |
|
306 end; |
|
307 |
|
308 val Expr [(loc1, (prfx1, insts1))] = expr'; |
|
309 val ctxt0 = ProofContext.init thy; |
|
310 val (parms, ctxt') = declare_parameters fixed ctxt0; |
|
311 val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt'; |
|
312 val ctxt'' = add_declarations loc1 morph1 ctxt'; |
|
313 in ctxt0 end; |
|
314 |
|
315 |
235 |
316 (*** Locale processing ***) |
236 (*** Locale processing ***) |
317 |
237 |
318 (** Parsing **) |
238 (** Parsing **) |
319 |
239 |
344 (asms ~~ propps) |> map (fn ((b, _), propp) => (b, propp)) |> Assumes |
264 (asms ~~ propps) |> map (fn ((b, _), propp) => (b, propp)) |> Assumes |
345 | restore_elem (Defines defs, propps) = |
265 | restore_elem (Defines defs, propps) = |
346 (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines |
266 (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines |
347 | restore_elem (Notes notes, _) = Notes notes; |
267 | restore_elem (Notes notes, _) = Notes notes; |
348 |
268 |
349 fun check_autofix_elems elems concl ctxt = |
269 fun check_autofix insts elems concl ctxt = |
350 let |
270 let |
351 val termss = elems |> map extract_elem; |
271 val instss = map (snd o snd) insts |> (map o map) (fn t => (t, [])); |
352 val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ flat termss); |
272 val elemss = elems |> map extract_elem; |
|
273 val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ instss @ flat elemss); |
353 (* val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *) |
274 (* val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *) |
354 val (concl', terms') = chop (length concl) all_terms'; |
275 val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) all_terms' ctxt; |
355 val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) terms' ctxt; |
276 val (concl', mores') = chop (length concl) all_terms'; |
356 in (terms' |> unflat termss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end; |
277 val (insts', elems') = chop (length instss) mores'; |
|
278 in (insts' |> (map o map) fst |> curry (op ~~) insts |> map (fn ((l, (p, _)), is) => (l, (p, is))), |
|
279 elems' |> unflat elemss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end; |
357 |
280 |
358 |
281 |
359 (** Prepare locale elements **) |
282 (** Prepare locale elements **) |
360 |
283 |
361 fun declare_elem prep_vars (Fixes fixes) ctxt = |
284 fun declare_elem prep_vars (Fixes fixes) ctxt = |
362 let val (vars, _) = prep_vars fixes ctxt |
285 let val (vars, _) = prep_vars fixes ctxt |
363 in ctxt |> ProofContext.add_fixes_i vars |> snd end |
286 in ctxt |> ProofContext.add_fixes_i vars |> snd end |
364 | declare_elem prep_vars (Constrains csts) ctxt = |
287 | declare_elem prep_vars (Constrains csts) ctxt = |
365 ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd |
288 ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd |
366 | declare_elem _ (Assumes asms) ctxt = ctxt |
289 | declare_elem _ (Assumes _) ctxt = ctxt |
367 | declare_elem _ (Defines defs) ctxt = ctxt |
290 | declare_elem _ (Defines _) ctxt = ctxt |
368 | declare_elem _ (Notes _) ctxt = ctxt; |
291 | declare_elem _ (Notes _) ctxt = ctxt; |
369 |
292 |
370 (** Finish locale elements, extract specification text **) |
293 (** Finish locale elements, extract specification text **) |
371 |
|
372 local |
|
373 |
294 |
374 val norm_term = Envir.beta_norm oo Term.subst_atomic; |
295 val norm_term = Envir.beta_norm oo Term.subst_atomic; |
375 |
296 |
376 fun abstract_thm thy eq = |
297 fun abstract_thm thy eq = |
377 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; |
298 Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def; |
388 exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso |
309 exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso |
389 err "Attempt to redefine variable"; |
310 err "Attempt to redefine variable"; |
390 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) |
311 (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) |
391 end; |
312 end; |
392 |
313 |
393 fun eval_text _ (Fixes _) text = text |
314 fun eval_text _ _ (Fixes _) text = text |
394 | eval_text _ (Constrains _) text = text |
315 | eval_text _ _ (Constrains _) text = text |
395 | eval_text _ (Assumes asms) |
316 | eval_text _ is_ext (Assumes asms) |
396 (((exts, exts'), (ints, ints')), (xs, env, defs)) = |
317 (((exts, exts'), (ints, ints')), (xs, env, defs)) = |
397 let |
318 let |
398 val ts = maps (map #1 o #2) asms; |
319 val ts = maps (map #1 o #2) asms; |
399 val ts' = map (norm_term env) ts; |
320 val ts' = map (norm_term env) ts; |
400 val spec' = ((exts @ ts, exts' @ ts'), (ints, ints')); |
321 val spec' = |
|
322 if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) |
|
323 else ((exts, exts'), (ints @ ts, ints' @ ts')); |
401 in (spec', (fold Term.add_frees ts' xs, env, defs)) end |
324 in (spec', (fold Term.add_frees ts' xs, env, defs)) end |
402 | eval_text ctxt (Defines defs) (spec, binds) = |
325 | eval_text ctxt _ (Defines defs) (spec, binds) = |
403 (spec, fold (bind_def ctxt o #1 o #2) defs binds) |
326 (spec, fold (bind_def ctxt o #1 o #2) defs binds) |
404 | eval_text _ (Notes _) text = text; |
327 | eval_text _ _ (Notes _) text = text; |
405 |
328 |
406 fun closeup _ _ false elem = elem |
329 fun closeup _ _ false elem = elem |
407 | closeup ctxt parms true elem = |
330 | closeup ctxt parms true elem = |
408 let |
331 let |
409 fun close_frees t = |
332 fun close_frees t = |
422 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => |
345 | Defines defs => Defines (defs |> map (fn (a, (t, ps)) => |
423 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) |
346 (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) |
424 | e => e) |
347 | e => e) |
425 end; |
348 end; |
426 |
349 |
427 fun finish_ext_elem parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) => |
350 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) => |
428 let val x = Name.name_of binding |
351 let val x = Name.name_of binding |
429 in (binding, AList.lookup (op =) parms x, mx) end) fixes) |
352 in (binding, AList.lookup (op =) parms x, mx) end) fixes) |
430 | finish_ext_elem _ _ (Constrains _) = Constrains [] |
353 | finish_primitive _ _ (Constrains _) = Constrains [] |
431 | finish_ext_elem _ close (Assumes asms) = close (Assumes asms) |
354 | finish_primitive _ close (Assumes asms) = close (Assumes asms) |
432 | finish_ext_elem _ close (Defines defs) = close (Defines defs) |
355 | finish_primitive _ close (Defines defs) = close (Defines defs) |
433 | finish_ext_elem _ _ (Notes facts) = Notes facts; |
356 | finish_primitive _ _ (Notes facts) = Notes facts; |
|
357 |
|
358 fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text = |
|
359 let |
|
360 val thy = ProofContext.theory_of ctxt; |
|
361 val (parm_names, parm_types) = NewLocale.params_of thy loc |> |
|
362 map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list; |
|
363 val (asm, defs) = NewLocale.specification_of thy loc; |
|
364 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt; |
|
365 val asm' = Option.map (Morphism.term morph) asm; |
|
366 val defs' = map (Morphism.term morph) defs; |
|
367 val text' = text |> |
|
368 (if is_some asm |
|
369 then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])]) |
|
370 else I) |> |
|
371 (if not (null defs) |
|
372 then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs')) |
|
373 else I) |
|
374 (* FIXME clone from new_locale.ML *) |
|
375 in ((loc, morph), text') end; |
434 |
376 |
435 fun finish_elem ctxt parms do_close elem text = |
377 fun finish_elem ctxt parms do_close elem text = |
436 let |
378 let |
437 val elem' = finish_ext_elem parms (closeup ctxt parms do_close) elem; |
379 val elem' = finish_primitive parms (closeup ctxt parms do_close) elem; |
438 val text' = eval_text ctxt elem' text; |
380 val text' = eval_text ctxt true elem' text; |
439 in (elem', text') end |
381 in (elem', text') end |
440 |
382 |
441 in |
383 fun finish ctxt parms do_close insts elems text = |
442 |
384 let |
443 fun finish_elems ctxt parms do_close elems text = |
385 val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text; |
444 fold_map (finish_elem ctxt parms do_close) elems text; |
386 val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text'; |
445 |
387 in (deps, elems', text'') end; |
446 end; |
|
447 |
388 |
448 |
389 |
449 local |
390 local |
450 |
391 |
451 (* nice, but for now not needed |
392 (* nice, but for now not needed |
453 | fold_suffixes f (x :: xs) y = f (x :: xs) (f xs y); |
394 | fold_suffixes f (x :: xs) y = f (x :: xs) (f xs y); |
454 |
395 |
455 fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y; |
396 fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y; |
456 *) |
397 *) |
457 |
398 |
458 fun prep_elems parse_typ parse_prop prep_vars do_close context raw_elems raw_concl = |
399 fun prep_elems parse_typ parse_prop parse_inst prep_vars |
459 let |
400 do_close context fixed raw_insts raw_elems raw_concl = |
460 fun prep_elem raw_elem (elems, ctxt) = |
401 let |
|
402 val thy = ProofContext.theory_of context; |
|
403 |
|
404 fun prep_inst (loc, (prfx, inst)) (i, ids, insts, ctxt) = |
|
405 let |
|
406 val (parm_names, parm_types) = NewLocale.params_of thy loc |> |
|
407 map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list; |
|
408 val inst' = parse_inst parm_names inst ctxt; |
|
409 val parm_types' = map (TypeInfer.paramify_vars o varify_indexT i) parm_types; |
|
410 val inst'' = map2 TypeInfer.constrain parm_types' inst'; |
|
411 val insts' = insts @ [(loc, (prfx, inst''))]; |
|
412 val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt; |
|
413 val inst''' = insts'' |> List.last |> snd |> snd; |
|
414 val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; |
|
415 val (ids', ctxt'') = NewLocale.activate_declarations loc morph thy ids ctxt; |
|
416 in (i+1, ids', insts', ctxt'') end; |
|
417 |
|
418 fun prep_elem raw_elem (insts, elems, ctxt) = |
461 let |
419 let |
462 val ctxt' = declare_elem prep_vars raw_elem ctxt; |
420 val ctxt' = declare_elem prep_vars raw_elem ctxt; |
463 val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; |
421 val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; |
464 (* FIXME term bindings *) |
422 (* FIXME term bindings *) |
465 val (_, _, ctxt'') = check_autofix_elems elems' [] ctxt'; |
423 val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt'; |
466 in (elems', ctxt'') end; |
424 in (insts, elems', ctxt') end; |
467 |
425 |
468 fun prep_concl raw_concl (elems, ctxt) = |
426 fun prep_concl raw_concl (insts, elems, ctxt) = |
469 let |
427 let |
470 val concl = (map o map) (fn (t, ps) => |
428 val concl = (map o map) (fn (t, ps) => |
471 (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl; |
429 (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl; |
472 in check_autofix_elems elems concl ctxt end; |
430 in check_autofix insts elems concl ctxt end; |
473 |
431 |
474 val (elems, concl, ctxt) = fold prep_elem raw_elems ([], context) |> |
432 val fors = prep_vars fixed context |> fst; |
475 prep_concl raw_concl; |
433 val ctxt = context |> ProofContext.add_fixes_i fors |> snd; |
476 |
434 val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt); |
477 (* Retrieve parameter types *) |
435 val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt'); |
|
436 val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt''); |
|
437 |
|
438 (* Retrieve parameter types *) |
478 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) | |
439 val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) | |
479 _ => fn ps => ps) elems []; |
440 _ => fn ps => ps) (Fixes fors :: elems) []; |
480 val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; |
441 val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; |
481 val parms = xs ~~ Ts; |
442 val parms = xs ~~ Ts; |
482 |
443 |
483 val (elems', text) = finish_elems ctxt' parms do_close elems ((([], []), ([], [])), ([], [], [])); |
444 val Fixes fors' = finish_primitive parms I (Fixes fors); |
|
445 val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], [])); |
484 (* text has the following structure: |
446 (* text has the following structure: |
485 (((exts, exts'), (ints, ints')), (xs, env, defs)) |
447 (((exts, exts'), (ints, ints')), (xs, env, defs)) |
486 where |
448 where |
487 exts: external assumptions (terms in external assumes elements) |
449 exts: external assumptions (terms in assumes elements) |
488 exts': dito, normalised wrt. env |
450 exts': dito, normalised wrt. env |
489 ints: internal assumptions (terms in internal assumes elements) |
451 ints: internal assumptions (terms in assumptions from insts) |
490 ints': dito, normalised wrt. env |
452 ints': dito, normalised wrt. env |
491 xs: the free variables in exts' and ints' and rhss of definitions, |
453 xs: the free variables in exts' and ints' and rhss of definitions, |
492 this includes parameters except defined parameters |
454 this includes parameters except defined parameters |
493 env: list of term pairs encoding substitutions, where the first term |
455 env: list of term pairs encoding substitutions, where the first term |
494 is a free variable; substitutions represent defines elements and |
456 is a free variable; substitutions represent defines elements and |
519 fun prep_context_statement prep_expr prep_elems |
483 fun prep_context_statement prep_expr prep_elems |
520 do_close imprt elements raw_concl context = |
484 do_close imprt elements raw_concl context = |
521 let |
485 let |
522 val thy = ProofContext.theory_of context; |
486 val thy = ProofContext.theory_of context; |
523 |
487 |
524 val (expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt); |
488 val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt); |
525 val ctxt = context |> ProofContext.add_fixes fixed |> snd; |
489 val ctxt = context |> ProofContext.add_fixes fixed |> snd; |
|
490 (* FIXME push inside prep_elems *) |
|
491 val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) = |
|
492 prep_elems do_close context fixed expr elements raw_concl; |
|
493 (* FIXME activate deps *) |
|
494 val ((elems', _), ctxt') = |
|
495 Element.activate elems (ProofContext.set_stmt true ctxt); |
526 in |
496 in |
527 case expr of |
497 (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl) |
528 Expr [] => let |
498 end |
529 val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close |
|
530 context elements raw_concl; |
|
531 val ((elems', _), ctxt') = |
|
532 Element.activate elems (ProofContext.set_stmt true ctxt); |
|
533 in |
|
534 (((ctxt', elems'), (parms, spec, defs)), concl) |
|
535 end |
|
536 (* |
|
537 | Expr [(name, insts)] => let |
|
538 val parms = parameters_of thy name |> map (fn (b, SOME T, _) => (Name.name_of b, T)); |
|
539 val (morph, ctxt') = read_inst parms insts context; |
|
540 in |
|
541 |
|
542 end |
|
543 *) |
|
544 end |
|
545 |
499 |
546 in |
500 in |
547 |
501 |
548 fun read_context imprt body ctxt = |
502 fun read_context imprt body ctxt = |
549 #1 (prep_context_statement intern read_elems true imprt body [] ctxt); |
503 #1 (prep_context_statement intern read_elems true imprt body [] ctxt); |
|
504 (* |
550 fun cert_context imprt body ctxt = |
505 fun cert_context imprt body ctxt = |
551 #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt); |
506 #1 (prep_context_statement (K I) cert_elems true imprt body [] ctxt); |
552 |
507 *) |
553 end; |
508 end; |
554 |
509 |
555 |
510 |
556 (** Dependencies **) |
511 (** Dependencies **) |
557 |
512 |
698 in |
653 in |
699 (Notes (Thm.definitionK, notes), defns @ defs') |
654 (Notes (Thm.definitionK, notes), defns @ defs') |
700 end |
655 end |
701 | defines_to_notes _ e defns = (e, defns); |
656 | defines_to_notes _ e defns = (e, defns); |
702 |
657 |
703 fun gen_add_locale prep_ctxt |
658 fun gen_add_locale prep_context |
704 bname predicate_name raw_imprt raw_body thy = |
659 bname predicate_name raw_imprt raw_body thy = |
705 let |
660 let |
706 val thy_ctxt = ProofContext.init thy; |
661 val thy_ctxt = ProofContext.init thy; |
707 val name = Sign.full_name thy bname; |
662 val name = Sign.full_name thy bname; |
708 val _ = NewLocale.test_locale thy name andalso |
663 val _ = NewLocale.test_locale thy name andalso |
709 error ("Duplicate definition of locale " ^ quote name); |
664 error ("Duplicate definition of locale " ^ quote name); |
710 |
665 |
711 val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) = |
666 val ((fors, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) = |
712 prep_ctxt raw_imprt raw_body thy_ctxt; |
667 prep_context raw_imprt raw_body thy_ctxt; |
713 val ((statement, intro, axioms), _, thy') = |
668 val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = |
714 define_preds predicate_name text thy; |
669 define_preds predicate_name text thy; |
715 |
670 |
716 val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; |
671 val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; |
717 val _ = if null extraTs then () |
672 val _ = if null extraTs then () |
718 else warning ("Additional type variable(s) in locale specification " ^ quote bname); |
673 else warning ("Additional type variable(s) in locale specification " ^ quote bname); |
719 |
674 |
720 val params = body_elems |> |
675 val satisfy = Element.satisfy_morphism b_axioms; |
721 map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat; |
676 val params = fors @ |
722 |
677 (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat); |
723 val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems []; |
678 val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems []; |
724 |
679 |
725 val notes = body_elems' |> |
680 val notes = body_elems' |> |
726 (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) |> |
681 (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |> |
727 fst |> |
682 fst |> map (Element.morph_ctxt satisfy) |> |
728 map_filter (fn Notes notes => SOME notes | _ => NONE); |
683 map_filter (fn Notes notes => SOME notes | _ => NONE); |
729 |
684 |
|
685 val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps; |
|
686 |
730 val loc_ctxt = thy' |> |
687 val loc_ctxt = thy' |> |
731 NewLocale.register_locale name (extraTs, params) (statement, defns) ([], []) |
688 NewLocale.register_locale name (extraTs, params) |
732 (map (fn n => (n, stamp ())) notes |> rev) [] |> |
689 (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], []) |
|
690 (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |> |
733 NewLocale.init name |
691 NewLocale.init name |
734 in (name, loc_ctxt) end; |
692 in (name, loc_ctxt) end; |
735 |
693 |
736 in |
694 in |
737 |
695 |