author | boehmes |
Fri, 11 Dec 2009 15:35:29 +0100 | |
changeset 34068 | a78307d72e58 |
parent 33671 | 4b0f2599ed48 |
child 34079 | 3edfefaaf355 |
permissions | -rw-r--r-- |
33419 | 1 |
(* Title: HOL/Boogie/Tools/boogie_commands.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Isar commands to create a Boogie environment simulation. |
|
5 |
*) |
|
6 |
||
7 |
signature BOOGIE_COMMANDS = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
10 |
end |
|
11 |
||
12 |
structure Boogie_Commands: BOOGIE_COMMANDS = |
|
13 |
struct |
|
14 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
15 |
(* commands *) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
16 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
17 |
fun boogie_load (quiet, base_name) thy = |
33419 | 18 |
let |
19 |
val path = Path.explode (base_name ^ ".b2i") |
|
20 |
val _ = File.exists path orelse |
|
21 |
error ("Unable to find file " ^ quote (Path.implode path)) |
|
22 |
val _ = Boogie_VCs.is_closed thy orelse |
|
23 |
error ("Found the beginning of a new Boogie environment, " ^ |
|
24 |
"but another Boogie environment is still open.") |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
25 |
in Boogie_Loader.load_b2i (not quiet) path thy end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
26 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
27 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
28 |
datatype vc_opts = VC_full of bool | VC_only of string list |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
29 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
30 |
fun get_vc thy vc_name = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
31 |
(case Boogie_VCs.lookup thy vc_name of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
32 |
SOME vc => vc |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
33 |
| NONE => |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
34 |
(case AList.lookup (op =) (Boogie_VCs.state_of thy) vc_name of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
35 |
SOME Boogie_VCs.Proved => error ("The verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
36 |
quote vc_name ^ " has already been proved.") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
37 |
| _ => error ("There is no verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
38 |
quote vc_name ^ "."))) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
39 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
40 |
fun boogie_vc (vc_opts, vc_name) lthy = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
41 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
42 |
val thy = ProofContext.theory_of lthy |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
43 |
val vc = get_vc thy vc_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
44 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
45 |
val (sks, ts) = split_list |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
46 |
(case vc_opts of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
47 |
VC_full paths => [vc] |> paths ? maps Boogie_VCs.paths_of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
48 |
| VC_only assertions => map_filter (Boogie_VCs.extract vc) assertions) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
49 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
50 |
val discharge = fold (Boogie_VCs.discharge o pair vc_name) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
51 |
fun after_qed [thms] = Local_Theory.theory (discharge (sks ~~ thms)) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
52 |
| after_qed _ = I |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
53 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
54 |
lthy |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
55 |
|> fold Variable.auto_fixes ts |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
56 |
|> Proof.theorem_i NONE after_qed [map (rpair []) ts] |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
57 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
58 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
59 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
60 |
fun write_list head pp xs = Pretty.writeln (Pretty.big_list head (map pp xs)) |
33419 | 61 |
|
62 |
fun boogie_status thy = |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
63 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
64 |
fun string_of_state Boogie_VCs.Proved = "proved" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
65 |
| string_of_state Boogie_VCs.NotProved = "not proved" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
66 |
| string_of_state Boogie_VCs.PartiallyProved = "partially proved" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
67 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
68 |
fun pretty_vc_name (name, proved) = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
69 |
Pretty.str (name ^ " (" ^ string_of_state proved ^ ")") |
33419 | 70 |
in |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
71 |
Boogie_VCs.state_of thy |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
72 |
|> write_list "Boogie verification conditions:" pretty_vc_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
73 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
74 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
75 |
fun boogie_status_vc (full, vc_name) thy = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
76 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
77 |
fun pretty tag s = s ^ " (" ^ tag ^ ")" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
78 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
79 |
val (ps, us) = Boogie_VCs.state_of_vc thy vc_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
80 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
81 |
if full |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
82 |
then write_list ("Assertions of Boogie verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
83 |
quote vc_name ^ ":") Pretty.str (sort fast_string_ord |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
84 |
(map (pretty "proved") ps @ map (pretty "not proved") us)) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
85 |
else write_list ("Unproved assertions of Boogie verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
86 |
quote vc_name ^ ":") Pretty.str (sort fast_string_ord us) |
33419 | 87 |
end |
88 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
89 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
90 |
local |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
91 |
fun trying s = tracing ("Trying " ^ s ^ " ...") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
92 |
fun success_on s = tracing ("Succeeded on " ^ s ^ ".") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
93 |
fun failure_on s c = tracing ("Failed on " ^ s ^ c) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
94 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
95 |
fun string_of_asserts goal = space_implode ", " (Boogie_VCs.names_of goal) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
96 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
97 |
fun string_of_path (i, n) = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
98 |
"path " ^ string_of_int i ^ " of " ^ string_of_int n |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
99 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
100 |
fun itemize_paths ps = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
101 |
let val n = length ps |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
102 |
in fst (fold_map (fn p => fn i => (((i, n), p), i+1)) ps 1) end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
103 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
104 |
fun par_map f = flat o Par_List.map f |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
105 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
106 |
fun divide f goal = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
107 |
let val n = Boogie_VCs.size_of goal |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
108 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
109 |
if n = 1 then Boogie_VCs.names_of goal |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
110 |
else |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
111 |
let val (goal1, goal2) = Boogie_VCs.split_path (n div 2) goal |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
112 |
in par_map f [goal1, goal2] end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
113 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
114 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
115 |
fun prove thy meth (_, goal) = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
116 |
ProofContext.init thy |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
117 |
|> Proof.theorem_i NONE (K I) [[(goal, [])]] |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
118 |
|> Proof.apply meth |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
119 |
|> Seq.hd |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
120 |
|> Proof.global_done_proof |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
121 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
122 |
fun boogie_narrow_vc ((timeout, vc_name), meth) thy = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
123 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
124 |
val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
125 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
126 |
fun try_goal (tag, split_tag) split goal = (trying tag; |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
127 |
(case try tp goal of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
128 |
SOME _ => (success_on tag; []) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
129 |
| NONE => (failure_on tag split_tag; split goal))) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
130 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
131 |
fun group_goal goal = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
132 |
try_goal (string_of_asserts goal, |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
133 |
if Boogie_VCs.size_of goal = 1 then "." else ", further splitting ...") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
134 |
(divide group_goal) goal |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
135 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
136 |
fun path_goal p = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
137 |
try_goal (string_of_path p, ", splitting into assertions ...") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
138 |
(divide group_goal) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
139 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
140 |
val full_goal = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
141 |
try_goal ("full goal", ", splitting into paths ...") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
142 |
(par_map (uncurry path_goal) o itemize_paths o Boogie_VCs.paths_of) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
143 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
144 |
val unsolved = full_goal (get_vc thy vc_name) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
145 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
146 |
if null unsolved |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
147 |
then writeln ("Completely solved Boogie verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
148 |
quote vc_name ^ ".") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
149 |
else write_list ("Unsolved assertions of Boogie verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
150 |
quote vc_name ^ ":") Pretty.str (sort fast_string_ord unsolved) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
151 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
152 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
153 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
154 |
|
33419 | 155 |
|
156 |
fun boogie_end thy = |
|
157 |
let |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
158 |
fun not_proved (_, Boogie_VCs.Proved) = NONE |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
159 |
| not_proved (name, _) = SOME name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
160 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
161 |
val unproved = map_filter not_proved (Boogie_VCs.state_of thy) |
33419 | 162 |
in |
163 |
if null unproved then Boogie_VCs.close thy |
|
164 |
else error (Pretty.string_of (Pretty.big_list |
|
165 |
"The following verification conditions have not been proved:" |
|
166 |
(map Pretty.str unproved))) |
|
167 |
end |
|
168 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
169 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
170 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
171 |
(* syntax and setup *) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
172 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
173 |
fun scan_val n f = Args.$$$ n -- Args.colon |-- f |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
174 |
fun scan_arg f = Args.parens f |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
175 |
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n) >> K true) false |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
176 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
177 |
|
33419 | 178 |
val _ = |
179 |
OuterSyntax.command "boogie_open" |
|
180 |
"Open a new Boogie environment and load a Boogie-generated .b2i file." |
|
181 |
OuterKeyword.thy_decl |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
182 |
(scan_opt "quiet" -- OuterParse.name >> (Toplevel.theory o boogie_load)) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
183 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
184 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
185 |
val vc_name = OuterParse.name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
186 |
val vc_opts = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
187 |
scan_arg (scan_val "only" (Scan.repeat1 OuterParse.name)) >> VC_only || |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
188 |
scan_opt "paths" >> VC_full |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
189 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
190 |
fun vc_cmd f = Toplevel.print o Toplevel.local_theory_to_proof NONE f |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
191 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
192 |
val _ = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
193 |
OuterSyntax.command "boogie_vc" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
194 |
"Enter into proof mode for a specific verification condition." |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
195 |
OuterKeyword.thy_goal |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
196 |
(vc_opts -- vc_name >> (vc_cmd o boogie_vc)) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
197 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
198 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
199 |
val default_timeout = 5 |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
200 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
201 |
val status_narrow_vc = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
202 |
scan_arg (Args.$$$ "narrow" |-- |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
203 |
Scan.optional (scan_val "timeout" OuterParse.nat) default_timeout) -- |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
204 |
vc_name -- |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
205 |
scan_arg (scan_val "try" Method.parse) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
206 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
207 |
val status_vc_opts = scan_opt "full" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
208 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
209 |
fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state => |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
210 |
f (Toplevel.theory_of state)) |
33419 | 211 |
|
212 |
val _ = |
|
213 |
OuterSyntax.improper_command "boogie_status" |
|
214 |
"Show the name and state of all loaded verification conditions." |
|
215 |
OuterKeyword.diag |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
216 |
(status_narrow_vc >> (status_cmd o boogie_narrow_vc) || |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
217 |
status_vc_opts -- vc_name >> (status_cmd o boogie_status_vc) || |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
218 |
Scan.succeed (status_cmd boogie_status)) |
33419 | 219 |
|
220 |
||
221 |
val _ = |
|
222 |
OuterSyntax.command "boogie_end" |
|
223 |
"Close the current Boogie environment." |
|
224 |
OuterKeyword.thy_decl |
|
225 |
(Scan.succeed (Toplevel.theory boogie_end)) |
|
226 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
227 |
|
33419 | 228 |
val setup = Theory.at_end (fn thy => |
229 |
let |
|
230 |
val _ = Boogie_VCs.is_closed thy |
|
231 |
orelse error ("Found the end of the theory, " ^ |
|
232 |
"but the last Boogie environment is still open.") |
|
233 |
in NONE end) |
|
234 |
||
235 |
end |