52 funs: (string list * string) tab, |
52 funs: (string list * string) tab, |
53 ids: (term * string) Symtab.table * Name.context, |
53 ids: (term * string) Symtab.table * Name.context, |
54 proving: bool, |
54 proving: bool, |
55 vcs: (string * thm list option * |
55 vcs: (string * thm list option * |
56 (string * expr) list * (string * expr) list) VCtab.table, |
56 (string * expr) list * (string * expr) list) VCtab.table, |
57 path: Path.T} option} |
57 path: Path.T, |
|
58 prefix: string} option} |
58 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} |
59 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} |
59 val extend = I |
60 val extend = I |
60 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, |
61 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, |
61 {pfuns = pfuns2, type_map = type_map2, env = NONE}) = |
62 {pfuns = pfuns2, type_map = type_map2, env = NONE}) = |
62 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), |
63 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), |
70 |
71 |
71 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; |
72 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; |
72 |
73 |
73 val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); |
74 val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); |
74 |
75 |
|
76 fun lookup_prfx "" tab s = Symtab.lookup tab s |
|
77 | lookup_prfx prfx tab s = (case Symtab.lookup tab s of |
|
78 NONE => Symtab.lookup tab (prfx ^ "__" ^ s) |
|
79 | x => x); |
|
80 |
|
81 fun strip_prfx s = |
|
82 let |
|
83 fun strip ys [] = ("", implode ys) |
|
84 | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys) |
|
85 | strip ys (x :: xs) = strip (x :: ys) xs |
|
86 in strip [] (rev (raw_explode s)) end; |
|
87 |
75 fun mk_unop s t = |
88 fun mk_unop s t = |
76 let val T = fastype_of t |
89 let val T = fastype_of t |
77 in Const (s, T --> T) $ t end; |
90 in Const (s, T --> T) $ t end; |
78 |
91 |
79 fun mk_times (t, u) = |
92 fun mk_times (t, u) = |
84 in |
97 in |
85 Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) --> |
98 Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) --> |
86 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) |
99 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) |
87 end; |
100 end; |
88 |
101 |
89 fun get_type thy ty = |
102 fun get_type thy prfx ty = |
90 let val {type_map, ...} = VCs.get thy |
103 let val {type_map, ...} = VCs.get thy |
91 in Symtab.lookup type_map ty end; |
104 in lookup_prfx prfx type_map ty end; |
92 |
105 |
93 fun mk_type _ "integer" = HOLogic.intT |
106 fun mk_type _ _ "integer" = HOLogic.intT |
94 | mk_type _ "boolean" = HOLogic.boolT |
107 | mk_type _ _ "boolean" = HOLogic.boolT |
95 | mk_type thy ty = |
108 | mk_type thy prfx ty = |
96 (case get_type thy ty of |
109 (case get_type thy prfx ty of |
97 NONE => |
110 NONE => |
98 Syntax.check_typ (Proof_Context.init_global thy) |
111 Syntax.check_typ (Proof_Context.init_global thy) |
99 (Type (Sign.full_name thy (Binding.name ty), [])) |
112 (Type (Sign.full_name thy (Binding.name ty), [])) |
100 | SOME T => T); |
113 | SOME T => T); |
101 |
114 |
118 fun strip_tilde s = |
131 fun strip_tilde s = |
119 unsuffix "~" s ^ "_init" handle Fail _ => s; |
132 unsuffix "~" s ^ "_init" handle Fail _ => s; |
120 |
133 |
121 val mangle_name = strip_underscores #> strip_tilde; |
134 val mangle_name = strip_underscores #> strip_tilde; |
122 |
135 |
123 fun mk_variables thy xs ty (tab, ctxt) = |
136 fun mk_variables thy prfx xs ty (tab, ctxt) = |
124 let |
137 let |
125 val T = mk_type thy ty; |
138 val T = mk_type thy prfx ty; |
126 val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt; |
139 val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt; |
127 val zs = map (Free o rpair T) ys; |
140 val zs = map (Free o rpair T) ys; |
128 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; |
141 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; |
129 |
142 |
130 fun get_record_info thy T = (case Record.dest_recTs T of |
143 fun get_record_info thy T = (case Record.dest_recTs T of |
278 | check_enum (el :: els) ((cname, _) :: cs) = |
291 | check_enum (el :: els) ((cname, _) :: cs) = |
279 if lcase_eq (el, cname) then check_enum els cs |
292 if lcase_eq (el, cname) then check_enum els cs |
280 else SOME ("either has no element " ^ el ^ |
293 else SOME ("either has no element " ^ el ^ |
281 " or it is at the wrong position"); |
294 " or it is at the wrong position"); |
282 |
295 |
283 fun add_type_def (s, Basic_Type ty) (ids, thy) = |
296 fun add_type_def prfx (s, Basic_Type ty) (ids, thy) = |
284 (check_no_assoc thy s; |
297 (check_no_assoc thy prfx s; |
285 (ids, |
298 (ids, |
286 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
299 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
287 (mk_type thy ty) thy |> snd)) |
300 (mk_type thy prfx ty) thy |> snd)) |
288 |
301 |
289 | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) = |
302 | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) = |
290 let |
303 let |
291 val (thy', tyname) = (case get_type thy s of |
304 val (thy', tyname) = (case get_type thy prfx s of |
292 NONE => |
305 NONE => |
293 let |
306 let |
294 val tyb = Binding.name s; |
307 val tyb = Binding.name s; |
295 val tyname = Sign.full_name thy tyb |
308 val tyname = Sign.full_name thy tyb |
296 in |
309 in |
302 tyname) |
315 tyname) |
303 end |
316 end |
304 | SOME (T as Type (tyname, [])) => |
317 | SOME (T as Type (tyname, [])) => |
305 (case Datatype_Data.get_constrs thy tyname of |
318 (case Datatype_Data.get_constrs thy tyname of |
306 NONE => assoc_ty_err thy T s "is not a datatype" |
319 NONE => assoc_ty_err thy T s "is not a datatype" |
307 | SOME cs => (case check_enum els cs of |
320 | SOME cs => |
308 NONE => (thy, tyname) |
321 let |
309 | SOME msg => assoc_ty_err thy T s msg))); |
322 val (prfx', _) = strip_prfx s; |
|
323 val els' = |
|
324 if prfx' = "" then els |
|
325 else map (unprefix (prfx' ^ "__")) els |
|
326 handle Fail _ => error ("Bad enumeration type " ^ s) |
|
327 in |
|
328 case check_enum els' cs of |
|
329 NONE => (thy, tyname) |
|
330 | SOME msg => assoc_ty_err thy T s msg |
|
331 end)); |
310 val cs = map Const (the (Datatype_Data.get_constrs thy' tyname)) |
332 val cs = map Const (the (Datatype_Data.get_constrs thy' tyname)) |
311 in |
333 in |
312 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, |
334 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, |
313 fold Name.declare els ctxt), |
335 fold Name.declare els ctxt), |
314 thy') |
336 thy') |
315 end |
337 end |
316 |
338 |
317 | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) = |
339 | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) = |
318 (check_no_assoc thy s; |
340 (check_no_assoc thy prfx s; |
319 (ids, |
341 (ids, |
320 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
342 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
321 (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) --> |
343 (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) --> |
322 mk_type thy resty) thy |> snd)) |
344 mk_type thy prfx resty) thy |> snd)) |
323 |
345 |
324 | add_type_def (s, Record_Type fldtys) (ids, thy) = |
346 | add_type_def prfx (s, Record_Type fldtys) (ids, thy) = |
325 (ids, |
347 (ids, |
326 let val fldTs = maps (fn (flds, ty) => |
348 let val fldTs = maps (fn (flds, ty) => |
327 map (rpair (mk_type thy ty)) flds) fldtys |
349 map (rpair (mk_type thy prfx ty)) flds) fldtys |
328 in case get_type thy s of |
350 in case get_type thy prfx s of |
329 NONE => |
351 NONE => |
330 Record.add_record true ([], Binding.name s) NONE |
352 Record.add_record true ([], Binding.name s) NONE |
331 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy |
353 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy |
332 | SOME rT => |
354 | SOME rT => |
333 (case get_record_info thy rT of |
355 (case get_record_info thy rT of |
347 "\ndoes not match declared type\n" ^ |
369 "\ndoes not match declared type\n" ^ |
348 Syntax.string_of_typ_global thy T)) fldTs; |
370 Syntax.string_of_typ_global thy T)) fldTs; |
349 thy)) |
371 thy)) |
350 end) |
372 end) |
351 |
373 |
352 | add_type_def (s, Pending_Type) (ids, thy) = |
374 | add_type_def prfx (s, Pending_Type) (ids, thy) = |
353 (check_no_assoc thy s; |
375 (check_no_assoc thy prfx s; |
354 (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd)); |
376 (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd)); |
355 |
377 |
356 |
378 |
357 fun term_of_expr thy types funs pfuns = |
379 fun term_of_expr thy prfx types pfuns = |
358 let |
380 let |
359 fun tm_of vs (Funct ("->", [e, e'])) = |
381 fun tm_of vs (Funct ("->", [e, e'])) = |
360 (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN) |
382 (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN) |
361 |
383 |
362 | tm_of vs (Funct ("<->", [e, e'])) = |
384 | tm_of vs (Funct ("<->", [e, e'])) = |
422 |
444 |
423 | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN) |
445 | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN) |
424 |
446 |
425 | tm_of vs (Quantifier (s, xs, ty, e)) = |
447 | tm_of vs (Quantifier (s, xs, ty, e)) = |
426 let |
448 let |
427 val (ys, vs') = mk_variables thy xs ty vs; |
449 val (ys, vs') = mk_variables thy prfx xs ty vs; |
428 val q = (case s of |
450 val q = (case s of |
429 "for_all" => HOLogic.mk_all |
451 "for_all" => HOLogic.mk_all |
430 | "for_some" => HOLogic.mk_exists) |
452 | "for_some" => HOLogic.mk_exists) |
431 in |
453 in |
432 (fold_rev (fn Free (x, T) => fn t => q (x, T, t)) |
454 (fold_rev (fn Free (x, T) => fn t => q (x, T, t)) |
440 (case try (unprefix "fld_") s of |
462 (case try (unprefix "fld_") s of |
441 SOME fname => (case es of |
463 SOME fname => (case es of |
442 [e] => |
464 [e] => |
443 let |
465 let |
444 val (t, rcdty) = tm_of vs e; |
466 val (t, rcdty) = tm_of vs e; |
445 val rT = mk_type thy rcdty |
467 val rT = mk_type thy prfx rcdty |
446 in case (get_record_info thy rT, lookup types rcdty) of |
468 in case (get_record_info thy rT, lookup types rcdty) of |
447 (SOME {fields, ...}, SOME (Record_Type fldtys)) => |
469 (SOME {fields, ...}, SOME (Record_Type fldtys)) => |
448 (case (find_field fname fields, |
470 (case (find_field fname fields, |
449 find_field' fname fldtys) of |
471 find_field' fname fldtys) of |
450 (SOME (fname', fT), SOME fldty) => |
472 (SOME (fname', fT), SOME fldty) => |
460 (case try (unprefix "upf_") s of |
482 (case try (unprefix "upf_") s of |
461 SOME fname => (case es of |
483 SOME fname => (case es of |
462 [e, e'] => |
484 [e, e'] => |
463 let |
485 let |
464 val (t, rcdty) = tm_of vs e; |
486 val (t, rcdty) = tm_of vs e; |
465 val rT = mk_type thy rcdty; |
487 val rT = mk_type thy prfx rcdty; |
466 val (u, fldty) = tm_of vs e'; |
488 val (u, fldty) = tm_of vs e'; |
467 val fT = mk_type thy fldty |
489 val fT = mk_type thy prfx fldty |
468 in case get_record_info thy rT of |
490 in case get_record_info thy rT of |
469 SOME {fields, ...} => |
491 SOME {fields, ...} => |
470 (case find_field fname fields of |
492 (case find_field fname fields of |
471 SOME (fname', fU) => |
493 SOME (fname', fU) => |
472 if fT = fU then |
494 if fT = fU then |
488 |
510 |
489 (* enumeration type to integer *) |
511 (* enumeration type to integer *) |
490 (case try (unsuffix "__pos") s of |
512 (case try (unsuffix "__pos") s of |
491 SOME tyname => (case es of |
513 SOME tyname => (case es of |
492 [e] => (Const (@{const_name pos}, |
514 [e] => (Const (@{const_name pos}, |
493 mk_type thy tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN) |
515 mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e), |
|
516 integerN) |
494 | _ => error ("Function " ^ s ^ " expects one argument")) |
517 | _ => error ("Function " ^ s ^ " expects one argument")) |
495 | NONE => |
518 | NONE => |
496 |
519 |
497 (* integer to enumeration type *) |
520 (* integer to enumeration type *) |
498 (case try (unsuffix "__val") s of |
521 (case try (unsuffix "__val") s of |
499 SOME tyname => (case es of |
522 SOME tyname => (case es of |
500 [e] => (Const (@{const_name val}, |
523 [e] => (Const (@{const_name val}, |
501 HOLogic.intT --> mk_type thy tyname) $ fst (tm_of vs e), tyname) |
524 HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e), |
|
525 tyname) |
502 | _ => error ("Function " ^ s ^ " expects one argument")) |
526 | _ => error ("Function " ^ s ^ " expects one argument")) |
503 | NONE => |
527 | NONE => |
504 |
528 |
505 (* successor / predecessor of enumeration type element *) |
529 (* successor / predecessor of enumeration type element *) |
506 if s = "succ" orelse s = "pred" then (case es of |
530 if s = "succ" orelse s = "pred" then (case es of |
507 [e] => |
531 [e] => |
508 let |
532 let |
509 val (t, tyname) = tm_of vs e; |
533 val (t, tyname) = tm_of vs e; |
510 val T = mk_type thy tyname |
534 val T = mk_type thy prfx tyname |
511 in (Const |
535 in (Const |
512 (if s = "succ" then @{const_name succ} |
536 (if s = "succ" then @{const_name succ} |
513 else @{const_name pred}, T --> T) $ t, tyname) |
537 else @{const_name pred}, T --> T) $ t, tyname) |
514 end |
538 end |
515 | _ => error ("Function " ^ s ^ " expects one argument")) |
539 | _ => error ("Function " ^ s ^ " expects one argument")) |
516 |
540 |
517 (* user-defined proof function *) |
541 (* user-defined proof function *) |
518 else |
542 else |
519 (case Symtab.lookup pfuns s of |
543 (case lookup_prfx prfx pfuns s of |
520 SOME (SOME (_, resty), t) => |
544 SOME (SOME (_, resty), t) => |
521 (list_comb (t, map (fst o tm_of vs) es), resty) |
545 (list_comb (t, map (fst o tm_of vs) es), resty) |
522 | _ => error ("Undeclared proof function " ^ s)))))) |
546 | _ => error ("Undeclared proof function " ^ s)))))) |
523 |
547 |
524 | tm_of vs (Element (e, es)) = |
548 | tm_of vs (Element (e, es)) = |
532 | tm_of vs (Update (e, es, e')) = |
556 | tm_of vs (Update (e, es, e')) = |
533 let val (t, ty) = tm_of vs e |
557 let val (t, ty) = tm_of vs e |
534 in case lookup types ty of |
558 in case lookup types ty of |
535 SOME (Array_Type (idxtys, elty)) => |
559 SOME (Array_Type (idxtys, elty)) => |
536 let |
560 let |
537 val T = foldr1 HOLogic.mk_prodT (map (mk_type thy) idxtys); |
561 val T = foldr1 HOLogic.mk_prodT |
538 val U = mk_type thy elty; |
562 (map (mk_type thy prfx) idxtys); |
|
563 val U = mk_type thy prfx elty; |
539 val fT = T --> U |
564 val fT = T --> U |
540 in |
565 in |
541 (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $ |
566 (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $ |
542 t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ |
567 t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ |
543 fst (tm_of vs e'), |
568 fst (tm_of vs e'), |
546 | _ => error (ty ^ " is not an array type") |
571 | _ => error (ty ^ " is not an array type") |
547 end |
572 end |
548 |
573 |
549 | tm_of vs (Record (s, flds)) = |
574 | tm_of vs (Record (s, flds)) = |
550 let |
575 let |
551 val T = mk_type thy s; |
576 val T = mk_type thy prfx s; |
552 val {extension = (ext_name, _), fields, ...} = |
577 val {extension = (ext_name, _), fields, ...} = |
553 (case get_record_info thy T of |
578 (case get_record_info thy T of |
554 NONE => error (s ^ " is not a record type") |
579 NONE => error (s ^ " is not a record type") |
555 | SOME info => info); |
580 | SOME info => info); |
556 val flds' = map (apsnd (tm_of vs)) flds; |
581 val flds' = map (apsnd (tm_of vs)) flds; |
570 | xs => error ("Duplicate field(s) " ^ commas xs ^ |
595 | xs => error ("Duplicate field(s) " ^ commas xs ^ |
571 " in record " ^ s)) |
596 " in record " ^ s)) |
572 in |
597 in |
573 (list_comb |
598 (list_comb |
574 (Const (ext_name, |
599 (Const (ext_name, |
575 map (mk_type thy) ftys @ [HOLogic.unitT] ---> T), |
600 map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T), |
576 fvals @ [HOLogic.unit]), |
601 fvals @ [HOLogic.unit]), |
577 s) |
602 s) |
578 end |
603 end |
579 |
604 |
580 | tm_of vs (Array (s, default, assocs)) = |
605 | tm_of vs (Array (s, default, assocs)) = |
581 (case lookup types s of |
606 (case lookup types s of |
582 SOME (Array_Type (idxtys, elty)) => |
607 SOME (Array_Type (idxtys, elty)) => |
583 let |
608 let |
584 val Ts = map (mk_type thy) idxtys; |
609 val Ts = map (mk_type thy prfx) idxtys; |
585 val T = foldr1 HOLogic.mk_prodT Ts; |
610 val T = foldr1 HOLogic.mk_prodT Ts; |
586 val U = mk_type thy elty; |
611 val U = mk_type thy prfx elty; |
587 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)] |
612 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)] |
588 | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost}, |
613 | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost}, |
589 T --> T --> HOLogic.mk_setT T) $ |
614 T --> T --> HOLogic.mk_setT T) $ |
590 fst (tm_of vs e) $ fst (tm_of vs e'); |
615 fst (tm_of vs e) $ fst (tm_of vs e'); |
591 fun mk_idx idx = |
616 fun mk_idx idx = |
616 | _ => error (s ^ " is not an array type")) |
641 | _ => error (s ^ " is not an array type")) |
617 |
642 |
618 in tm_of end; |
643 in tm_of end; |
619 |
644 |
620 |
645 |
621 fun term_of_rule thy types funs pfuns ids rule = |
646 fun term_of_rule thy prfx types pfuns ids rule = |
622 let val tm_of = fst o term_of_expr thy types funs pfuns ids |
647 let val tm_of = fst o term_of_expr thy prfx types pfuns ids |
623 in case rule of |
648 in case rule of |
624 Inference_Rule (es, e) => Logic.list_implies |
649 Inference_Rule (es, e) => Logic.list_implies |
625 (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e)) |
650 (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e)) |
626 | Substitution_Rule (es, e, e') => Logic.list_implies |
651 | Substitution_Rule (es, e, e') => Logic.list_implies |
627 (map (HOLogic.mk_Trueprop o tm_of) es, |
652 (map (HOLogic.mk_Trueprop o tm_of) es, |
674 val add_expr_pfuns = fold_expr |
699 val add_expr_pfuns = fold_expr |
675 (fn s => if is_pfun s then I else insert (op =) s) (K I); |
700 (fn s => if is_pfun s then I else insert (op =) s) (K I); |
676 |
701 |
677 val add_expr_idents = fold_expr (K I) (insert (op =)); |
702 val add_expr_idents = fold_expr (K I) (insert (op =)); |
678 |
703 |
679 fun pfun_type thy (argtys, resty) = |
704 fun pfun_type thy prfx (argtys, resty) = |
680 map (mk_type thy) argtys ---> mk_type thy resty; |
705 map (mk_type thy prfx) argtys ---> mk_type thy prfx resty; |
681 |
706 |
682 fun check_pfun_type thy s t optty1 optty2 = |
707 fun check_pfun_type thy prfx s t optty1 optty2 = |
683 let |
708 let |
684 val T = fastype_of t; |
709 val T = fastype_of t; |
685 fun check ty = |
710 fun check ty = |
686 let val U = pfun_type thy ty |
711 let val U = pfun_type thy prfx ty |
687 in |
712 in |
688 T = U orelse |
713 T = U orelse |
689 error ("Type\n" ^ |
714 error ("Type\n" ^ |
690 Syntax.string_of_typ_global thy T ^ |
715 Syntax.string_of_typ_global thy T ^ |
691 "\nof function " ^ |
716 "\nof function " ^ |
696 end |
721 end |
697 in (Option.map check optty1; Option.map check optty2; ()) end; |
722 in (Option.map check optty1; Option.map check optty2; ()) end; |
698 |
723 |
699 fun upd_option x y = if is_some x then x else y; |
724 fun upd_option x y = if is_some x then x else y; |
700 |
725 |
701 fun check_pfuns_types thy funs = |
726 fun check_pfuns_types thy prfx funs = |
702 Symtab.map (fn s => fn (optty, t) => |
727 Symtab.map (fn s => fn (optty, t) => |
703 let val optty' = lookup funs s |
728 let val optty' = lookup funs |
|
729 (if prfx = "" then s |
|
730 else unprefix (prfx ^ "__") s handle Fail _ => s) |
704 in |
731 in |
705 (check_pfun_type thy s t optty optty'; |
732 (check_pfun_type thy prfx s t optty optty'; |
706 (NONE |> upd_option optty |> upd_option optty', t)) |
733 (NONE |> upd_option optty |> upd_option optty', t)) |
707 end); |
734 end); |
708 |
735 |
709 |
736 |
710 (** the VC store **) |
737 (** the VC store **) |
711 |
738 |
712 fun err_vcs names = error (Pretty.string_of |
739 fun err_vcs names = error (Pretty.string_of |
713 (Pretty.big_list "The following verification conditions have not been proved:" |
740 (Pretty.big_list "The following verification conditions have not been proved:" |
714 (map Pretty.str names))) |
741 (map Pretty.str names))) |
715 |
742 |
716 fun set_env (env as {funs, ...}) thy = VCs.map (fn |
743 fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn |
717 {pfuns, type_map, env = NONE} => |
744 {pfuns, type_map, env = NONE} => |
718 {pfuns = check_pfuns_types thy funs pfuns, |
745 {pfuns = check_pfuns_types thy prefix funs pfuns, |
719 type_map = type_map, |
746 type_map = type_map, |
720 env = SOME env} |
747 env = SOME env} |
721 | _ => err_unfinished ()) thy; |
748 | _ => err_unfinished ()) thy; |
722 |
749 |
723 fun mk_pat s = (case Int.fromString s of |
750 fun mk_pat s = (case Int.fromString s of |
724 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] |
751 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] |
725 | NONE => error ("Bad conclusion identifier: C" ^ s)); |
752 | NONE => error ("Bad conclusion identifier: C" ^ s)); |
726 |
753 |
727 fun mk_vc thy types funs pfuns ids (tr, proved, ps, cs) = |
754 fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) = |
728 let val prop_of = |
755 let val prop_of = |
729 HOLogic.mk_Trueprop o fst o term_of_expr thy types funs pfuns ids |
756 HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids |
730 in |
757 in |
731 (tr, proved, |
758 (tr, proved, |
732 Element.Assumes (map (fn (s', e) => |
759 Element.Assumes (map (fn (s', e) => |
733 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps), |
760 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps), |
734 Element.Shows (map (fn (s', e) => |
761 Element.Shows (map (fn (s', e) => |
736 end; |
763 end; |
737 |
764 |
738 fun fold_vcs f vcs = |
765 fun fold_vcs f vcs = |
739 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs; |
766 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs; |
740 |
767 |
741 fun pfuns_of_vcs pfuns vcs = |
768 fun pfuns_of_vcs prfx pfuns vcs = |
742 fold_vcs (add_expr_pfuns o snd) vcs [] |> |
769 fold_vcs (add_expr_pfuns o snd) vcs [] |> |
743 filter_out (Symtab.defined pfuns); |
770 filter (is_none o lookup_prfx prfx pfuns); |
744 |
771 |
745 fun declare_missing_pfuns thy funs pfuns vcs (tab, ctxt) = |
772 fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) = |
746 let |
773 let |
747 val (fs, (tys, Ts)) = |
774 val (fs, (tys, Ts)) = |
748 pfuns_of_vcs pfuns vcs |> |
775 pfuns_of_vcs prfx pfuns vcs |> |
749 map_filter (fn s => lookup funs s |> |
776 map_filter (fn s => lookup funs s |> |
750 Option.map (fn ty => (s, (SOME ty, pfun_type thy ty)))) |> |
777 Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |> |
751 split_list ||> split_list; |
778 split_list ||> split_list; |
752 val (fs', ctxt') = Name.variants fs ctxt |
779 val (fs', ctxt') = Name.variants fs ctxt |
753 in |
780 in |
754 (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns, |
781 (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns, |
755 Element.Fixes (map2 (fn s => fn T => |
782 Element.Fixes (map2 (fn s => fn T => |
760 fun add_proof_fun prep (s, (optty, raw_t)) thy = |
787 fun add_proof_fun prep (s, (optty, raw_t)) thy = |
761 VCs.map (fn |
788 VCs.map (fn |
762 {env = SOME {proving = true, ...}, ...} => err_unfinished () |
789 {env = SOME {proving = true, ...}, ...} => err_unfinished () |
763 | {pfuns, type_map, env} => |
790 | {pfuns, type_map, env} => |
764 let |
791 let |
765 val optty' = (case env of |
792 val (optty', prfx) = (case env of |
766 SOME {funs, ...} => lookup funs s |
793 SOME {funs, prefix, ...} => (lookup funs s, prefix) |
767 | NONE => NONE); |
794 | NONE => (NONE, "")); |
768 val optty'' = NONE |> upd_option optty |> upd_option optty'; |
795 val optty'' = NONE |> upd_option optty |> upd_option optty'; |
769 val t = prep (Option.map (pfun_type thy) optty'') raw_t; |
796 val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t; |
770 val _ = (case fold_aterms (fn u => |
797 val _ = (case fold_aterms (fn u => |
771 if is_Var u orelse is_Free u then insert (op =) u else I) t [] of |
798 if is_Var u orelse is_Free u then insert (op =) u else I) t [] of |
772 [] => () |
799 [] => () |
773 | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ |
800 | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ |
774 "\nto be associated with proof function " ^ s ^ |
801 "\nto be associated with proof function " ^ s ^ |
775 " contains free variable(s) " ^ |
802 " contains free variable(s) " ^ |
776 commas (map (Syntax.string_of_term_global thy) ts))); |
803 commas (map (Syntax.string_of_term_global thy) ts))); |
777 in |
804 in |
778 (check_pfun_type thy s t optty optty'; |
805 (check_pfun_type thy prfx s t optty optty'; |
779 if is_some optty'' orelse is_none env then |
806 if is_some optty'' orelse is_none env then |
780 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns, |
807 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns, |
781 type_map = type_map, |
808 type_map = type_map, |
782 env = env} |
809 env = env} |
783 handle Symtab.DUP _ => error ("Proof function " ^ s ^ |
810 handle Symtab.DUP _ => error ("Proof function " ^ s ^ |
811 |
838 |
812 val is_closed = is_none o #env o VCs.get; |
839 val is_closed = is_none o #env o VCs.get; |
813 |
840 |
814 fun lookup_vc thy name = |
841 fun lookup_vc thy name = |
815 (case VCs.get thy of |
842 (case VCs.get thy of |
816 {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} => |
843 {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} => |
817 (case VCtab.lookup vcs name of |
844 (case VCtab.lookup vcs name of |
818 SOME vc => |
845 SOME vc => |
819 let val (pfuns', ctxt', ids') = |
846 let val (pfuns', ctxt', ids') = |
820 declare_missing_pfuns thy funs pfuns vcs ids |
847 declare_missing_pfuns thy prefix funs pfuns vcs ids |
821 in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end |
848 in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end |
822 | NONE => NONE) |
849 | NONE => NONE) |
823 | _ => NONE); |
850 | _ => NONE); |
824 |
851 |
825 fun get_vcs thy = (case VCs.get thy of |
852 fun get_vcs thy = (case VCs.get thy of |
826 {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} => |
853 {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} => |
827 let val (pfuns', ctxt', ids') = |
854 let val (pfuns', ctxt', ids') = |
828 declare_missing_pfuns thy funs pfuns vcs ids |
855 declare_missing_pfuns thy prefix funs pfuns vcs ids |
829 in |
856 in |
830 (ctxt @ [ctxt'], defs, |
857 (ctxt @ [ctxt'], defs, |
831 VCtab.dest vcs |> |
858 VCtab.dest vcs |> |
832 map (apsnd (mk_vc thy types funs pfuns' ids'))) |
859 map (apsnd (mk_vc thy prefix types pfuns' ids'))) |
833 end |
860 end |
834 | _ => ([], [], [])); |
861 | _ => ([], [], [])); |
835 |
862 |
836 fun mark_proved name thms = VCs.map (fn |
863 fun mark_proved name thms = VCs.map (fn |
837 {pfuns, type_map, |
864 {pfuns, type_map, |
838 env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => |
865 env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} => |
839 {pfuns = pfuns, |
866 {pfuns = pfuns, |
840 type_map = type_map, |
867 type_map = type_map, |
841 env = SOME {ctxt = ctxt, defs = defs, |
868 env = SOME {ctxt = ctxt, defs = defs, |
842 types = types, funs = funs, ids = ids, |
869 types = types, funs = funs, ids = ids, |
843 proving = true, |
870 proving = true, |
844 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
871 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
845 (trace, SOME thms, ps, cs)) vcs, |
872 (trace, SOME thms, ps, cs)) vcs, |
846 path = path}} |
873 path = path, |
|
874 prefix = prefix}} |
847 | x => x); |
875 | x => x); |
848 |
876 |
849 fun close thy = |
877 fun close thy = |
850 thy |> |
878 thy |> |
851 VCs.map (fn |
879 VCs.map (fn |
876 fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs)) |
904 fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs)) |
877 | dest_def _ = NONE; |
905 | dest_def _ = NONE; |
878 |
906 |
879 fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i); |
907 fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i); |
880 |
908 |
881 fun add_const (s, ty) ((tab, ctxt), thy) = |
909 fun add_const prfx (s, ty) ((tab, ctxt), thy) = |
882 let |
910 let |
883 val T = mk_type thy ty; |
911 val T = mk_type thy prfx ty; |
884 val b = Binding.name s; |
912 val b = Binding.name s; |
885 val c = Const (Sign.full_name thy b, T) |
913 val c = Const (Sign.full_name thy b, T) |
886 in |
914 in |
887 (c, |
915 (c, |
888 ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt), |
916 ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt), |
889 Sign.add_consts_i [(b, T, NoSyn)] thy)) |
917 Sign.add_consts_i [(b, T, NoSyn)] thy)) |
890 end; |
918 end; |
891 |
919 |
892 fun add_def types funs pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = |
920 fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) = |
893 (case lookup consts s of |
921 (case lookup consts s of |
894 SOME ty => |
922 SOME ty => |
895 let |
923 let |
896 val (t, ty') = term_of_expr thy types funs pfuns ids e; |
924 val (t, ty') = term_of_expr thy prfx types pfuns ids e; |
897 val T = mk_type thy ty; |
925 val T = mk_type thy prfx ty; |
898 val T' = mk_type thy ty'; |
926 val T' = mk_type thy prfx ty'; |
899 val _ = T = T' orelse |
927 val _ = T = T' orelse |
900 error ("Declared type " ^ ty ^ " of " ^ s ^ |
928 error ("Declared type " ^ ty ^ " of " ^ s ^ |
901 "\ndoes not match type " ^ ty' ^ " in definition"); |
929 "\ndoes not match type " ^ ty' ^ " in definition"); |
902 val id' = mk_rulename id; |
930 val id' = mk_rulename id; |
903 val lthy = Named_Target.theory_init thy; |
931 val lthy = Named_Target.theory_init thy; |
911 Name.declare s ctxt), |
939 Name.declare s ctxt), |
912 Local_Theory.exit_global lthy')) |
940 Local_Theory.exit_global lthy')) |
913 end |
941 end |
914 | NONE => error ("Undeclared constant " ^ s)); |
942 | NONE => error ("Undeclared constant " ^ s)); |
915 |
943 |
916 fun add_var (s, ty) (ids, thy) = |
944 fun add_var prfx (s, ty) (ids, thy) = |
917 let val ([Free p], ids') = mk_variables thy [s] ty ids |
945 let val ([Free p], ids') = mk_variables thy prfx [s] ty ids |
918 in (p, (ids', thy)) end; |
946 in (p, (ids', thy)) end; |
919 |
947 |
920 fun add_init_vars vcs (ids_thy as ((tab, _), _)) = |
948 fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) = |
921 fold_map add_var |
949 fold_map (add_var prfx) |
922 (map_filter |
950 (map_filter |
923 (fn s => case try (unsuffix "~") s of |
951 (fn s => case try (unsuffix "~") s of |
924 SOME s' => (case Symtab.lookup tab s' of |
952 SOME s' => (case Symtab.lookup tab s' of |
925 SOME (_, ty) => SOME (s, ty) |
953 SOME (_, ty) => SOME (s, ty) |
926 | NONE => error ("Undeclared identifier " ^ s')) |
954 | NONE => error ("Undeclared identifier " ^ s')) |
933 |
961 |
934 fun rulenames rules = commas |
962 fun rulenames rules = commas |
935 (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules); |
963 (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules); |
936 |
964 |
937 (* sort definitions according to their dependency *) |
965 (* sort definitions according to their dependency *) |
938 fun sort_defs _ _ [] sdefs = rev sdefs |
966 fun sort_defs _ _ _ [] sdefs = rev sdefs |
939 | sort_defs pfuns consts defs sdefs = |
967 | sort_defs prfx pfuns consts defs sdefs = |
940 (case find_first (fn (_, (_, e)) => |
968 (case find_first (fn (_, (_, e)) => |
941 forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso |
969 forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns e []) andalso |
942 forall (fn id => |
970 forall (fn id => |
943 member (fn (s, (_, (s', _))) => s = s') sdefs id orelse |
971 member (fn (s, (_, (s', _))) => s = s') sdefs id orelse |
944 consts id) |
972 consts id) |
945 (add_expr_idents e [])) defs of |
973 (add_expr_idents e [])) defs of |
946 SOME d => sort_defs pfuns consts |
974 SOME d => sort_defs prfx pfuns consts |
947 (remove (op =) d defs) (d :: sdefs) |
975 (remove (op =) d defs) (d :: sdefs) |
948 | NONE => error ("Bad definitions: " ^ rulenames defs)); |
976 | NONE => error ("Bad definitions: " ^ rulenames defs)); |
949 |
977 |
950 fun set_vcs ({types, vars, consts, funs} : decls) |
978 fun set_vcs ({types, vars, consts, funs} : decls) |
951 (rules, _) ((_, ident), vcs) path thy = |
979 (rules, _) ((_, ident), vcs) path prfx thy = |
952 let |
980 let |
953 val {pfuns, ...} = VCs.get thy; |
981 val {pfuns, ...} = VCs.get thy; |
954 val (defs, rules') = partition_opt dest_def rules; |
982 val (defs, rules') = partition_opt dest_def rules; |
955 val consts' = |
983 val consts' = |
956 subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); |
984 subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts); |
963 val vcs' = VCtab.make (maps (fn (tr, vcs) => |
991 val vcs' = VCtab.make (maps (fn (tr, vcs) => |
964 map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs))) |
992 map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs))) |
965 (filter_out (is_trivial_vc o snd) vcs)) vcs); |
993 (filter_out (is_trivial_vc o snd) vcs)) vcs); |
966 |
994 |
967 val _ = (case filter_out (is_some o lookup funs) |
995 val _ = (case filter_out (is_some o lookup funs) |
968 (pfuns_of_vcs pfuns vcs') of |
996 (pfuns_of_vcs prfx pfuns vcs') of |
969 [] => () |
997 [] => () |
970 | fs => error ("Undeclared proof function(s) " ^ commas fs)); |
998 | fs => error ("Undeclared proof function(s) " ^ commas fs)); |
971 |
999 |
972 val (((defs', vars''), ivars), (ids, thy')) = |
1000 val (((defs', vars''), ivars), (ids, thy')) = |
973 ((Symtab.empty |> |
1001 ((Symtab.empty |> |
974 Symtab.update ("false", (HOLogic.false_const, booleanN)) |> |
1002 Symtab.update ("false", (HOLogic.false_const, booleanN)) |> |
975 Symtab.update ("true", (HOLogic.true_const, booleanN)), |
1003 Symtab.update ("true", (HOLogic.true_const, booleanN)), |
976 Name.context), |
1004 Name.context), |
977 thy |> Sign.add_path (Long_Name.base_name ident)) |> |
1005 thy |> Sign.add_path (Long_Name.base_name ident)) |> |
978 fold add_type_def (items types) |> |
1006 fold (add_type_def prfx) (items types) |> |
979 fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) => |
1007 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) => |
980 ids_thy |> |
1008 ids_thy |> |
981 fold_map (add_def types funs pfuns consts) |
1009 fold_map (add_def prfx types pfuns consts) |
982 (sort_defs pfuns (Symtab.defined tab) defs []) ||>> |
1010 (sort_defs prfx pfuns (Symtab.defined tab) defs []) ||>> |
983 fold_map add_var (items vars) ||>> |
1011 fold_map (add_var prfx) (items vars) ||>> |
984 add_init_vars vcs'); |
1012 add_init_vars prfx vcs'); |
985 |
1013 |
986 val ctxt = |
1014 val ctxt = |
987 [Element.Fixes (map (fn (s, T) => |
1015 [Element.Fixes (map (fn (s, T) => |
988 (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)), |
1016 (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)), |
989 Element.Assumes (map (fn (id, rl) => |
1017 Element.Assumes (map (fn (id, rl) => |
990 ((mk_rulename id, []), |
1018 ((mk_rulename id, []), |
991 [(term_of_rule thy' types funs pfuns ids rl, [])])) |
1019 [(term_of_rule thy' prfx types pfuns ids rl, [])])) |
992 other_rules), |
1020 other_rules), |
993 Element.Notes (Thm.definitionK, |
1021 Element.Notes (Thm.definitionK, |
994 [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])] |
1022 [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])] |
995 |
1023 |
996 in |
1024 in |
997 set_env {ctxt = ctxt, defs = defs', types = types, funs = funs, |
1025 set_env {ctxt = ctxt, defs = defs', types = types, funs = funs, |
998 ids = ids, proving = false, vcs = vcs', path = path} thy' |
1026 ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy' |
999 end; |
1027 end; |
1000 |
1028 |
1001 end; |
1029 end; |