author | haftmann |
Wed, 01 Sep 2010 15:33:59 +0200 | |
changeset 39020 | ac0f24f850c9 |
parent 38795 | 848be46708dc |
child 39687 | 4e9b6ada3a21 |
permissions | -rw-r--r-- |
33419 | 1 |
(* Title: HOL/Boogie/Tools/boogie_vcs.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Store for Boogie's verification conditions. |
|
5 |
*) |
|
6 |
||
7 |
signature BOOGIE_VCS = |
|
8 |
sig |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
9 |
type vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
10 |
val prop_of_vc: vc -> term |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
11 |
val size_of: vc -> int |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
12 |
val names_of: vc -> string list * string list |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
13 |
val path_names_of: vc -> (string * bool) list list |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
14 |
val paths_of: vc -> vc list |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
15 |
val split_path: int -> vc -> (vc * vc) option |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
16 |
val extract: vc -> string -> vc option |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
17 |
val only: string list -> vc -> vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
18 |
val without: string list -> vc -> vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
19 |
val paths_and: int list -> string list -> vc -> vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
20 |
val paths_without: int list -> string list -> vc -> vc |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
21 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
22 |
datatype state = Proved | NotProved | PartiallyProved |
33419 | 23 |
val set: (string * term) list -> theory -> theory |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
24 |
val lookup: theory -> string -> vc option |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
25 |
val discharge: string * (vc * thm) -> theory -> theory |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
26 |
val state_of: theory -> (string * state) list |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
27 |
val state_of_vc: theory -> string -> string list * string list |
33419 | 28 |
val close: theory -> theory |
29 |
val is_closed: theory -> bool |
|
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
30 |
|
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
31 |
val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) -> |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
32 |
theory -> theory |
38246
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
33 |
val add_assertion_filter: (term -> bool) -> theory -> theory |
33419 | 34 |
end |
35 |
||
36 |
structure Boogie_VCs: BOOGIE_VCS = |
|
37 |
struct |
|
38 |
||
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
39 |
fun app_both f g (x, y) = (f x, g y) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
40 |
fun app_hd_tl f g = (fn [] => [] | x :: xs => f x :: map g xs) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
41 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
42 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
43 |
(* abstract representation of verification conditions *) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
44 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
45 |
datatype vc = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
46 |
Assume of term * vc | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
47 |
Assert of (string * term) * vc | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
48 |
Ignore of vc | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
49 |
Proved of string * vc | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
50 |
Choice of vc * vc | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
51 |
True |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
52 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
53 |
val assume = curry Assume and assert = curry Assert |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
54 |
and proved = curry Proved and choice = curry Choice |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
55 |
and choice' = curry (Choice o swap) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
56 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
57 |
val vc_of_term = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
58 |
let |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
59 |
fun vc_of @{term True} = NONE |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
60 |
| vc_of (@{term assert_at} $ Free (n, _) $ t) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
61 |
SOME (Assert ((n, t), True)) |
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38246
diff
changeset
|
62 |
| vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u |
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38246
diff
changeset
|
63 |
| vc_of (@{term HOL.implies} $ t $ u) = |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
64 |
vc_of u |> Option.map (assume t) |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
65 |
| vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) = |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
66 |
SOME (vc_of u |> the_default True |> assert (n, t)) |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
67 |
| vc_of (@{term HOL.conj} $ t $ u) = |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
68 |
(case (vc_of t, vc_of u) of |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
69 |
(NONE, r) => r |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
70 |
| (l, NONE) => l |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
71 |
| (SOME lv, SOME rv) => SOME (Choice (lv, rv))) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
72 |
| vc_of t = raise TERM ("vc_of_term", [t]) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
73 |
in the_default True o vc_of end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
74 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
75 |
val prop_of_vc = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
76 |
let |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset
|
77 |
fun mk_conj t u = @{term HOL.conj} $ t $ u |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
78 |
|
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38246
diff
changeset
|
79 |
fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
80 |
| term_of (Assert ((n, t), v)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
81 |
mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
82 |
| term_of (Ignore v) = term_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
83 |
| term_of (Proved (_, v)) = term_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
84 |
| term_of (Choice (lv, rv)) = mk_conj (term_of lv) (term_of rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
85 |
| term_of True = @{term True} |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
86 |
in HOLogic.mk_Trueprop o term_of end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
87 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
88 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
89 |
(* properties of verification conditions *) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
90 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
91 |
fun size_of (Assume (_, v)) = size_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
92 |
| size_of (Assert (_, v)) = size_of v + 1 |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
93 |
| size_of (Ignore v) = size_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
94 |
| size_of (Proved (_, v)) = size_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
95 |
| size_of (Choice (lv, rv)) = size_of lv + size_of rv |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
96 |
| size_of True = 0 |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
97 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
98 |
val names_of = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
99 |
let |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
100 |
fun add (Assume (_, v)) = add v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
101 |
| add (Assert ((n, _), v)) = apfst (cons n) #> add v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
102 |
| add (Ignore v) = add v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
103 |
| add (Proved (n, v)) = apsnd (cons n) #> add v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
104 |
| add (Choice (lv, rv)) = add lv #> add rv |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
105 |
| add True = I |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
106 |
in (fn vc => pairself rev (add vc ([], []))) end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
107 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
108 |
fun path_names_of (Assume (_, v)) = path_names_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
109 |
| path_names_of (Assert ((n, _), v)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
110 |
path_names_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
111 |
|> app_hd_tl (cons (n, true)) (cons (n, false)) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
112 |
| path_names_of (Ignore v) = path_names_of v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
113 |
| path_names_of (Proved (n, v)) = map (cons (n, false)) (path_names_of v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
114 |
| path_names_of (Choice (lv, rv)) = path_names_of lv @ path_names_of rv |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
115 |
| path_names_of True = [[]] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
116 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
117 |
fun count_paths (Assume (_, v)) = count_paths v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
118 |
| count_paths (Assert (_, v)) = count_paths v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
119 |
| count_paths (Ignore v) = count_paths v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
120 |
| count_paths (Proved (_, v)) = count_paths v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
121 |
| count_paths (Choice (lv, rv)) = count_paths lv + count_paths rv |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
122 |
| count_paths True = 1 |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
123 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
124 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
125 |
(* extract parts of a verification condition *) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
126 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
127 |
fun paths_of (Assume (t, v)) = paths_of v |> map (assume t) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
128 |
| paths_of (Assert (a, v)) = paths_of v |> app_hd_tl (assert a) Ignore |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
129 |
| paths_of (Ignore v) = paths_of v |> map Ignore |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
130 |
| paths_of (Proved (n, v)) = paths_of v |> app_hd_tl (proved n) Ignore |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
131 |
| paths_of (Choice (lv, rv)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
132 |
map (choice' True) (paths_of lv) @ map (choice True) (paths_of rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
133 |
| paths_of True = [True] |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
134 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
135 |
fun prune f (Assume (t, v)) = Option.map (assume t) (prune f v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
136 |
| prune f (Assert (a, v)) = f a v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
137 |
| prune f (Ignore v) = Option.map Ignore (prune f v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
138 |
| prune f (Proved (n, v)) = Option.map (proved n) (prune f v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
139 |
| prune f (Choice (lv, rv)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
140 |
(case (prune f lv, prune f rv) of |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
141 |
(NONE, r) => r |> Option.map (choice True) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
142 |
| (l, NONE) => l |> Option.map (choice' True) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
143 |
| (SOME lv', SOME rv') => SOME (Choice (lv', rv'))) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
144 |
| prune _ True = NONE |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
145 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
146 |
val split_path = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
147 |
let |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
148 |
fun app f = Option.map (pairself f) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
149 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
150 |
fun split i (Assume (t, v)) = app (assume t) (split i v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
151 |
| split i (Assert (a, v)) = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
152 |
if i > 1 |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
153 |
then Option.map (app_both (assert a) Ignore) (split (i-1) v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
154 |
else Option.map (pair (Assert (a, True))) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
155 |
(prune (SOME o Assert oo pair) (Ignore v)) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
156 |
| split i (Ignore v) = app Ignore (split i v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
157 |
| split i (Proved (n, v)) = app (proved n) (split i v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
158 |
| split i (Choice (v, True)) = app (choice' True) (split i v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
159 |
| split i (Choice (True, v)) = app (choice True) (split i v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
160 |
| split _ _ = NONE |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
161 |
in split end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
162 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
163 |
fun select_labels P = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
164 |
let |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
165 |
fun assert (a as (n, _)) v = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
166 |
if P n then SOME (Assert (a, the_default True v)) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
167 |
else Option.map Ignore v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
168 |
fun sel vc = prune (fn a => assert a o sel) vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
169 |
in sel end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
170 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
171 |
fun extract vc l = select_labels (equal l) vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
172 |
fun only ls = the_default True o select_labels (member (op =) ls) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
173 |
fun without ls = the_default True o select_labels (not o member (op =) ls) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
174 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
175 |
fun select_paths ps sub_select = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
176 |
let |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
177 |
fun disjoint pp = null (inter (op =) ps pp) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
178 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
179 |
fun sel pp (Assume (t, v)) = Assume (t, sel pp v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
180 |
| sel pp (Assert (a, v)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
181 |
if member (op =) ps (hd pp) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
182 |
then Assert (a, sel pp v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
183 |
else Ignore (sel pp v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
184 |
| sel pp (Ignore v) = Ignore (sel pp v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
185 |
| sel pp (Proved (n, v)) = Proved (n, sel pp v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
186 |
| sel pp (Choice (lv, rv)) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
187 |
let val (lpp, rpp) = chop (count_paths lv) pp |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
188 |
in |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
189 |
if disjoint lpp then Choice (sub_select lv, sel rpp rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
190 |
else if disjoint rpp then Choice (sel lpp lv, sub_select rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
191 |
else Choice (sel lpp lv, sel rpp rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
192 |
end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
193 |
| sel _ True = True |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
194 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
195 |
fun sel0 vc = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
196 |
let val pp = 1 upto count_paths vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
197 |
in if disjoint pp then True else sel pp vc end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
198 |
in sel0 end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
199 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
200 |
fun paths_and ps ls = select_paths ps (only ls) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
201 |
fun paths_without ps ls = without ls o select_paths ps (K True) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
202 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
203 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
204 |
(* discharge parts of a verification condition *) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
205 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
206 |
local |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
207 |
fun cprop_of thy t = Thm.cterm_of thy (HOLogic.mk_Trueprop t) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
208 |
fun imp_intr ct thm = Thm.implies_intr ct thm COMP_INCR @{thm impI} |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
209 |
fun imp_elim th thm = @{thm mp} OF [thm, th] |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
210 |
fun conj1 thm = @{thm conjunct1} OF [thm] |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
211 |
fun conj2 thm = @{thm conjunct2} OF [thm] |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
212 |
fun conj_intr lth rth = @{thm conjI} OF [lth, rth] |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
213 |
in |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
214 |
fun thm_of thy (Assume (t, v)) = imp_intr (cprop_of thy t) (thm_of thy v) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
215 |
| thm_of thy (Assert (_, v)) = thm_of thy v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
216 |
| thm_of thy (Ignore v) = thm_of thy v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
217 |
| thm_of thy (Proved (_, v)) = thm_of thy v |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
218 |
| thm_of thy (Choice (lv, rv)) = conj_intr (thm_of thy lv) (thm_of thy rv) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
219 |
| thm_of _ True = @{thm TrueI} |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
220 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
221 |
fun join (Assume (_, pv), pthm) (Assume (t, v), thm) = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
222 |
let |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
223 |
val mk_prop = Thm.capply @{cterm Trueprop} |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
224 |
val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
225 |
val th = Thm.assume ct |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
226 |
val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
227 |
in (Assume (t, v'), imp_intr ct thm') end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
228 |
| join (Assert ((pn, pt), pv), pthm) (Assert ((n, t), v), thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
229 |
let val pthm1 = conj1 pthm |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
230 |
in |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
231 |
if pn = n andalso pt aconv t |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
232 |
then |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
233 |
let val (v', thm') = join (pv, conj2 pthm) (v, thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
234 |
in (Proved (n, v'), conj_intr pthm1 thm') end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
235 |
else raise THM ("join: not matching", 1, [thm, pthm]) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
236 |
end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
237 |
| join (Ignore pv, pthm) (Assert (a, v), thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
238 |
join (pv, pthm) (v, thm) |>> assert a |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
239 |
| join (Proved (_, pv), pthm) (Proved (n, v), thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
240 |
let val (v', thm') = join (pv, pthm) (v, conj2 thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
241 |
in (Proved (n, v'), conj_intr (conj1 thm) thm') end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
242 |
| join (Ignore pv, pthm) (Proved (n, v), thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
243 |
let val (v', thm') = join (pv, pthm) (v, conj2 thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
244 |
in (Proved (n, v'), conj_intr (conj1 thm) thm') end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
245 |
| join (Choice (plv, prv), pthm) (Choice (lv, rv), thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
246 |
let |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
247 |
val (lv', lthm) = join (plv, conj1 pthm) (lv, conj1 thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
248 |
val (rv', rthm) = join (prv, conj2 pthm) (rv, conj2 thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
249 |
in (Choice (lv', rv'), conj_intr lthm rthm) end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
250 |
| join (True, pthm) (v, thm) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
251 |
if Thm.prop_of pthm aconv @{prop True} then (v, thm) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
252 |
else raise THM ("join: not True", 1, [pthm]) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
253 |
| join (_, pthm) (_, thm) = raise THM ("join: not matching", 1, [thm, pthm]) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
254 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
255 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
256 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
257 |
(* the VC store *) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
258 |
|
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
259 |
fun err_unfinished () = error "An unfinished Boogie environment is still open." |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
260 |
|
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
261 |
fun err_vcs names = error (Pretty.string_of |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
262 |
(Pretty.big_list "Undischarged Boogie verification conditions found:" |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
263 |
(map Pretty.str names))) |
33419 | 264 |
|
33522 | 265 |
structure VCs = Theory_Data |
33419 | 266 |
( |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
267 |
type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option |
33419 | 268 |
val empty = NONE |
269 |
val extend = I |
|
33522 | 270 |
fun merge (NONE, NONE) = NONE |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
271 |
| merge _ = err_unfinished () |
33419 | 272 |
) |
273 |
||
38246
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
274 |
fun serial_ord ((i, _), (j, _)) = int_ord (i, j) |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
275 |
|
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
276 |
structure Filters = Theory_Data |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
277 |
( |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
278 |
type T = (serial * (term -> bool)) OrdList.T |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
279 |
val empty = [] |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
280 |
val extend = I |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
281 |
fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1 |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
282 |
) |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
283 |
|
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
284 |
fun add_assertion_filter f = |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
285 |
Filters.map (OrdList.insert serial_ord (serial (), f)) |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
286 |
|
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
287 |
fun filter_assertions thy = |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
288 |
let |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
289 |
fun filt_assert [] a = assert a |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
290 |
| filt_assert ((_, f) :: fs) (a as (_, t)) = |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
291 |
if f t then filt_assert fs a else I |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
292 |
|
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
293 |
fun filt fs vc = |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
294 |
the_default True (prune (fn a => SOME o filt_assert fs a o filt fs) vc) |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
295 |
in filt (Filters.get thy) end |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
296 |
|
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
297 |
fun prep thy = |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
298 |
vc_of_term #> |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
299 |
filter_assertions thy #> |
130d89f79ac1
added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
boehmes
parents:
35863
diff
changeset
|
300 |
(fn vc => (vc, (prop_of_vc vc, thm_of thy vc))) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
301 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
302 |
fun set vcs thy = VCs.map (fn |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
303 |
NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
304 |
| SOME _ => err_unfinished ()) thy |
33419 | 305 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33522
diff
changeset
|
306 |
fun lookup thy name = |
33419 | 307 |
(case VCs.get thy of |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
308 |
SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name) |
33419 | 309 |
| NONE => NONE) |
310 |
||
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
311 |
fun discharge (name, prf) = |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
312 |
let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
313 |
in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
314 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
315 |
datatype state = Proved | NotProved | PartiallyProved |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
316 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
317 |
fun state_of_vc thy name = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
318 |
(case lookup thy name of |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
319 |
SOME vc => names_of vc |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
320 |
| NONE => ([], [])) |
33419 | 321 |
|
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
322 |
fun state_of_vc' (vc, _) = |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
323 |
(case names_of vc of |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
324 |
([], _) => Proved |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
325 |
| (_, []) => NotProved |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
326 |
| (_, _) => PartiallyProved) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
327 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
328 |
fun state_of thy = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
329 |
(case VCs.get thy of |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
330 |
SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs) |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
331 |
| NONE => []) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
332 |
|
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
333 |
fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
334 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
335 |
fun close thy = thy |> VCs.map (fn |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
336 |
SOME (vcs, g) => |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
337 |
let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
338 |
in |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
339 |
Symtab.dest vcs |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
340 |
|> map_filter (fn (n, vc) => if check vc then NONE else SOME n) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
341 |
|> (fn names => if null names then NONE else err_vcs names) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
342 |
end |
33419 | 343 |
| NONE => NONE) |
344 |
||
345 |
val is_closed = is_none o VCs.get |
|
346 |
||
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
347 |
fun rewrite_vcs f g thy = |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
348 |
let |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
349 |
fun rewr (_, (t, _)) = vc_of_term (f thy t) |
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
350 |
|> (fn vc => (vc, (t, thm_of thy vc))) |
39020 | 351 |
in VCs.map (Option.map (fn (vcs, _) => (Symtab.map (K rewr) vcs, g))) thy end |
35863
d4218a55cf20
provide a hook to safely manipulate verification conditions
boehmes
parents:
34181
diff
changeset
|
352 |
|
33419 | 353 |
end |