author | boehmes |
Fri, 13 Nov 2009 15:06:19 +0100 | |
changeset 33661 | 31a129cc0d10 |
parent 33497 | 39c9d0785911 |
child 33893 | 24b648ea4834 |
permissions | -rw-r--r-- |
33419 | 1 |
(* Title: HOL/Boogie/Tools/boogie_loader.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Loading and interpreting Boogie-generated files. |
|
5 |
*) |
|
6 |
||
7 |
signature BOOGIE_LOADER = |
|
8 |
sig |
|
9 |
val load_b2i: bool -> Path.T -> theory -> theory |
|
10 |
end |
|
11 |
||
12 |
structure Boogie_Loader: BOOGIE_LOADER = |
|
13 |
struct |
|
14 |
||
15 |
fun log verbose text args thy = |
|
16 |
if verbose |
|
17 |
then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); thy) |
|
18 |
else thy |
|
19 |
||
20 |
val isabelle_name = |
|
21 |
let |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
22 |
fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else |
33419 | 23 |
(case s of |
24 |
"." => "_o_" |
|
25 |
| "_" => "_n_" |
|
26 |
| "$" => "_S_" |
|
27 |
| "@" => "_G_" |
|
28 |
| "#" => "_H_" |
|
29 |
| "^" => "_T_" |
|
30 |
| _ => ("_" ^ string_of_int (ord s) ^ "_")) |
|
31 |
in prefix "b_" o translate_string purge end |
|
32 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
33 |
val short_name = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
34 |
translate_string (fn s => if Symbol.is_letdig s then s else "") |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
35 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
36 |
fun label_name line col = "L_" ^ string_of_int line ^ "_" ^ string_of_int col |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
37 |
|
33419 | 38 |
datatype attribute_value = StringValue of string | TermValue of Term.term |
39 |
||
40 |
||
41 |
||
42 |
local |
|
43 |
fun lookup_type_name thy name arity = |
|
44 |
let val intern = Sign.intern_type thy name |
|
45 |
in |
|
46 |
if Sign.declared_tyname thy intern |
|
47 |
then |
|
48 |
if Sign.arity_number thy intern = arity then SOME intern |
|
49 |
else error ("Boogie: type already declared with different arity: " ^ |
|
50 |
quote name) |
|
51 |
else NONE |
|
52 |
end |
|
53 |
||
54 |
fun declare (name, arity) thy = |
|
55 |
let val isa_name = isabelle_name name |
|
56 |
in |
|
57 |
(case lookup_type_name thy isa_name arity of |
|
58 |
SOME type_name => ((type_name, false), thy) |
|
59 |
| NONE => |
|
60 |
let |
|
61 |
val args = Name.variant_list [] (replicate arity "'") |
|
62 |
val (T, thy') = |
|
63 |
ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy |
|
64 |
val type_name = fst (Term.dest_Type T) |
|
65 |
in ((type_name, true), thy') end) |
|
66 |
end |
|
67 |
||
68 |
fun type_names ((name, _), (new_name, new)) = |
|
69 |
if new then SOME (new_name ^ " (was " ^ name ^ ")") else NONE |
|
70 |
in |
|
71 |
fun declare_types verbose tys = |
|
72 |
fold_map declare tys #-> (fn tds => |
|
73 |
log verbose "Declared types:" (map_filter type_names (tys ~~ tds)) #> |
|
74 |
rpair (Symtab.make (map fst tys ~~ map fst tds))) |
|
75 |
end |
|
76 |
||
77 |
||
78 |
||
79 |
local |
|
80 |
val quote_mixfix = |
|
81 |
Symbol.explode #> map |
|
82 |
(fn "_" => "'_" |
|
83 |
| "(" => "'(" |
|
84 |
| ")" => "')" |
|
85 |
| "/" => "'/" |
|
86 |
| s => s) #> |
|
87 |
implode |
|
88 |
||
89 |
fun mk_syntax name i = |
|
90 |
let |
|
91 |
val syn = quote_mixfix name |
|
92 |
val args = concat (separate ",/ " (replicate i "_")) |
|
93 |
in |
|
94 |
if i = 0 then Mixfix (syn, [], 1000) |
|
95 |
else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) |
|
96 |
end |
|
97 |
||
98 |
fun process_attributes T = |
|
99 |
let |
|
100 |
fun const name = SOME (Const (name, T)) |
|
101 |
||
102 |
fun choose builtin = |
|
103 |
(case builtin of |
|
104 |
"bvnot" => const @{const_name z3_bvnot} |
|
105 |
| "bvand" => const @{const_name z3_bvand} |
|
106 |
| "bvor" => const @{const_name z3_bvor} |
|
107 |
| "bvxor" => const @{const_name z3_bvxor} |
|
108 |
| "bvadd" => const @{const_name z3_bvadd} |
|
109 |
| "bvneg" => const @{const_name z3_bvneg} |
|
110 |
| "bvsub" => const @{const_name z3_bvsub} |
|
111 |
| "bvmul" => const @{const_name z3_bvmul} |
|
112 |
| "bvudiv" => const @{const_name z3_bvudiv} |
|
113 |
| "bvurem" => const @{const_name z3_bvurem} |
|
114 |
| "bvsdiv" => const @{const_name z3_bvsdiv} |
|
115 |
| "bvsrem" => const @{const_name z3_bvsrem} |
|
116 |
| "bvshl" => const @{const_name z3_bvshl} |
|
117 |
| "bvlshr" => const @{const_name z3_bvlshr} |
|
118 |
| "bvashr" => const @{const_name z3_bvashr} |
|
119 |
| "bvult" => const @{const_name z3_bvult} |
|
120 |
| "bvule" => const @{const_name z3_bvule} |
|
121 |
| "bvugt" => const @{const_name z3_bvugt} |
|
122 |
| "bvuge" => const @{const_name z3_bvuge} |
|
123 |
| "bvslt" => const @{const_name z3_bvslt} |
|
124 |
| "bvsle" => const @{const_name z3_bvsle} |
|
125 |
| "bvsgt" => const @{const_name z3_bvsgt} |
|
126 |
| "bvsge" => const @{const_name z3_bvsge} |
|
127 |
| "sign_extend" => const @{const_name z3_sign_extend} |
|
128 |
| _ => NONE) |
|
129 |
||
130 |
fun is_builtin att = |
|
131 |
(case att of |
|
132 |
("bvbuiltin", [StringValue builtin]) => choose builtin |
|
133 |
| ("bvint", [StringValue "ITE"]) => const @{const_name If} |
|
134 |
| _ => NONE) |
|
135 |
in get_first is_builtin end |
|
136 |
||
137 |
fun lookup_const thy name T = |
|
33465 | 138 |
let val intern = Sign.intern_const thy name |
33419 | 139 |
in |
140 |
if Sign.declared_const thy intern |
|
141 |
then |
|
33465 | 142 |
if Sign.typ_instance thy (T, Sign.the_const_type thy intern) |
33419 | 143 |
then SOME (Const (intern, T)) |
144 |
else error ("Boogie: function already declared with different type: " ^ |
|
145 |
quote name) |
|
146 |
else NONE |
|
147 |
end |
|
148 |
||
149 |
fun declare (name, ((Ts, T), atts)) thy = |
|
150 |
let val isa_name = isabelle_name name and U = Ts ---> T |
|
151 |
in |
|
152 |
(case lookup_const thy isa_name U of |
|
153 |
SOME t => (((name, t), false), thy) |
|
154 |
| NONE => |
|
155 |
(case process_attributes U atts of |
|
156 |
SOME t => (((name, t), false), thy) |
|
157 |
| NONE => |
|
158 |
thy |
|
159 |
|> Sign.declare_const ((Binding.name isa_name, U), |
|
160 |
mk_syntax name (length Ts)) |
|
161 |
|> apfst (rpair true o pair name))) |
|
162 |
end |
|
163 |
||
164 |
fun const_names ((name, _), ((_, t), new)) = |
|
165 |
if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE |
|
166 |
in |
|
167 |
fun declare_functions verbose fns = |
|
168 |
fold_map declare fns #-> (fn fds => |
|
169 |
log verbose "Declared constants:" (map_filter const_names (fns ~~ fds)) #> |
|
170 |
rpair (Symtab.make (map fst fds))) |
|
171 |
end |
|
172 |
||
173 |
||
174 |
||
175 |
local |
|
176 |
fun name_axioms axs = |
|
177 |
let fun mk_name idx = "axiom_" ^ string_of_int (idx + 1) |
|
178 |
in map_index (fn (idx, t) => (mk_name idx, HOLogic.mk_Trueprop t)) axs end |
|
179 |
||
180 |
fun only_new_boogie_axioms thy = |
|
181 |
let val baxs = map Thm.prop_of (Boogie_Axioms.get (ProofContext.init thy)) |
|
182 |
in filter_out (member (op aconv) baxs o snd) end |
|
183 |
in |
|
184 |
fun add_axioms verbose axs thy = |
|
185 |
let val axs' = only_new_boogie_axioms thy (name_axioms axs) |
|
186 |
in |
|
187 |
thy |
|
188 |
|> PureThy.add_axioms (map (rpair [] o apfst Binding.name) axs') |
|
189 |
|-> Context.theory_map o fold Boogie_Axioms.add_thm |
|
190 |
|> log verbose "The following axioms were added:" (map fst axs') |
|
191 |
|> Context.theory_map (fn context => fold Split_VC_SMT_Rules.add_thm |
|
192 |
(Boogie_Axioms.get (Context.proof_of context)) context) |
|
193 |
end |
|
194 |
end |
|
195 |
||
196 |
||
197 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
198 |
local |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
199 |
fun burrow_distinct eq f xs = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
200 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
201 |
val ys = distinct eq xs |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
202 |
val tab = ys ~~ f ys |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
203 |
in map (the o AList.lookup eq tab) xs end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
204 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
205 |
fun indexed names = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
206 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
207 |
val dup = member (op =) (duplicates (op =) (map fst names)) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
208 |
fun make_name (n, i) = n ^ (if dup n then "_" ^ string_of_int i else "") |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
209 |
in map make_name names end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
210 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
211 |
fun rename idx_names = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
212 |
idx_names |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
213 |
|> burrow_fst (burrow_distinct (op =) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
214 |
(map short_name #> ` (duplicates (op =)) #-> Name.variant_list)) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
215 |
|> indexed |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
216 |
in |
33419 | 217 |
fun add_vcs verbose vcs thy = |
218 |
let |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
219 |
val vcs' = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
220 |
vcs |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
221 |
|> burrow_fst rename |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
222 |
|> map (apsnd HOLogic.mk_Trueprop) |
33419 | 223 |
in |
224 |
thy |
|
225 |
|> Boogie_VCs.set vcs' |
|
226 |
|> log verbose "The following verification conditions were loaded:" |
|
227 |
(map fst vcs') |
|
228 |
end |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
229 |
end |
33419 | 230 |
|
231 |
||
232 |
||
233 |
local |
|
234 |
fun mk_bitT i T = |
|
235 |
if i = 0 |
|
236 |
then Type (@{type_name "Numeral_Type.bit0"}, [T]) |
|
237 |
else Type (@{type_name "Numeral_Type.bit1"}, [T]) |
|
238 |
||
239 |
fun mk_binT size = |
|
240 |
if size = 0 then @{typ "Numeral_Type.num0"} |
|
241 |
else if size = 1 then @{typ "Numeral_Type.num1"} |
|
242 |
else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end |
|
243 |
in |
|
244 |
fun mk_wordT size = |
|
245 |
if size >= 0 then Type (@{type_name "word"}, [mk_binT size]) |
|
246 |
else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], []) |
|
247 |
end |
|
248 |
||
249 |
local |
|
250 |
fun dest_binT T = |
|
251 |
(case T of |
|
252 |
Type (@{type_name "Numeral_Type.num0"}, _) => 0 |
|
253 |
| Type (@{type_name "Numeral_Type.num1"}, _) => 1 |
|
254 |
| Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T |
|
255 |
| Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T |
|
256 |
| _ => raise TYPE ("dest_binT", [T], [])) |
|
257 |
in |
|
258 |
val dest_wordT = (fn |
|
259 |
Type (@{type_name "word"}, [T]) => dest_binT T |
|
260 |
| T => raise TYPE ("dest_wordT", [T], [])) |
|
261 |
end |
|
262 |
||
263 |
fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T]) |
|
264 |
||
265 |
||
266 |
||
267 |
datatype token = Token of string | Newline | EOF |
|
268 |
||
269 |
fun tokenize path = |
|
270 |
let |
|
271 |
fun blank c = (c = #" " orelse c = #"\t" orelse c = #"\n" orelse c = #"\r") |
|
272 |
fun split line (i, tss) = (i + 1, |
|
273 |
map (pair i) (map Token (String.tokens blank line) @ [Newline]) :: tss) |
|
274 |
in apsnd (flat o rev) (File.fold_lines split path (1, [])) end |
|
275 |
||
276 |
fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false) |
|
277 |
||
278 |
fun scan_err msg [] = "Boogie (at end of input): " ^ msg |
|
279 |
| scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^ |
|
280 |
msg |
|
281 |
||
282 |
fun scan_fail msg = Scan.fail_with (scan_err msg) |
|
283 |
||
284 |
fun finite scan path = |
|
285 |
let val (i, ts) = tokenize path |
|
286 |
in |
|
287 |
(case Scan.error (Scan.finite (stopper i) scan) ts of |
|
288 |
(x, []) => x |
|
289 |
| (_, ts) => error (scan_err "unparsed input" ts)) |
|
290 |
end |
|
291 |
||
292 |
fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE) |
|
293 |
||
294 |
fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false) |
|
33497 | 295 |
fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st |
296 |
fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st |
|
33419 | 297 |
|
298 |
fun scan_line key scan = |
|
299 |
$$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false) |
|
300 |
fun scan_line' key = scan_line key (Scan.succeed ()) |
|
301 |
||
302 |
fun scan_count scan i = |
|
303 |
if i > 0 then scan ::: scan_count scan (i - 1) else Scan.succeed [] |
|
304 |
||
305 |
fun scan_lookup kind tab key = |
|
306 |
(case Symtab.lookup tab key of |
|
307 |
SOME value => Scan.succeed value |
|
308 |
| NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key)) |
|
309 |
||
310 |
fun typ tds = |
|
311 |
let |
|
312 |
fun tp st = |
|
313 |
(scan_line' "bool" >> K @{typ bool} || |
|
314 |
scan_line' "int" >> K @{typ int} || |
|
315 |
scan_line "bv" num >> mk_wordT || |
|
316 |
scan_line "type-con" (str -- num) :|-- (fn (name, arity) => |
|
317 |
scan_lookup "type constructor" tds name -- scan_count tp arity >> |
|
318 |
Type) || |
|
319 |
scan_line "array" num :|-- (fn arity => |
|
320 |
scan_count tp (arity - 1) -- tp >> mk_arrayT) || |
|
321 |
scan_fail "illegal type") st |
|
322 |
in tp end |
|
323 |
||
324 |
local |
|
325 |
fun mk_nary _ t [] = t |
|
33661 | 326 |
| mk_nary f _ ts = uncurry (fold_rev f) (split_last ts) |
33419 | 327 |
|
328 |
fun mk_distinct T ts = |
|
329 |
Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ |
|
330 |
HOLogic.mk_list T ts |
|
331 |
||
332 |
fun quant name f = scan_line name (num -- num -- num) >> pair f |
|
333 |
val quants = |
|
334 |
quant "forall" HOLogic.all_const || |
|
335 |
quant "exists" HOLogic.exists_const || |
|
336 |
scan_fail "illegal quantifier kind" |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
337 |
fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t) |
33419 | 338 |
|
339 |
val patternT = @{typ pattern} |
|
340 |
fun mk_pattern _ [] = raise TERM ("mk_pattern", []) |
|
341 |
| mk_pattern n [t] = Const (n, Term.fastype_of t --> patternT) $ t |
|
342 |
| mk_pattern n (t :: ts) = |
|
343 |
let val T = patternT --> Term.fastype_of t --> patternT |
|
344 |
in Const (@{const_name andpat}, T) $ mk_pattern n ts $ t end |
|
345 |
fun patt n c scan = |
|
346 |
scan_line n num :|-- scan_count scan >> (mk_pattern c) |
|
347 |
fun pattern scan = |
|
348 |
patt "pat" @{const_name pat} scan || |
|
349 |
patt "nopat" @{const_name nopat} scan || |
|
350 |
scan_fail "illegal pattern kind" |
|
351 |
fun mk_trigger [] t = t |
|
352 |
| mk_trigger ps t = @{term trigger} $ HOLogic.mk_list patternT ps $ t |
|
353 |
||
354 |
val label_kind = |
|
355 |
$$$ "pos" >> K @{term block_at} || |
|
356 |
$$$ "neg" >> K @{term assert_at} || |
|
357 |
scan_fail "illegal label kind" |
|
358 |
||
359 |
fun mk_select (m, k) = |
|
360 |
let |
|
361 |
val mT = Term.fastype_of m and kT = Term.fastype_of k |
|
362 |
val vT = Term.range_type mT |
|
363 |
in Const (@{const_name boogie_select}, mT --> kT --> vT) $ m $ k end |
|
364 |
||
365 |
fun mk_store ((m, k), v) = |
|
366 |
let |
|
367 |
val mT = Term.fastype_of m and kT = Term.fastype_of k |
|
368 |
val vT = Term.fastype_of v |
|
369 |
in |
|
370 |
Const (@{const_name boogie_store}, mT --> kT --> vT --> mT) $ m $ k $ v |
|
371 |
end |
|
372 |
||
373 |
fun mk_extract ((msb, lsb), t) = |
|
374 |
let |
|
375 |
val dT = Term.fastype_of t and rT = mk_wordT (msb - lsb) |
|
376 |
val nT = @{typ nat} |
|
377 |
val mk_nat_num = HOLogic.mk_number @{typ nat} |
|
378 |
in |
|
379 |
Const (@{const_name boogie_bv_extract}, [nT, nT, dT] ---> rT) $ |
|
380 |
mk_nat_num msb $ mk_nat_num lsb $ t |
|
381 |
end |
|
382 |
||
383 |
fun mk_concat (t1, t2) = |
|
384 |
let |
|
385 |
val T1 = Term.fastype_of t1 and T2 = Term.fastype_of t2 |
|
386 |
val U = mk_wordT (dest_wordT T1 + dest_wordT T2) |
|
387 |
in Const (@{const_name boogie_bv_concat}, [T1, T2] ---> U) $ t1 $ t2 end |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
388 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
389 |
val var_name = str >> prefix "V" |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
390 |
val dest_var_name = unprefix "V" |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
391 |
fun rename_variables t = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
392 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
393 |
fun make_context names = Name.make_context (duplicates (op =) names) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
394 |
fun short_var_name n = short_name (dest_var_name n) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
395 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
396 |
val (names, nctxt) = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
397 |
Term.add_free_names t [] |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
398 |
|> map_filter (try (fn n => (n, short_var_name n))) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
399 |
|> split_list |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
400 |
||>> (fn names => Name.variants names (make_context names)) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
401 |
|>> Symtab.make o (op ~~) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
402 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
403 |
fun rename_free n = the_default n (Symtab.lookup names n) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
404 |
fun rename_abs n = yield_singleton Name.variants (short_var_name n) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
405 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
406 |
fun rename _ (Free (n, T)) = Free (rename_free n, T) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
407 |
| rename nctxt (Abs (n, T, t)) = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
408 |
let val (n', nctxt') = rename_abs n nctxt |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
409 |
in Abs (n', T, rename nctxt' t) end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
410 |
| rename nctxt (t $ u) = rename nctxt t $ rename nctxt u |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
411 |
| rename _ t = t |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
412 |
in rename nctxt t end |
33419 | 413 |
in |
414 |
fun expr tds fds = |
|
415 |
let |
|
416 |
fun binop t (u1, u2) = t $ u1 $ u2 |
|
417 |
fun binexp s f = scan_line' s |-- exp -- exp >> f |
|
418 |
||
419 |
and exp st = |
|
420 |
(scan_line' "true" >> K @{term True} || |
|
421 |
scan_line' "false" >> K @{term False} || |
|
422 |
scan_line' "not" |-- exp >> HOLogic.mk_not || |
|
423 |
scan_line "and" num :|-- scan_count exp >> |
|
424 |
mk_nary (curry HOLogic.mk_conj) @{term True} || |
|
425 |
scan_line "or" num :|-- scan_count exp >> |
|
426 |
mk_nary (curry HOLogic.mk_disj) @{term False} || |
|
427 |
binexp "implies" (binop @{term "op -->"}) || |
|
428 |
scan_line "distinct" num :|-- scan_count exp >> |
|
429 |
(fn [] => @{term True} |
|
430 |
| ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) || |
|
431 |
binexp "=" HOLogic.mk_eq || |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
432 |
scan_line "var" var_name -- typ tds >> Free || |
33419 | 433 |
scan_line "fun" (str -- num) :|-- (fn (name, arity) => |
434 |
scan_lookup "constant" fds name -- scan_count exp arity >> |
|
435 |
Term.list_comb) || |
|
436 |
quants :|-- (fn (q, ((n, k), i)) => |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
437 |
scan_count (scan_line "var" var_name -- typ tds) n -- |
33419 | 438 |
scan_count (pattern exp) k -- |
439 |
scan_count (attribute tds fds) i -- |
|
440 |
exp >> (fn (((vs, ps), _), t) => |
|
441 |
fold_rev (mk_quant q) vs (mk_trigger ps t))) || |
|
442 |
scan_line "label" (label_kind -- num -- num) -- exp >> |
|
443 |
(fn (((l, line), col), t) => |
|
444 |
if line = 0 orelse col = 0 then t |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
445 |
else l $ Free (label_name line col, @{typ bool}) $ t) || |
33419 | 446 |
scan_line "int-num" num >> HOLogic.mk_number @{typ int} || |
447 |
binexp "<" (binop @{term "op < :: int => _"}) || |
|
448 |
binexp "<=" (binop @{term "op <= :: int => _"}) || |
|
449 |
binexp ">" (binop @{term "op < :: int => _"} o swap) || |
|
450 |
binexp ">=" (binop @{term "op <= :: int => _"} o swap) || |
|
451 |
binexp "+" (binop @{term "op + :: int => _"}) || |
|
33661 | 452 |
binexp "-" (binop @{term "op - :: int => _"}) || |
453 |
binexp "*" (binop @{term "op * :: int => _"}) || |
|
33419 | 454 |
binexp "/" (binop @{term boogie_div}) || |
455 |
binexp "%" (binop @{term boogie_mod}) || |
|
456 |
scan_line "select" num :|-- (fn arity => |
|
457 |
exp -- (scan_count exp (arity - 1) >> HOLogic.mk_tuple) >> |
|
458 |
mk_select) || |
|
459 |
scan_line "store" num :|-- (fn arity => |
|
460 |
exp -- (scan_count exp (arity - 2) >> HOLogic.mk_tuple) -- exp >> |
|
461 |
mk_store) || |
|
462 |
scan_line "bv-num" (num -- num) >> (fn (size, i) => |
|
463 |
HOLogic.mk_number (mk_wordT size) i) || |
|
464 |
scan_line "bv-extract" (num -- num) -- exp >> mk_extract || |
|
465 |
binexp "bv-concat" mk_concat || |
|
466 |
scan_fail "illegal expression") st |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
467 |
in exp >> rename_variables end |
33419 | 468 |
|
469 |
and attribute tds fds = |
|
470 |
let |
|
471 |
val attr_val = |
|
472 |
scan_line' "expr-attr" |-- expr tds fds >> TermValue || |
|
473 |
scan_line "string-attr" (Scan.repeat1 str) >> |
|
474 |
(StringValue o space_implode " ") || |
|
475 |
scan_fail "illegal attribute value" |
|
476 |
in |
|
477 |
scan_line "attribute" (str -- num) :|-- (fn (name, i) => |
|
478 |
scan_count attr_val i >> pair name) || |
|
479 |
scan_fail "illegal attribute" |
|
480 |
end |
|
481 |
end |
|
482 |
||
483 |
fun type_decls verbose = Scan.depend (fn thy => |
|
484 |
Scan.repeat (scan_line "type-decl" (str -- num -- num) :|-- (fn (ty, i) => |
|
485 |
scan_count (attribute Symtab.empty Symtab.empty) i >> K ty)) >> |
|
486 |
(fn tys => declare_types verbose tys thy)) |
|
487 |
||
488 |
fun fun_decls verbose tds = Scan.depend (fn thy => |
|
489 |
Scan.repeat (scan_line "fun-decl" (str -- num -- num) :|-- |
|
490 |
(fn ((name, arity), i) => |
|
491 |
scan_count (typ tds) (arity - 1) -- typ tds -- |
|
492 |
scan_count (attribute tds Symtab.empty) i >> pair name)) >> |
|
493 |
(fn fns => declare_functions verbose fns thy)) |
|
494 |
||
495 |
fun axioms verbose tds fds = Scan.depend (fn thy => |
|
496 |
Scan.repeat (scan_line "axiom" num :|-- (fn i => |
|
497 |
expr tds fds --| scan_count (attribute tds fds) i)) >> |
|
498 |
(fn axs => (add_axioms verbose axs thy, ()))) |
|
499 |
||
500 |
fun var_decls tds fds = Scan.depend (fn thy => |
|
501 |
Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) => |
|
502 |
typ tds -- scan_count (attribute tds fds) i >> K ())) >> K (thy, ())) |
|
503 |
||
504 |
fun vcs verbose tds fds = Scan.depend (fn thy => |
|
505 |
Scan.repeat (scan_line "vc" (str -- num) -- |
|
506 |
(expr tds fds >> Sign.cert_term thy)) >> |
|
507 |
(fn vcs => ((), add_vcs verbose vcs thy))) |
|
508 |
||
509 |
fun parse verbose thy = Scan.pass thy |
|
510 |
(type_decls verbose :|-- (fn tds => |
|
511 |
fun_decls verbose tds :|-- (fn fds => |
|
512 |
axioms verbose tds fds |-- |
|
513 |
var_decls tds fds |-- |
|
514 |
vcs verbose tds fds))) |
|
515 |
||
516 |
fun load_b2i verbose path thy = finite (parse verbose thy) path |
|
517 |
||
518 |
end |