124 |
133 |
125 (* diagnostics *) |
134 (* diagnostics *) |
126 |
135 |
127 fun err_in_locale ctxt msg ids = |
136 fun err_in_locale ctxt msg ids = |
128 let |
137 let |
129 fun prt_id (name, parms) = [Pretty.block (Pretty.breaks (map Pretty.str (name :: parms)))]; |
138 val sign = ProofContext.sign_of ctxt; |
|
139 fun prt_id (name, parms) = |
|
140 [Pretty.block (Pretty.breaks (map Pretty.str (cond_extern sign name :: parms)))]; |
130 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
141 val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); |
131 val err_msg = |
142 val err_msg = |
132 if null ids then msg |
143 if forall (equal "" o #1) ids then msg |
133 else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
144 else msg ^ "\n" ^ Pretty.string_of (Pretty.block |
134 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
145 (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids)); |
135 in raise ProofContext.CONTEXT (err_msg, ctxt) end; |
146 in raise ProofContext.CONTEXT (err_msg, ctxt) end; |
136 |
147 |
137 |
148 |
138 |
149 |
139 (** operations on locale elements **) |
150 (** primitives **) |
140 |
|
141 (* misc utilities *) |
|
142 |
|
143 fun frozen_tvars ctxt Ts = |
|
144 let |
|
145 val tvars = rev (foldl Term.add_tvarsT ([], Ts)); |
|
146 val tfrees = map TFree |
|
147 (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars); |
|
148 in map #1 tvars ~~ tfrees end; |
|
149 |
|
150 fun fixes_of_elemss elemss = flat (map (snd o fst) elemss); |
|
151 |
|
152 |
|
153 (* prepare elements *) |
|
154 |
|
155 datatype fact = Int of thm list | Ext of string; |
|
156 |
|
157 local |
|
158 |
|
159 fun prep_name ctxt (name, atts) = |
|
160 if NameSpace.is_qualified name then |
|
161 raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) |
|
162 else (name, atts); |
|
163 |
|
164 fun prep_elem prep_vars prep_propp prep_thms ctxt = |
|
165 fn Fixes fixes => |
|
166 let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) |
|
167 in Fixes (map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes)) end |
|
168 | Assumes asms => |
|
169 Assumes (map (prep_name ctxt o #1) asms ~~ snd (prep_propp (ctxt, map #2 asms))) |
|
170 | Defines defs => |
|
171 let val propps = snd (prep_propp (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)) in |
|
172 Defines (map (prep_name ctxt o #1) defs ~~ map (fn [(t', (ps', []))] => (t', ps')) propps) |
|
173 end |
|
174 | Notes facts => |
|
175 Notes (map (fn (a, bs) => (prep_name ctxt a, map (apfst (prep_thms ctxt)) bs)) facts); |
|
176 |
|
177 in |
|
178 |
|
179 fun read_elem x = prep_elem ProofContext.read_vars ProofContext.read_propp (K I) x; |
|
180 fun cert_elem x = prep_elem ProofContext.cert_vars ProofContext.cert_propp (K I) x; |
|
181 fun int_facts x = prep_elem I I (K Int) x; |
|
182 fun ext_facts x = prep_elem I I (K Ext) x; |
|
183 fun get_facts x = prep_elem I I |
|
184 (fn ctxt => (fn Int ths => ths | Ext name => ProofContext.get_thms ctxt name)) x; |
|
185 |
|
186 fun read_expr ctxt (Locale xname) = Locale (intern (ProofContext.sign_of ctxt) xname) |
|
187 | read_expr ctxt (Merge exprs) = Merge (map (read_expr ctxt) exprs) |
|
188 | read_expr ctxt (Rename (expr, xs)) = Rename (read_expr ctxt expr, xs); |
|
189 |
|
190 end; |
|
191 |
|
192 |
|
193 (* internalize attributes *) |
|
194 |
|
195 local fun read_att attrib (x, srcs) = (x, map attrib srcs) in |
|
196 |
|
197 fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) |
|
198 | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) |
|
199 | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) |
|
200 | attribute attrib (Elem (Notes facts)) = |
|
201 Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) |
|
202 | attribute _ (Expr expr) = Expr expr; |
|
203 |
|
204 end; |
|
205 |
|
206 |
151 |
207 (* renaming *) |
152 (* renaming *) |
208 |
153 |
209 fun rename ren x = if_none (assoc_string (ren, x)) x; |
154 fun rename ren x = if_none (assoc_string (ren, x)) x; |
210 |
155 |
288 | inst_elem env (Defines defs) = Defines (map (apsnd (fn (t, ps) => |
236 | inst_elem env (Defines defs) = Defines (map (apsnd (fn (t, ps) => |
289 (inst_term env t, map (inst_term env) ps))) defs) |
237 (inst_term env t, map (inst_term env) ps))) defs) |
290 | inst_elem env (Notes facts) = Notes (map (apsnd (map (apfst (map (inst_thm env))))) facts); |
238 | inst_elem env (Notes facts) = Notes (map (apsnd (map (apfst (map (inst_thm env))))) facts); |
291 |
239 |
292 |
240 |
293 (* evaluation *) |
241 |
|
242 (** structured contexts: rename + merge + implicit type instantiation **) |
|
243 |
|
244 (* parameter types *) |
|
245 |
|
246 fun frozen_tvars ctxt Ts = |
|
247 let |
|
248 val tvars = rev (foldl Term.add_tvarsT ([], Ts)); |
|
249 val tfrees = map TFree |
|
250 (Term.invent_type_names (ProofContext.used_types ctxt) (length tvars) ~~ map #2 tvars); |
|
251 in map #1 tvars ~~ tfrees end; |
|
252 |
|
253 |
|
254 fun unify_frozen ctxt maxidx Ts Us = |
|
255 let |
|
256 val FIXME = (PolyML.print "unify_frozen 1"; PolyML.print (Ts, Us)); |
|
257 val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); |
|
258 fun unify (env, (Some T, Some U)) = Type.unify tsig env (U, T) |
|
259 | unify (env, _) = env; |
|
260 fun paramify (i, None) = (i, None) |
|
261 | paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T)); |
|
262 |
|
263 val (maxidx', Ts') = foldl_map paramify (maxidx, Ts); |
|
264 val (maxidx'', Us') = foldl_map paramify (maxidx, Us); |
|
265 val FIXME = (PolyML.print "unify_frozen 2"; PolyML.print (Ts', Us')); |
|
266 val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us'); |
|
267 val Vs = map (apsome (Envir.norm_type unifier)) Us'; |
|
268 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs)); |
|
269 val Vs' = map (apsome (Envir.norm_type unifier')) Vs; |
|
270 val FIXME = (PolyML.print "unify_frozen 3"; PolyML.print Vs'); |
|
271 in Vs' end; |
|
272 |
|
273 |
|
274 fun params_of elemss = flat (map (snd o fst) elemss); |
|
275 fun param_types ps = mapfilter (fn (_, None) => None | (x, Some T) => Some (x, T)) ps; |
|
276 |
|
277 |
|
278 (* flatten expressions *) |
294 |
279 |
295 local |
280 local |
296 |
|
297 fun unify_parms ctxt raw_parmss = |
|
298 let |
|
299 val tsig = Sign.tsig_of (ProofContext.sign_of ctxt); |
|
300 val maxidx = length raw_parmss; |
|
301 val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss; |
|
302 |
|
303 fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); |
|
304 fun varify_parms (i, ps) = |
|
305 mapfilter (fn (_, None) => None | (x, Some T) => Some (x, varify i T)) ps; |
|
306 val parms = flat (map varify_parms idx_parmss); |
|
307 |
|
308 fun unify T ((env, maxidx), U) = Type.unify tsig maxidx env (U, T); (*should never fail*) |
|
309 fun unify_list (envir, T :: Us) = foldl (unify T) (envir, Us) |
|
310 | unify_list (envir, []) = envir; |
|
311 val (unifier, _) = foldl unify_list |
|
312 ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms))); |
|
313 |
|
314 val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms); |
|
315 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); |
|
316 |
|
317 fun inst_parms (i, ps) = |
|
318 foldr Term.add_typ_tfrees (mapfilter snd ps, []) |
|
319 |> mapfilter (fn (a, S) => |
|
320 let val T = Envir.norm_type unifier' (TVar ((a, i), S)) |
|
321 in if T = TFree (a, S) then None else Some ((a, S), T) end); |
|
322 in map inst_parms idx_parmss end; |
|
323 |
281 |
324 fun unique_parms ctxt elemss = |
282 fun unique_parms ctxt elemss = |
325 let |
283 let |
326 val param_decls = |
284 val param_decls = |
327 flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss) |
285 flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss) |
384 val ren = filter_out (op =) (map #1 ps ~~ xs); |
370 val ren = filter_out (op =) (map #1 ps ~~ xs); |
385 val (params', elems') = |
371 val (params', elems') = |
386 if null ren then ((ps, qs), map #1 elems) |
372 if null ren then ((ps, qs), map #1 elems) |
387 else ((map (apfst (rename ren)) ps, map (rename ren) qs), |
373 else ((map (apfst (rename ren)) ps, map (rename ren) qs), |
388 map (rename_elem ren o #1) elems); |
374 map (rename_elem ren o #1) elems); |
389 val elems'' = map (qualify_elem [NameSpace.base name, space_implode "_" xs]) elems'; |
375 val elems'' = map (rename_facts [NameSpace.base name, space_implode "_" xs]) elems'; |
390 in ((name, params'), elems'') end; |
376 in ((name, params'), elems'') end; |
391 |
377 |
392 val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr)))); |
378 val raw_elemss = unique_parms ctxt (map eval (#1 (identify (([], []), expr)))); |
393 val elemss = inst_types ctxt raw_elemss; |
379 val elemss = unify_elemss ctxt [] raw_elemss; |
394 in elemss end; |
380 in elemss end; |
395 |
381 |
396 end; |
382 end; |
397 |
383 |
398 |
384 |
399 |
385 (* activate elements *) |
400 (** activation **) |
386 |
401 |
387 fun declare_fixes (s: string) fixes = (PolyML.print s; PolyML.print fixes; |
402 (* internalize elems *) |
388 ProofContext.add_syntax fixes o |
|
389 ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes)); |
403 |
390 |
404 local |
391 local |
405 |
392 |
406 fun perform_elems f named_elems = ProofContext.qualified (fn context => |
393 fun activate_elem (Fixes fixes) = declare_fixes "activate_elem" fixes |
407 foldl (fn (ctxt, ((name, ps), es)) => |
|
408 foldl (fn (c, e) => f e c) (ctxt, es) handle ProofContext.CONTEXT (msg, ctxt) => |
|
409 err_in_locale ctxt msg [(name, map fst ps)]) (context, named_elems)); |
|
410 |
|
411 in |
|
412 |
|
413 fun declare_elem gen = |
|
414 let |
|
415 val gen_typ = if gen then Term.map_type_tfree (Type.param []) else I; |
|
416 val gen_term = if gen then Term.map_term_types gen_typ else I; |
|
417 |
|
418 fun declare (Fixes fixes) = ProofContext.add_syntax fixes o |
|
419 ProofContext.fix_direct (map (fn (x, T, _) => ([x], apsome gen_typ T)) fixes) |
|
420 | declare (Assumes asms) = (fn ctxt => #1 (ProofContext.bind_propp_i |
|
421 (ctxt, map (map (fn (t, (ps, ps')) => |
|
422 (gen_term t, (map gen_term ps, map gen_term ps'))) o #2) asms))) |
|
423 | declare (Defines defs) = (fn ctxt => #1 (ProofContext.bind_propp_i |
|
424 (ctxt, map (fn (_, (t, ps)) => [(gen_term t, (map gen_term ps, []))]) defs))) |
|
425 | declare (Notes _) = I; |
|
426 in declare end; |
|
427 |
|
428 fun activate_elem (Fixes fixes) = ProofContext.add_syntax fixes o |
|
429 ProofContext.fix_direct (map (fn (x, T, _) => ([x], T)) fixes) |
|
430 | activate_elem (Assumes asms) = |
394 | activate_elem (Assumes asms) = |
431 #1 o ProofContext.assume_i ProofContext.export_assume asms o |
395 #1 o ProofContext.assume_i ProofContext.export_assume asms o |
432 ProofContext.fix_frees (flat (map (map #1 o #2) asms)) |
396 ProofContext.fix_frees (flat (map (map #1 o #2) asms)) |
433 | activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def |
397 | activate_elem (Defines defs) = (fn ctxt => #1 (ProofContext.assume_i ProofContext.export_def |
434 (map (fn ((name, atts), (t, ps)) => |
398 (map (fn ((name, atts), (t, ps)) => |
435 let val (c, t') = ProofContext.cert_def ctxt t |
399 let val (c, t') = ProofContext.cert_def ctxt t |
436 in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt)) |
400 in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt)) |
437 | activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts; |
401 | activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts; |
438 |
402 |
439 fun declare_elemss gen = perform_elems (declare_elem gen); |
403 in |
440 fun activate_elemss x = perform_elems activate_elem x; |
404 |
441 |
405 fun activate_elems ((name, ps), elems) = ProofContext.qualified (fn ctxt => |
442 end; |
406 foldl (fn (c, e) => activate_elem e c) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) => |
443 |
407 err_in_locale ctxt msg [(name, map fst ps)]); |
444 |
408 |
445 (* context specifications: import expression + external elements *) |
409 end; |
|
410 |
|
411 |
|
412 |
|
413 (** prepare context elements **) |
|
414 |
|
415 (* expressions *) |
|
416 |
|
417 fun intern_expr sg (Locale xname) = Locale (intern sg xname) |
|
418 | intern_expr sg (Merge exprs) = Merge (map (intern_expr sg) exprs) |
|
419 | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs); |
|
420 |
|
421 |
|
422 (* parameters *) |
446 |
423 |
447 local |
424 local |
|
425 |
|
426 fun prep_fixes prep_vars ctxt fixes = |
|
427 let val vars = snd (foldl_map prep_vars (ctxt, map (fn (x, T, _) => ([x], T)) fixes)) |
|
428 in map (fn (([x'], T'), (_, _, mx)) => (x', T', mx)) (vars ~~ fixes) end; |
|
429 |
|
430 in |
|
431 |
|
432 fun read_fixes x = prep_fixes ProofContext.read_vars x; |
|
433 fun cert_fixes x = prep_fixes ProofContext.cert_vars x; |
|
434 |
|
435 end; |
|
436 |
|
437 |
|
438 (* propositions and bindings *) |
|
439 |
|
440 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b; |
|
441 |
|
442 local |
|
443 |
|
444 fun declare_int_elem i (ctxt, Fixes fixes) = |
|
445 (ctxt |> declare_fixes "declare_int_elem" (map (fn (x, T, mx) => |
|
446 (x, apsome (Term.map_type_tfree (Type.param i)) T, mx)) fixes), []) |
|
447 | declare_int_elem _ (ctxt, _) = (ctxt, []); |
|
448 |
|
449 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) = |
|
450 (ctxt |> declare_fixes "declare_ext_elem" (prep_fixes ctxt fixes), []) |
|
451 | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms) |
|
452 | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs) |
|
453 | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []); |
|
454 |
|
455 fun declare_elems prep_fixes ((ctxt, i), ((name, ps), elems)) = |
|
456 let val (ctxt', propps) = |
|
457 (case elems of |
|
458 Int es => foldl_map (declare_int_elem i) (ctxt, es) |
|
459 | Ext es => foldl_map (declare_ext_elem prep_fixes) (ctxt, es)) |
|
460 handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] |
|
461 in ((ctxt', i + 1), propps) end; |
|
462 |
448 |
463 |
449 fun close_frees ctxt t = |
464 fun close_frees ctxt t = |
450 let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t))) |
465 let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1) (Term.add_frees ([], t))) |
451 in Term.list_all_free (frees, t) end; |
466 in Term.list_all_free (frees, t) end; |
452 |
467 |
453 (*quantify dangling frees, strip term bindings*) |
|
454 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) => |
468 fun closeup ctxt (Assumes asms) = Assumes (asms |> map (fn (a, propps) => |
455 (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps))) |
469 (a, map (fn (t, _) => (close_frees ctxt t, ([], []))) propps))) |
456 | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) => |
470 | closeup ctxt (Defines defs) = Defines (defs |> map (fn (a, (t, _)) => |
457 (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), [])))) |
471 (a, (close_frees ctxt (#2 (ProofContext.cert_def ctxt t)), [])))) |
458 | closeup ctxt elem = elem; |
472 | closeup ctxt elem = elem; |
459 |
473 |
460 fun fixes_of_elem (Fixes fixes) = map (fn (x, T, _) => (x, T)) fixes |
474 fun finish_elem parms _ (Fixes fixes, _) = Ext (Fixes (map (fn (x, _, mx) => |
461 | fixes_of_elem _ = []; |
475 (x, assoc_string (parms, x), mx)) fixes)) |
462 |
476 | finish_elem _ close (Assumes asms, propp) = Ext (close (Assumes (map #1 asms ~~ propp))) |
463 fun prepare_context prep_expr prep_elem1 prep_elem2 close (import, elements) context = |
477 | finish_elem _ close (Defines defs, propp) = |
464 let |
478 Ext (close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))) |
465 fun declare_expr (c, raw_expr) = |
479 | finish_elem _ _ (Notes facts, _) = Ext (Notes facts); |
|
480 |
|
481 fun finish_elems ctxt parms close (((name, ps), elems), propps) = |
|
482 let |
|
483 val elems' = |
|
484 (case elems of |
|
485 Int es => map Int (#2 (hd (unify_elemss ctxt parms [((name, ps), es)]))) |
|
486 | Ext es => map2 (finish_elem parms close) (es, propps)); |
|
487 val ps' = map (fn (x, _) => (x, assoc (parms, x))) ps; |
|
488 in ((name, ps'), elems') end; |
|
489 |
|
490 |
|
491 fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = |
|
492 let |
|
493 val ((raw_ctxt, maxidx), raw_proppss) = |
|
494 foldl_map (declare_elems prep_fixes) ((context, 0), raw_elemss); |
|
495 val raw_propps = map flat raw_proppss; |
|
496 val raw_propp = flat raw_propps; |
|
497 val (ctxt, all_propp) = |
|
498 prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); |
|
499 val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt; |
|
500 |
|
501 val all_propp' = map2 (op ~~) |
|
502 (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); |
|
503 val n = length raw_concl; |
|
504 val concl = take (n, all_propp'); |
|
505 val propp = drop (n, all_propp'); |
|
506 val propps = unflat raw_propps propp; |
|
507 val proppss = map2 (uncurry unflat) (raw_proppss, propps); |
|
508 |
|
509 val xs = map #1 (params_of raw_elemss); |
|
510 val typing = unify_frozen ctxt maxidx |
|
511 (map (ProofContext.default_type raw_ctxt) xs) |
|
512 (map (ProofContext.default_type ctxt) xs); |
|
513 val parms = param_types (xs ~~ typing); |
|
514 |
|
515 val close = if do_close then closeup ctxt else I; |
|
516 val elemss = map2 (finish_elems ctxt parms close) (raw_elemss, proppss); |
|
517 in (parms, elemss, concl) end; |
|
518 |
|
519 in |
|
520 |
|
521 fun read_elemss x = prep_elemss read_fixes ProofContext.read_propp_schematic x; |
|
522 fun cert_elemss x = prep_elemss cert_fixes ProofContext.cert_propp_schematic x; |
|
523 |
|
524 end; |
|
525 |
|
526 |
|
527 (* facts *) |
|
528 |
|
529 local |
|
530 |
|
531 fun prep_name ctxt (name, atts) = |
|
532 if NameSpace.is_qualified name then |
|
533 raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt) |
|
534 else (name, atts); |
|
535 |
|
536 fun prep_facts _ _ (Int elem) = elem |
|
537 | prep_facts _ _ (Ext (Fixes fixes)) = Fixes fixes |
|
538 | prep_facts _ ctxt (Ext (Assumes asms)) = Assumes (map (apfst (prep_name ctxt)) asms) |
|
539 | prep_facts _ ctxt (Ext (Defines defs)) = Defines (map (apfst (prep_name ctxt)) defs) |
|
540 | prep_facts get ctxt (Ext (Notes facts)) = Notes (facts |> map (fn (a, bs) => |
|
541 (prep_name ctxt a, map (apfst (get ctxt)) bs))); |
|
542 |
|
543 in |
|
544 |
|
545 fun get_facts x = prep_facts ProofContext.get_thms x; |
|
546 fun get_facts_i x = prep_facts (K I) x; |
|
547 |
|
548 end; |
|
549 |
|
550 |
|
551 (* attributes *) |
|
552 |
|
553 local fun read_att attrib (x, srcs) = (x, map attrib srcs) in |
|
554 |
|
555 fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) |
|
556 | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) |
|
557 | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) |
|
558 | attribute attrib (Elem (Notes facts)) = |
|
559 Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) |
|
560 | attribute _ (Expr expr) = Expr expr; |
|
561 |
|
562 end; |
|
563 |
|
564 |
|
565 |
|
566 (** prepare context statements: import + elements + conclusion **) |
|
567 |
|
568 local |
|
569 |
|
570 fun prep_context_statement prep_expr prep_elemss prep_facts |
|
571 close fixed_params import elements raw_concl context = |
|
572 let |
|
573 val sign = ProofContext.sign_of context; |
|
574 fun flatten (Elem (Fixes fixes)) = [(("", map (rpair None o #1) fixes), Ext [Fixes fixes])] |
|
575 | flatten (Elem elem) = [(("", []), Ext [elem])] |
|
576 | flatten (Expr expr) = map (apsnd Int) (flatten_expr context (prep_expr sign expr)); |
|
577 |
|
578 val raw_import_elemss = flatten (Expr import); |
|
579 val raw_elemss = flat (map flatten elements); |
|
580 val (parms, all_elemss, concl) = |
|
581 prep_elemss close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; |
|
582 |
|
583 fun activate_facts (ctxt, ((name, ps), raw_elems)) = |
466 let |
584 let |
467 val expr = prep_expr c raw_expr; |
585 val elems = map (prep_facts ctxt) raw_elems; |
468 val named_elemss = eval_expr c expr; |
|
469 in (c |> declare_elemss true named_elemss, named_elemss) end; |
|
470 |
|
471 fun declare_element (c, Elem raw_elem) = |
|
472 let |
|
473 val elem = (if close then closeup c else I) (prep_elem2 c (prep_elem1 c raw_elem)); |
|
474 val res = [(("", fixes_of_elem elem), [elem])]; |
|
475 in (c |> declare_elemss false res, res) end |
|
476 | declare_element (c, Expr raw_expr) = |
|
477 apsnd (map (apsnd (map (int_facts c)))) (declare_expr (c, raw_expr)); |
|
478 |
|
479 fun activate_elems (c, ((name, ps), raw_elems)) = |
|
480 let |
|
481 val elems = map (get_facts c) raw_elems; |
|
482 val res = ((name, ps), elems); |
586 val res = ((name, ps), elems); |
483 in (c |> activate_elemss [res], res) end; |
587 in (ctxt |> activate_elems res, res) end; |
484 |
588 |
485 val (import_ctxt, import_elemss) = declare_expr (context, import); |
589 val n = length raw_import_elemss; |
486 val (ctxt, elemss) = apsnd flat (foldl_map declare_element (import_ctxt, elements)); |
590 val (import_ctxt, import_elemss) = foldl_map activate_facts (context, take (n, all_elemss)); |
487 val type_env = frozen_tvars ctxt (mapfilter (ProofContext.default_type ctxt o #1) |
591 val (ctxt, elemss) = foldl_map activate_facts (import_ctxt, drop (n, all_elemss)); |
488 (fixes_of_elemss import_elemss @ fixes_of_elemss elemss)); |
592 in (((import_ctxt, import_elemss), (ctxt, elemss)), concl) end; |
489 |
593 |
490 fun inst_elems ((name, ps), elems) = ((name, ps), elems); (* FIXME *) |
594 val gen_context = prep_context_statement intern_expr read_elemss get_facts; |
491 |
595 val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i; |
492 val import_elemss' = map inst_elems import_elemss; |
596 |
493 val import_ctxt' = context |> activate_elemss import_elemss'; |
597 fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt = |
494 val (ctxt', elemss') = foldl_map activate_elems (import_ctxt', map inst_elems elemss); |
598 let |
495 in ((import_ctxt', import_elemss'), (ctxt', elemss')) end; |
599 val thy = ProofContext.theory_of ctxt; |
496 |
600 val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; |
497 val prep_context = prepare_context read_expr read_elem ext_facts; |
601 val (fixed_params, import) = |
498 val prep_context_i = prepare_context (K I) cert_elem int_facts; |
602 (case locale of None => ([], empty) |
|
603 | Some name => (param_types (#1 (#params (the_locale thy name))), Locale name)); |
|
604 val (((locale_ctxt, _), (elems_ctxt, _)), concl') = |
|
605 prep_ctxt false fixed_params import elems concl ctxt; |
|
606 in (locale, locale_ctxt, elems_ctxt, concl') end; |
499 |
607 |
500 in |
608 in |
501 |
609 |
502 val read_context = prep_context true; |
610 fun read_context x y z = #1 (gen_context true [] x y [] z); |
503 val cert_context = prep_context_i true; |
611 fun cert_context x y z = #1 (gen_context_i true [] x y [] z); |
504 val activate_context = pairself fst oo prep_context false; |
612 val read_context_statement = gen_statement intern gen_context; |
505 val activate_context_i = pairself fst oo prep_context_i false; |
613 val cert_context_statement = gen_statement (K I) gen_context_i; |
506 fun activate_locale name = #1 o activate_context_i (Locale name, []); |
|
507 |
614 |
508 end; |
615 end; |
509 |
616 |
510 |
617 |
511 |
618 |