author | wenzelm |
Sat, 16 Apr 2011 16:15:37 +0200 | |
changeset 42361 | 23f352990944 |
parent 42003 | 6e45dc518ebb |
child 43702 | 24fb44c1086a |
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 |
|
35125
acace7e30357
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
boehmes
parents:
34181
diff
changeset
|
17 |
fun boogie_open ((quiet, base_name), offsets) thy = |
33419 | 18 |
let |
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
38756
diff
changeset
|
19 |
val ext = "b2i" |
40580
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40540
diff
changeset
|
20 |
fun check_ext path = snd (Path.split_ext path) = ext orelse |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41887
diff
changeset
|
21 |
error ("Bad file ending of file " ^ Path.print path ^ ", " ^ |
40580
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40540
diff
changeset
|
22 |
"expected file ending " ^ quote ext) |
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40540
diff
changeset
|
23 |
|
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40540
diff
changeset
|
24 |
val base_path = Path.explode base_name |> tap check_ext |
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
25 |
val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path |
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
38756
diff
changeset
|
26 |
|
33419 | 27 |
val _ = Boogie_VCs.is_closed thy orelse |
28 |
error ("Found the beginning of a new Boogie environment, " ^ |
|
29 |
"but another Boogie environment is still open.") |
|
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
38756
diff
changeset
|
30 |
in |
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
38756
diff
changeset
|
31 |
thy |
40540 | 32 |
|> Boogie_Loader.load_b2i (not quiet) offsets full_path |
33 |
|> Thy_Load.provide_file base_path |
|
40514
db5f14910dce
let the theory formally depend on the Boogie output
boehmes
parents:
38756
diff
changeset
|
34 |
end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
35 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
36 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
37 |
datatype vc_opts = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
38 |
VC_Complete | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
39 |
VC_Take of int list * (bool * string list) option | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
40 |
VC_Only of string list | |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
41 |
VC_Without of string list | |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
42 |
VC_Examine of string list | |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
43 |
VC_Single of string |
34068
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 |
fun get_vc thy vc_name = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
46 |
(case Boogie_VCs.lookup thy vc_name of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
47 |
SOME vc => vc |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
48 |
| NONE => |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
49 |
(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
|
50 |
SOME Boogie_VCs.Proved => error ("The verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
51 |
quote vc_name ^ " has already been proved.") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
52 |
| _ => error ("There is no verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
53 |
quote vc_name ^ "."))) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
54 |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
55 |
local |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
56 |
fun split_goal t = |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
57 |
(case Boogie_Tactics.split t of |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
58 |
[tp] => tp |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
59 |
| _ => error "Multiple goals.") |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
60 |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
61 |
fun single_prep t = |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
62 |
let |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
63 |
val (us, u) = split_goal t |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
64 |
val assms = [((@{binding vc_trace}, []), map (rpair []) us)] |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
65 |
in |
42361 | 66 |
pair [u] o snd o Proof_Context.add_assms_i Assumption.assume_export assms |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
67 |
end |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
68 |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
69 |
fun single_prove goal ctxt thm = |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
70 |
Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL ( |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
71 |
Boogie_Tactics.split_tac |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
72 |
THEN' Boogie_Tactics.drop_assert_at_tac |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
73 |
THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context)) |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
74 |
in |
35864 | 75 |
fun boogie_vc (vc_name, vc_opts) thy = |
34068
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 |
val vc = get_vc thy vc_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
78 |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
79 |
fun extract vc l = |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
80 |
(case Boogie_VCs.extract vc l of |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
81 |
SOME vc' => vc' |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
82 |
| NONE => error ("There is no assertion to be proved with label " ^ |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
83 |
quote l ^ ".")) |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
84 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
85 |
val vcs = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
86 |
(case vc_opts of |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
87 |
VC_Complete => [vc] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
88 |
| VC_Take (ps, NONE) => [Boogie_VCs.paths_and ps [] vc] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
89 |
| VC_Take (ps, SOME (true, ls)) => [Boogie_VCs.paths_and ps ls vc] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
90 |
| VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
91 |
| VC_Only ls => [Boogie_VCs.only ls vc] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
92 |
| VC_Without ls => [Boogie_VCs.without ls vc] |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
93 |
| VC_Examine ls => map (extract vc) ls |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
94 |
| VC_Single l => [extract vc l]) |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
95 |
val ts = map Boogie_VCs.prop_of_vc vcs |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
96 |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
97 |
val (prepare, finish) = |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
98 |
(case vc_opts of |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
99 |
VC_Single _ => (single_prep (hd ts), single_prove (hd ts)) |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
100 |
| _ => (pair ts, K I)) |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
101 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
102 |
val discharge = fold (Boogie_VCs.discharge o pair vc_name) |
42361 | 103 |
fun after_qed [thms] = Proof_Context.background_theory (discharge (vcs ~~ thms)) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
104 |
| after_qed _ = I |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
105 |
in |
42361 | 106 |
Proof_Context.init_global thy |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
107 |
|> fold Variable.auto_fixes ts |
35864 | 108 |
|> (fn ctxt1 => ctxt1 |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
109 |
|> prepare |
35864 | 110 |
|-> (fn us => fn ctxt2 => ctxt2 |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35864
diff
changeset
|
111 |
|> Proof.theorem NONE (fn thmss => fn ctxt => |
42361 | 112 |
let val export = map (finish ctxt1) o Proof_Context.export ctxt ctxt2 |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
113 |
in after_qed (map export thmss) ctxt end) [map (rpair []) us])) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
114 |
end |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
115 |
end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
116 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
117 |
fun write_list head = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40580
diff
changeset
|
118 |
map Pretty.str o sort (dict_ord string_ord o pairself raw_explode) #> |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
119 |
Pretty.writeln o Pretty.big_list head |
33419 | 120 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
121 |
fun parens s = "(" ^ s ^ ")" |
34079 | 122 |
|
33419 | 123 |
fun boogie_status thy = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
124 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
125 |
fun string_of_state Boogie_VCs.Proved = "proved" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
126 |
| string_of_state Boogie_VCs.NotProved = "not proved" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
127 |
| string_of_state Boogie_VCs.PartiallyProved = "partially proved" |
33419 | 128 |
in |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
129 |
Boogie_VCs.state_of thy |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
130 |
|> map (fn (name, proved) => name ^ " " ^ parens (string_of_state proved)) |
34080
a36d80e4e42e
also sort verification conditions before printing
boehmes
parents:
34079
diff
changeset
|
131 |
|> write_list "Boogie verification conditions:" |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
132 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
133 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
134 |
fun boogie_status_vc full vc_name thy = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
135 |
let |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
136 |
fun pretty tag s = s ^ " " ^ parens tag |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
137 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
138 |
val (not_proved, proved) = Boogie_VCs.state_of_vc thy vc_name |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
139 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
140 |
if full |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
141 |
then write_list ("Assertions of Boogie verification condition " ^ |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
142 |
quote vc_name ^ ":") |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
143 |
(map (pretty "proved") proved @ map (pretty "not proved") not_proved) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
144 |
else write_list ("Unproved assertions of Boogie verification condition " ^ |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
145 |
quote vc_name ^ ":") not_proved |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
146 |
end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
147 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
148 |
fun boogie_status_vc_paths full vc_name thy = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
149 |
let |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
150 |
fun labels ls = Pretty.blk (0, Pretty.breaks (map Pretty.str ls)) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
151 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
152 |
fun pp (i, ns) = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
153 |
if full |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
154 |
then |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
155 |
[Pretty.big_list ("Path " ^ string_of_int (i+1) ^ ":") |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
156 |
[labels (map (fn (n, true) => n | (n, _) => parens n) ns)]] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
157 |
else |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
158 |
let val ns' = map_filter (fn (n, true) => SOME n | _ => NONE) ns |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
159 |
in |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
160 |
if null ns' then [] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
161 |
else |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
162 |
[Pretty.big_list ("Unproved assertions of path " ^ |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
163 |
string_of_int (i+1) ^ ":") [labels ns']] |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
164 |
end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
165 |
in |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
166 |
Pretty.writeln |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
167 |
(Pretty.big_list |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
168 |
("Paths of Boogie verification condition " ^ quote vc_name ^ ":") |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
169 |
(flat (map_index pp (Boogie_VCs.path_names_of (get_vc thy vc_name))))) |
33419 | 170 |
end |
171 |
||
34068
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 |
local |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
174 |
fun trying s = tracing ("Trying " ^ s ^ " ...") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
175 |
fun success_on s = tracing ("Succeeded on " ^ s ^ ".") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
176 |
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
|
177 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
178 |
fun string_of_asserts vc = space_implode ", " (fst (Boogie_VCs.names_of vc)) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
179 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
180 |
fun string_of_path (i, n) = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
181 |
"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
|
182 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
183 |
fun itemize_paths ps = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
184 |
let val n = length ps |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
185 |
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
|
186 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
187 |
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
|
188 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
189 |
fun divide f vc = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
190 |
let val n = Boogie_VCs.size_of vc |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
191 |
in |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
192 |
if n <= 1 then fst (Boogie_VCs.names_of vc) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
193 |
else |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
194 |
let val (vc1, vc2) = the (Boogie_VCs.split_path (n div 2) vc) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
195 |
in par_map f [vc1, vc2] end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
196 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
197 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
198 |
fun prove thy meth vc = |
42361 | 199 |
Proof_Context.init_global thy |
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35864
diff
changeset
|
200 |
|> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]] |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
201 |
|> Proof.apply meth |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
202 |
|> Seq.hd |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
203 |
|> Proof.global_done_proof |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
204 |
in |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
205 |
fun boogie_narrow_vc (quick, timeout) vc_name meth thy = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
206 |
let |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
207 |
fun tp t = TimeLimit.timeLimit (Time.fromSeconds t) (prove thy meth) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
208 |
|
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
209 |
fun try_vc t (tag, split_tag) split vc = (trying tag; |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
210 |
(case try (tp t) vc of |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
211 |
SOME _ => (success_on tag; []) |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
212 |
| NONE => (failure_on tag split_tag; split vc))) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
213 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
214 |
fun some_asserts vc = |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
215 |
let |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
216 |
val (t, sep) = if Boogie_VCs.size_of vc = 1 then (timeout, ".") |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
217 |
else (quick, ", further splitting ...") |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
218 |
in try_vc t (string_of_asserts vc, sep) (divide some_asserts) vc end |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
219 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
220 |
fun single_path p = |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
221 |
try_vc quick (string_of_path p, ", splitting into assertions ...") |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
222 |
(divide some_asserts) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
223 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
224 |
val complete_vc = |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
225 |
try_vc quick ("full goal", ", splitting into paths ...") |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
226 |
(par_map (uncurry single_path) o itemize_paths o Boogie_VCs.paths_of) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
227 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
228 |
val unsolved = complete_vc (get_vc thy vc_name) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
229 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
230 |
if null unsolved |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
231 |
then writeln ("Completely solved Boogie verification condition " ^ |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
232 |
quote vc_name ^ ".") |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
233 |
else write_list ("Unsolved assertions of Boogie verification condition " ^ |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
234 |
quote vc_name ^ ":") unsolved |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
235 |
end |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
236 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
237 |
fun boogie_scan_vc timeout vc_name meth thy = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
238 |
let |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
239 |
val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
240 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
241 |
val vc = get_vc thy vc_name |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
242 |
fun prove_assert name = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
243 |
(trying name; tp (the (Boogie_VCs.extract vc name))) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
244 |
val find_first_failure = find_first (is_none o try prove_assert) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
245 |
in |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
246 |
(case find_first_failure (fst (Boogie_VCs.names_of vc)) of |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
247 |
SOME name => writeln ("failed on " ^ quote name) |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
248 |
| NONE => writeln "succeeded") |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
249 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
250 |
end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
251 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
252 |
|
33419 | 253 |
|
254 |
fun boogie_end thy = |
|
255 |
let |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
256 |
fun not_proved (_, Boogie_VCs.Proved) = NONE |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
257 |
| not_proved (name, _) = SOME name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
258 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
259 |
val unproved = map_filter not_proved (Boogie_VCs.state_of thy) |
33419 | 260 |
in |
261 |
if null unproved then Boogie_VCs.close thy |
|
262 |
else error (Pretty.string_of (Pretty.big_list |
|
263 |
"The following verification conditions have not been proved:" |
|
264 |
(map Pretty.str unproved))) |
|
265 |
end |
|
266 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
267 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
268 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
269 |
(* syntax and setup *) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
270 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
271 |
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
|
272 |
fun scan_arg f = Args.parens f |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
273 |
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
274 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
275 |
val vc_offsets = Scan.optional (Args.bracks (Parse.list1 |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
276 |
(Parse.string --| Args.colon -- Parse.nat))) [] |
35125
acace7e30357
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
boehmes
parents:
34181
diff
changeset
|
277 |
|
33419 | 278 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
279 |
Outer_Syntax.command "boogie_open" |
37944 | 280 |
"open a new Boogie environment and load a Boogie-generated .b2i file" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
281 |
Keyword.thy_decl |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
282 |
(scan_opt "quiet" -- Parse.name -- vc_offsets >> |
35125
acace7e30357
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
boehmes
parents:
34181
diff
changeset
|
283 |
(Toplevel.theory o boogie_open)) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
284 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
285 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
286 |
val vc_name = Parse.name |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
287 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
288 |
val vc_label = Parse.name |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
289 |
val vc_labels = Scan.repeat1 vc_label |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
290 |
|
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
291 |
val vc_paths = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
292 |
Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) || |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
293 |
Parse.nat >> single |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
294 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
295 |
val vc_opts = |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
296 |
scan_arg |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
297 |
(scan_val "assertion" vc_label >> VC_Single || |
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
298 |
scan_val "examine" vc_labels >> VC_Examine || |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
299 |
scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option ( |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
300 |
scan_val "without" vc_labels >> pair false || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
301 |
scan_val "and_also" vc_labels >> pair true) >> VC_Take) || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
302 |
scan_val "only" vc_labels >> VC_Only || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
303 |
scan_val "without" vc_labels >> VC_Without) || |
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
35323
diff
changeset
|
304 |
Scan.succeed VC_Complete |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
305 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
306 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
307 |
Outer_Syntax.command "boogie_vc" |
37944 | 308 |
"enter into proof mode for a specific verification condition" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
309 |
Keyword.thy_goal |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
310 |
(vc_name -- vc_opts >> (fn args => |
35864 | 311 |
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args)))) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
312 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
313 |
|
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
314 |
val quick_timeout = 5 |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
315 |
val default_timeout = 20 |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
316 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
317 |
fun timeout name = Scan.optional (scan_val name Parse.nat) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
318 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
319 |
val status_test = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
320 |
scan_arg ( |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
321 |
Args.$$$ "scan" |-- timeout "timeout" quick_timeout >> boogie_scan_vc || |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
322 |
Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout -- |
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
323 |
timeout "final_timeout" default_timeout >> boogie_narrow_vc) -- |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
324 |
vc_name -- Method.parse >> |
35323
259931828ecc
separated narrowing timeouts for intermediate and final steps
boehmes
parents:
35125
diff
changeset
|
325 |
(fn ((f, vc_name), meth) => f vc_name meth) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
326 |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
327 |
val status_vc = |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
328 |
(scan_arg |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
329 |
(Args.$$$ "full" |-- |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
330 |
(Args.$$$ "paths" >> K (boogie_status_vc_paths true) || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
331 |
Scan.succeed (boogie_status_vc true)) || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
332 |
Args.$$$ "paths" >> K (boogie_status_vc_paths false)) || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
333 |
Scan.succeed (boogie_status_vc false)) -- |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
334 |
vc_name >> (fn (f, vc_name) => f vc_name) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
335 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
336 |
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
|
337 |
f (Toplevel.theory_of state)) |
33419 | 338 |
|
339 |
val _ = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
340 |
Outer_Syntax.improper_command "boogie_status" |
37944 | 341 |
"show the name and state of all loaded verification conditions" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
342 |
Keyword.diag |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
343 |
(status_test >> status_cmd || |
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34080
diff
changeset
|
344 |
status_vc >> status_cmd || |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
345 |
Scan.succeed (status_cmd boogie_status)) |
33419 | 346 |
|
347 |
||
348 |
val _ = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
349 |
Outer_Syntax.command "boogie_end" |
37944 | 350 |
"close the current Boogie environment" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset
|
351 |
Keyword.thy_decl |
33419 | 352 |
(Scan.succeed (Toplevel.theory boogie_end)) |
353 |
||
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
33671
diff
changeset
|
354 |
|
33419 | 355 |
val setup = Theory.at_end (fn thy => |
356 |
let |
|
357 |
val _ = Boogie_VCs.is_closed thy |
|
358 |
orelse error ("Found the end of the theory, " ^ |
|
359 |
"but the last Boogie environment is still open.") |
|
360 |
in NONE end) |
|
361 |
||
362 |
end |