11 Path.T -> theory -> theory |
11 Path.T -> theory -> theory |
12 val add_proof_fun: (typ option -> 'a -> term) -> |
12 val add_proof_fun: (typ option -> 'a -> term) -> |
13 string * ((string list * string) option * 'a) -> |
13 string * ((string list * string) option * 'a) -> |
14 theory -> theory |
14 theory -> theory |
15 val lookup_vc: theory -> string -> (Element.context_i list * |
15 val lookup_vc: theory -> string -> (Element.context_i list * |
16 (string * bool * Element.context_i * Element.statement_i)) option |
16 (string * thm list option * Element.context_i * Element.statement_i)) option |
17 val get_vcs: theory -> |
17 val get_vcs: theory -> |
18 Element.context_i list * (binding * thm) list * |
18 Element.context_i list * (binding * thm) list * (string * |
19 (string * (string * bool * Element.context_i * Element.statement_i)) list |
19 (string * thm list option * Element.context_i * Element.statement_i)) list |
20 val mark_proved: string -> theory -> theory |
20 val mark_proved: string -> thm list -> theory -> theory |
21 val close: theory -> theory |
21 val close: theory -> theory |
22 val is_closed: theory -> bool |
22 val is_closed: theory -> bool |
23 end; |
23 end; |
24 |
24 |
25 structure SPARK_VCs: SPARK_VCS = |
25 structure SPARK_VCs: SPARK_VCS = |
614 defs: (binding * thm) list, |
614 defs: (binding * thm) list, |
615 types: fdl_type tab, |
615 types: fdl_type tab, |
616 funs: (string list * string) tab, |
616 funs: (string list * string) tab, |
617 ids: (term * string) Symtab.table * Name.context, |
617 ids: (term * string) Symtab.table * Name.context, |
618 proving: bool, |
618 proving: bool, |
619 vcs: (string * bool * |
619 vcs: (string * thm list option * |
620 (string * expr) list * (string * expr) list) VCtab.table, |
620 (string * expr) list * (string * expr) list) VCtab.table, |
621 path: Path.T} option} |
621 path: Path.T} option} |
622 val empty : T = {pfuns = Symtab.empty, env = NONE} |
622 val empty : T = {pfuns = Symtab.empty, env = NONE} |
623 val extend = I |
623 val extend = I |
624 fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) = |
624 fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) = |
711 VCtab.dest vcs |> |
711 VCtab.dest vcs |> |
712 map (apsnd (mk_vc thy types funs pfuns' ids'))) |
712 map (apsnd (mk_vc thy types funs pfuns' ids'))) |
713 end |
713 end |
714 | _ => ([], [], [])); |
714 | _ => ([], [], [])); |
715 |
715 |
716 fun mark_proved name = VCs.map (fn |
716 fun mark_proved name thms = VCs.map (fn |
717 {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => |
717 {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => |
718 {pfuns = pfuns, |
718 {pfuns = pfuns, |
719 env = SOME {ctxt = ctxt, defs = defs, |
719 env = SOME {ctxt = ctxt, defs = defs, |
720 types = types, funs = funs, ids = ids, |
720 types = types, funs = funs, ids = ids, |
721 proving = true, |
721 proving = true, |
722 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
722 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
723 (trace, true, ps, cs)) vcs, |
723 (trace, SOME thms, ps, cs)) vcs, |
724 path = path}} |
724 path = path}} |
725 | x => x); |
725 | x => x); |
726 |
726 |
727 fun close thy = VCs.map (fn |
727 fun close thy = VCs.map (fn |
728 {pfuns, env = SOME {vcs, path, ...}} => |
728 {pfuns, env = SOME {vcs, path, ...}} => |
729 (case VCtab.fold_rev (fn (s, (_, p, _, _)) => |
729 (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) => |
730 (if p then apfst else apsnd) (cons s)) vcs ([], []) of |
730 (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of |
731 (proved, []) => |
731 (proved, []) => |
732 (File.write (Path.ext "prv" path) |
732 (Thm.join_proofs (maps (the o #2 o snd) proved); |
733 (concat (map (fn s => snd (strip_number s) ^ |
733 File.write (Path.ext "prv" path) |
|
734 (concat (map (fn (s, _) => snd (strip_number s) ^ |
734 " -- proved by " ^ Distribution.version ^ "\n") proved)); |
735 " -- proved by " ^ Distribution.version ^ "\n") proved)); |
735 {pfuns = pfuns, env = NONE}) |
736 {pfuns = pfuns, env = NONE}) |
736 | (_, unproved) => err_vcs unproved) |
737 | (_, unproved) => err_vcs (map fst unproved)) |
737 | x => x) thy; |
738 | x => x) thy; |
738 |
739 |
739 |
740 |
740 (** set up verification conditions **) |
741 (** set up verification conditions **) |
741 |
742 |
832 List.partition (complex_rule o snd) rules'; |
833 List.partition (complex_rule o snd) rules'; |
833 val _ = if null rules'' then () |
834 val _ = if null rules'' then () |
834 else warning ("Ignoring rules: " ^ rulenames rules''); |
835 else warning ("Ignoring rules: " ^ rulenames rules''); |
835 |
836 |
836 val vcs' = VCtab.make (maps (fn (tr, vcs) => |
837 val vcs' = VCtab.make (maps (fn (tr, vcs) => |
837 map (fn (s, (ps, cs)) => (s, (tr, false, ps, cs))) |
838 map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs))) |
838 (filter_out (is_trivial_vc o snd) vcs)) vcs); |
839 (filter_out (is_trivial_vc o snd) vcs)) vcs); |
839 |
840 |
840 val _ = (case filter_out (is_some o lookup funs) |
841 val _ = (case filter_out (is_some o lookup funs) |
841 (pfuns_of_vcs pfuns vcs') of |
842 (pfuns_of_vcs pfuns vcs') of |
842 [] => () |
843 [] => () |