author | wenzelm |
Thu, 09 Jun 2011 20:22:22 +0200 | |
changeset 43329 | 84472e198515 |
parent 43326 | 47cf4bc789aa |
child 43702 | 24fb44c1086a |
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 |
|
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:
34959
diff
changeset
|
9 |
val load_b2i: bool -> (string * int) list -> Path.T -> theory -> theory |
33419 | 10 |
end |
11 |
||
12 |
structure Boogie_Loader: BOOGIE_LOADER = |
|
13 |
struct |
|
14 |
||
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
15 |
fun log verbose text args x = |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
16 |
if verbose andalso not (null args) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
17 |
then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); x) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
18 |
else x |
33419 | 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 |
||
34959
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
33 |
fun drop_underscore s = |
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
34 |
try (unsuffix "_") s |
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
35 |
|> Option.map drop_underscore |
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
36 |
|> the_default s |
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
37 |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
38 |
val short_name = |
34959
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
39 |
translate_string (fn s => if Symbol.is_letdig s then s else "") #> |
cd7c98fdab80
drop underscores at end of names coming from Boogie
boehmes
parents:
34181
diff
changeset
|
40 |
drop_underscore |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
41 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
42 |
(* these prefixes must be distinct: *) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
43 |
val var_prefix = "V_" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
44 |
val label_prefix = "L_" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
45 |
val position_prefix = "P_" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
46 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
47 |
val no_label_name = label_prefix ^ "unknown" |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
48 |
fun label_name line col = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
49 |
if line = 0 orelse col = 0 then no_label_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
50 |
else label_prefix ^ string_of_int line ^ "_" ^ string_of_int col |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
51 |
|
35358 | 52 |
fun mk_syntax name i = |
53 |
let |
|
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
40681
diff
changeset
|
54 |
val syn = Syntax_Ext.escape name |
35391 | 55 |
val args = space_implode ",/ " (replicate i "_") |
35358 | 56 |
in |
57 |
if i = 0 then Mixfix (syn, [], 1000) |
|
58 |
else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) |
|
59 |
end |
|
60 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
61 |
|
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
62 |
datatype attribute_value = StringValue of string | TermValue of term |
33419 | 63 |
|
64 |
||
65 |
||
66 |
local |
|
67 |
fun lookup_type_name thy name arity = |
|
68 |
let val intern = Sign.intern_type thy name |
|
69 |
in |
|
70 |
if Sign.declared_tyname thy intern |
|
71 |
then |
|
72 |
if Sign.arity_number thy intern = arity then SOME intern |
|
73 |
else error ("Boogie: type already declared with different arity: " ^ |
|
74 |
quote name) |
|
75 |
else NONE |
|
76 |
end |
|
77 |
||
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
78 |
fun log_new bname name = bname ^ " (as " ^ name ^ ")" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
79 |
fun log_ex bname name = "[" ^ bname ^ " has already been declared as " ^ |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
80 |
name ^ "]" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
81 |
|
33419 | 82 |
fun declare (name, arity) thy = |
83 |
let val isa_name = isabelle_name name |
|
84 |
in |
|
85 |
(case lookup_type_name thy isa_name arity of |
|
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
86 |
SOME type_name => (((name, type_name), log_ex name type_name), thy) |
33419 | 87 |
| NONE => |
88 |
let |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
89 |
val args = map (rpair dummyS) (Name.invent Name.context "'a" arity) |
35625 | 90 |
val (T, thy') = |
35682 | 91 |
Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy |
33419 | 92 |
val type_name = fst (Term.dest_Type T) |
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
93 |
in (((name, type_name), log_new name type_name), thy') end) |
33419 | 94 |
end |
95 |
in |
|
96 |
fun declare_types verbose tys = |
|
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
97 |
fold_map declare tys #>> split_list #-> (fn (tds, logs) => |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
98 |
log verbose "Declared types:" logs #> |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
99 |
rpair (Symtab.make tds)) |
33419 | 100 |
end |
101 |
||
102 |
||
103 |
||
104 |
local |
|
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
105 |
fun maybe_builtin T = |
33419 | 106 |
let |
107 |
fun const name = SOME (Const (name, T)) |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
108 |
fun const2_abs name = |
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
109 |
let val U = Term.domain_type T |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
110 |
in |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
111 |
SOME (Abs (Name.uu, U, Abs (Name.uu, U, |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
112 |
Const (name, T) $ Bound 0 $ Bound 1))) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
113 |
end |
33419 | 114 |
|
115 |
fun choose builtin = |
|
116 |
(case builtin of |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
117 |
"bvnot" => const @{const_name bitNOT} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
118 |
| "bvand" => const @{const_name bitAND} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
119 |
| "bvor" => const @{const_name bitOR} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
120 |
| "bvxor" => const @{const_name bitXOR} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
121 |
| "bvadd" => const @{const_name plus} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
122 |
| "bvneg" => const @{const_name uminus} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
123 |
| "bvsub" => const @{const_name minus} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
124 |
| "bvmul" => const @{const_name times} |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36610
diff
changeset
|
125 |
(* FIXME: |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
126 |
| "bvudiv" => const @{const_name div} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
127 |
| "bvurem" => const @{const_name mod} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
128 |
| "bvsdiv" => const @{const_name sdiv} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
129 |
| "bvsrem" => const @{const_name srem} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
130 |
| "bvshl" => const @{const_name bv_shl} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
131 |
| "bvlshr" => const @{const_name bv_lshr} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
132 |
| "bvashr" => const @{const_name bv_ashr} |
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36610
diff
changeset
|
133 |
*) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
134 |
| "bvult" => const @{const_name less} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
135 |
| "bvule" => const @{const_name less_eq} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
136 |
| "bvugt" => const2_abs @{const_name less} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
137 |
| "bvuge" => const2_abs @{const_name less_eq} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
138 |
| "bvslt" => const @{const_name word_sless} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
139 |
| "bvsle" => const @{const_name word_sle} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
140 |
| "bvsgt" => const2_abs @{const_name word_sless} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
141 |
| "bvsge" => const2_abs @{const_name word_sle} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
142 |
| "zero_extend" => const @{const_name ucast} |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
143 |
| "sign_extend" => const @{const_name scast} |
33419 | 144 |
| _ => NONE) |
145 |
||
146 |
fun is_builtin att = |
|
147 |
(case att of |
|
148 |
("bvbuiltin", [StringValue builtin]) => choose builtin |
|
149 |
| ("bvint", [StringValue "ITE"]) => const @{const_name If} |
|
150 |
| _ => NONE) |
|
151 |
in get_first is_builtin end |
|
152 |
||
153 |
fun lookup_const thy name T = |
|
33465 | 154 |
let val intern = Sign.intern_const thy name |
33419 | 155 |
in |
156 |
if Sign.declared_const thy intern |
|
157 |
then |
|
33465 | 158 |
if Sign.typ_instance thy (T, Sign.the_const_type thy intern) |
33419 | 159 |
then SOME (Const (intern, T)) |
160 |
else error ("Boogie: function already declared with different type: " ^ |
|
161 |
quote name) |
|
162 |
else NONE |
|
163 |
end |
|
164 |
||
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
165 |
fun log_term thy t = Syntax.string_of_term_global thy t |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
166 |
fun log_new thy name t = name ^ " (as " ^ log_term thy t ^ ")" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
167 |
fun log_ex thy name t = "[" ^ name ^ " has already been declared as " ^ |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
168 |
log_term thy t ^ "]" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
169 |
fun log_builtin thy name t = "[" ^ name ^ " has been identified as " ^ |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
170 |
log_term thy t ^ "]" |
33419 | 171 |
|
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
172 |
fun declare' name isa_name T arity atts thy = |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
173 |
(case lookup_const thy isa_name T of |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
174 |
SOME t => (((name, t), log_ex thy name t), thy) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
175 |
| NONE => |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
176 |
(case maybe_builtin T atts of |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
177 |
SOME t => (((name, t), log_builtin thy name t), thy) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
178 |
| NONE => |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
179 |
thy |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42361
diff
changeset
|
180 |
|> Sign.declare_const_global ((Binding.name isa_name, T), |
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
181 |
mk_syntax name arity) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
182 |
|> (fn (t, thy') => (((name, t), log_new thy' name t), thy')))) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
183 |
fun declare (name, ((Ts, T), atts)) = |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
184 |
declare' name (isabelle_name name) (Ts ---> T) (length Ts) atts |
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
185 |
|
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
186 |
fun uniques fns fds = |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
187 |
let |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
188 |
fun is_unique (name, (([], _), atts)) = |
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
189 |
(case AList.lookup (op =) atts "unique" of |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
190 |
SOME _ => Symtab.lookup fds name |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
191 |
| NONE => NONE) |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
192 |
| is_unique _ = NONE |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
193 |
fun mk_unique_axiom T ts = |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40627
diff
changeset
|
194 |
Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ |
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
195 |
HOLogic.mk_list T ts |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
196 |
in |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
197 |
map_filter is_unique fns |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
198 |
|> map (swap o Term.dest_Const) |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
199 |
|> AList.group (op =) |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
200 |
|> map (fn (T, ns) => mk_unique_axiom T (map (Const o rpair T) ns)) |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
201 |
end |
33419 | 202 |
in |
203 |
fun declare_functions verbose fns = |
|
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
204 |
fold_map declare fns #>> split_list #-> (fn (fds, logs) => |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
205 |
log verbose "Loaded constants:" logs #> |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
206 |
rpair (` (uniques fns) (Symtab.make fds))) |
33419 | 207 |
end |
208 |
||
209 |
||
210 |
||
211 |
local |
|
212 |
fun name_axioms axs = |
|
213 |
let fun mk_name idx = "axiom_" ^ string_of_int (idx + 1) |
|
214 |
in map_index (fn (idx, t) => (mk_name idx, HOLogic.mk_Trueprop t)) axs end |
|
215 |
||
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
216 |
datatype kind = Unused of thm | Used of thm | New of string |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
217 |
|
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
218 |
fun mark (name, t) axs = |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
219 |
(case Termtab.lookup axs t of |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
220 |
SOME (Unused thm) => Termtab.update (t, Used thm) axs |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
221 |
| NONE => Termtab.update (t, New name) axs |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
222 |
| SOME _ => axs) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
223 |
|
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
224 |
val sort_fst_str = sort (prod_ord fast_string_ord (K EQUAL)) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
225 |
fun split_list_kind thy axs = |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
226 |
let |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
227 |
fun split (_, Used thm) (used, new) = (thm :: used, new) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
228 |
| split (t, New name) (used, new) = (used, (name, t) :: new) |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
229 |
| split (_, Unused thm) (used, new) = |
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
230 |
(warning (Pretty.str_of |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
231 |
(Pretty.big_list "This background axiom has not been loaded:" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
232 |
[Display.pretty_thm_global thy thm])); |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
233 |
(used, new)) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
234 |
in apsnd sort_fst_str (fold split axs ([], [])) end |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
235 |
|
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
236 |
fun mark_axioms thy axs = |
42361 | 237 |
Boogie_Axioms.get (Proof_Context.init_global thy) |
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
238 |
|> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm)) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
239 |
|> fold mark axs |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
240 |
|> split_list_kind thy o Termtab.dest |
33419 | 241 |
in |
242 |
fun add_axioms verbose axs thy = |
|
35862
c2039b00ff0d
replaced old-style Drule.add_axiom by Specification.axiomatization
boehmes
parents:
35856
diff
changeset
|
243 |
let |
c2039b00ff0d
replaced old-style Drule.add_axiom by Specification.axiomatization
boehmes
parents:
35856
diff
changeset
|
244 |
val (used, new) = mark_axioms thy (name_axioms axs) |
33419 | 245 |
in |
246 |
thy |
|
35895
387de5db0a74
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
wenzelm
parents:
35862
diff
changeset
|
247 |
|> fold_map (fn (n, t) => Specification.axiom ((Binding.name n, []), t)) new |
387de5db0a74
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
wenzelm
parents:
35862
diff
changeset
|
248 |
|-> Context.theory_map o fold (Boogie_Axioms.add_thm o Drule.export_without_context) |
34011
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
249 |
|> log verbose "The following axioms were added:" (map fst new) |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
250 |
|> (fn thy' => log verbose "The following axioms already existed:" |
2b3f4fcbc066
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
boehmes
parents:
33893
diff
changeset
|
251 |
(map (Display.string_of_thm_global thy') used) thy') |
33419 | 252 |
end |
253 |
end |
|
254 |
||
255 |
||
256 |
||
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
257 |
local |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
258 |
fun burrow_distinct eq f xs = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
259 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
260 |
val ys = distinct eq xs |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
261 |
val tab = ys ~~ f ys |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
262 |
in map (the o AList.lookup eq tab) xs end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
263 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
264 |
fun indexed names = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
265 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
266 |
val dup = member (op =) (duplicates (op =) (map fst names)) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
267 |
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
|
268 |
in map make_name names end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
269 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
270 |
fun rename idx_names = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
271 |
idx_names |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
272 |
|> burrow_fst (burrow_distinct (op =) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
273 |
(map short_name #> ` (duplicates (op =)) #-> Name.variant_list)) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
274 |
|> indexed |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
275 |
in |
33419 | 276 |
fun add_vcs verbose vcs thy = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
277 |
let val vcs' = burrow_fst rename vcs |
33419 | 278 |
in |
279 |
thy |
|
280 |
|> Boogie_VCs.set vcs' |
|
281 |
|> log verbose "The following verification conditions were loaded:" |
|
282 |
(map fst vcs') |
|
283 |
end |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
284 |
end |
33419 | 285 |
|
286 |
||
287 |
||
288 |
local |
|
289 |
fun mk_bitT i T = |
|
290 |
if i = 0 |
|
291 |
then Type (@{type_name "Numeral_Type.bit0"}, [T]) |
|
292 |
else Type (@{type_name "Numeral_Type.bit1"}, [T]) |
|
293 |
||
294 |
fun mk_binT size = |
|
295 |
if size = 0 then @{typ "Numeral_Type.num0"} |
|
296 |
else if size = 1 then @{typ "Numeral_Type.num1"} |
|
297 |
else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end |
|
298 |
in |
|
299 |
fun mk_wordT size = |
|
300 |
if size >= 0 then Type (@{type_name "word"}, [mk_binT size]) |
|
301 |
else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], []) |
|
302 |
end |
|
303 |
||
304 |
local |
|
305 |
fun dest_binT T = |
|
306 |
(case T of |
|
307 |
Type (@{type_name "Numeral_Type.num0"}, _) => 0 |
|
308 |
| Type (@{type_name "Numeral_Type.num1"}, _) => 1 |
|
309 |
| Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T |
|
310 |
| Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T |
|
311 |
| _ => raise TYPE ("dest_binT", [T], [])) |
|
312 |
in |
|
313 |
val dest_wordT = (fn |
|
314 |
Type (@{type_name "word"}, [T]) => dest_binT T |
|
315 |
| T => raise TYPE ("dest_wordT", [T], [])) |
|
316 |
end |
|
317 |
||
318 |
fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T]) |
|
319 |
||
320 |
||
321 |
||
322 |
datatype token = Token of string | Newline | EOF |
|
323 |
||
324 |
fun tokenize path = |
|
325 |
let |
|
326 |
fun blank c = (c = #" " orelse c = #"\t" orelse c = #"\n" orelse c = #"\r") |
|
327 |
fun split line (i, tss) = (i + 1, |
|
328 |
map (pair i) (map Token (String.tokens blank line) @ [Newline]) :: tss) |
|
329 |
in apsnd (flat o rev) (File.fold_lines split path (1, [])) end |
|
330 |
||
331 |
fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false) |
|
332 |
||
333 |
fun scan_err msg [] = "Boogie (at end of input): " ^ msg |
|
334 |
| scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^ |
|
335 |
msg |
|
336 |
||
337 |
fun scan_fail msg = Scan.fail_with (scan_err msg) |
|
338 |
||
339 |
fun finite scan path = |
|
340 |
let val (i, ts) = tokenize path |
|
341 |
in |
|
342 |
(case Scan.error (Scan.finite (stopper i) scan) ts of |
|
343 |
(x, []) => x |
|
38245 | 344 |
| (_, ts') => error (scan_err "unparsed input" ts')) |
33419 | 345 |
end |
346 |
||
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40274
diff
changeset
|
347 |
fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE) |
33419 | 348 |
|
349 |
fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false) |
|
33497 | 350 |
fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st |
351 |
fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st |
|
33419 | 352 |
|
353 |
fun scan_line key scan = |
|
354 |
$$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false) |
|
355 |
fun scan_line' key = scan_line key (Scan.succeed ()) |
|
356 |
||
357 |
fun scan_count scan i = |
|
358 |
if i > 0 then scan ::: scan_count scan (i - 1) else Scan.succeed [] |
|
359 |
||
360 |
fun scan_lookup kind tab key = |
|
361 |
(case Symtab.lookup tab key of |
|
362 |
SOME value => Scan.succeed value |
|
363 |
| NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key)) |
|
364 |
||
365 |
fun typ tds = |
|
366 |
let |
|
367 |
fun tp st = |
|
368 |
(scan_line' "bool" >> K @{typ bool} || |
|
369 |
scan_line' "int" >> K @{typ int} || |
|
370 |
scan_line "bv" num >> mk_wordT || |
|
371 |
scan_line "type-con" (str -- num) :|-- (fn (name, arity) => |
|
372 |
scan_lookup "type constructor" tds name -- scan_count tp arity >> |
|
373 |
Type) || |
|
374 |
scan_line "array" num :|-- (fn arity => |
|
375 |
scan_count tp (arity - 1) -- tp >> mk_arrayT) || |
|
376 |
scan_fail "illegal type") st |
|
377 |
in tp end |
|
378 |
||
379 |
local |
|
380 |
fun mk_nary _ t [] = t |
|
33661 | 381 |
| mk_nary f _ ts = uncurry (fold_rev f) (split_last ts) |
33419 | 382 |
|
37124 | 383 |
fun mk_list T = HOLogic.mk_list T |
384 |
||
33419 | 385 |
fun mk_distinct T ts = |
40681
872b08416fb4
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents:
40627
diff
changeset
|
386 |
Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ |
37124 | 387 |
mk_list T ts |
33419 | 388 |
|
389 |
fun quant name f = scan_line name (num -- num -- num) >> pair f |
|
390 |
val quants = |
|
391 |
quant "forall" HOLogic.all_const || |
|
392 |
quant "exists" HOLogic.exists_const || |
|
393 |
scan_fail "illegal quantifier kind" |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
394 |
fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t) |
33419 | 395 |
|
37124 | 396 |
val patternT = @{typ "SMT.pattern"} |
33419 | 397 |
fun mk_pattern _ [] = raise TERM ("mk_pattern", []) |
37124 | 398 |
| mk_pattern n ts = |
399 |
let fun mk_pat t = Const (n, Term.fastype_of t --> patternT) $ t |
|
400 |
in mk_list patternT (map mk_pat ts) end |
|
33419 | 401 |
fun patt n c scan = |
402 |
scan_line n num :|-- scan_count scan >> (mk_pattern c) |
|
403 |
fun pattern scan = |
|
37124 | 404 |
patt "pat" @{const_name "SMT.pat"} scan || |
405 |
patt "nopat" @{const_name "SMT.nopat"} scan || |
|
33419 | 406 |
scan_fail "illegal pattern kind" |
407 |
fun mk_trigger [] t = t |
|
37124 | 408 |
| mk_trigger ps t = |
409 |
@{term "SMT.trigger"} $ mk_list @{typ "SMT.pattern list"} ps $ t |
|
33419 | 410 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
411 |
fun make_label (line, col) = Free (label_name line col, @{typ bool}) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
412 |
fun labelled_by kind pos t = kind $ make_label pos $ t |
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:
34959
diff
changeset
|
413 |
fun label offset = |
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:
34959
diff
changeset
|
414 |
$$$ "pos" |-- num -- num >> (fn (line, col) => |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
415 |
if label_name line col = no_label_name then I |
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:
34959
diff
changeset
|
416 |
else labelled_by @{term block_at} (line - offset, col)) || |
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:
34959
diff
changeset
|
417 |
$$$ "neg" |-- num -- num >> (fn (line, col) => |
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:
34959
diff
changeset
|
418 |
labelled_by @{term assert_at} (line - offset, col)) || |
33419 | 419 |
scan_fail "illegal label kind" |
420 |
||
421 |
fun mk_store ((m, k), v) = |
|
422 |
let |
|
423 |
val mT = Term.fastype_of m and kT = Term.fastype_of k |
|
424 |
val vT = Term.fastype_of v |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
425 |
in Const (@{const_name fun_upd}, mT --> kT --> vT --> mT) $ m $ k $ v end |
33419 | 426 |
|
427 |
fun mk_extract ((msb, lsb), t) = |
|
428 |
let |
|
429 |
val dT = Term.fastype_of t and rT = mk_wordT (msb - lsb) |
|
430 |
val nT = @{typ nat} |
|
431 |
val mk_nat_num = HOLogic.mk_number @{typ nat} |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
432 |
in Const (@{const_name slice}, [nT, dT] ---> rT) $ mk_nat_num lsb $ t end |
33419 | 433 |
|
434 |
fun mk_concat (t1, t2) = |
|
435 |
let |
|
436 |
val T1 = Term.fastype_of t1 and T2 = Term.fastype_of t2 |
|
437 |
val U = mk_wordT (dest_wordT T1 + dest_wordT T2) |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
438 |
in Const (@{const_name word_cat}, [T1, T2] ---> U) $ t1 $ t2 end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
439 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
440 |
fun unique_labels t = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
441 |
let |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
442 |
fun names_of (@{term assert_at} $ Free (n, _) $ t) = cons n #> names_of t |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
443 |
| names_of (t $ u) = names_of t #> names_of u |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
444 |
| names_of (Abs (_, _, t)) = names_of t |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
445 |
| names_of _ = I |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
446 |
val nctxt = Name.make_context (duplicates (op =) (names_of t [])) |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
447 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
448 |
fun fresh (i, nctxt) = (position_prefix ^ string_of_int i, (i+1, nctxt)) |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42375
diff
changeset
|
449 |
fun renamed n (i, nctxt) = Name.variant n nctxt ||> pair i |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
450 |
fun mk_label (name, t) = @{term assert_at} $ Free (name, @{typ bool}) $ t |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
451 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
452 |
fun unique t = |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
453 |
(case t of |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
454 |
@{term assert_at} $ Free (n, _) $ u => |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
455 |
if n = no_label_name |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
456 |
then fresh ##>> unique u #>> mk_label |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
457 |
else renamed n ##>> unique u #>> mk_label |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
458 |
| u1 $ u2 => unique u1 ##>> unique u2 #>> (op $) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
459 |
| Abs (n, T, u) => unique u #>> (fn u' => Abs (n, T, u')) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
460 |
| _ => pair t) |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
461 |
in fst (unique t (1, nctxt)) end |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
462 |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
463 |
val var_name = str >> prefix var_prefix |
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
464 |
val dest_var_name = unprefix var_prefix |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
465 |
fun rename_variables t = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
466 |
let |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
467 |
fun short_var_name n = short_name (dest_var_name n) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
468 |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
469 |
val all_names = Term.add_free_names t [] |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
470 |
val (names, nctxt) = |
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
471 |
all_names |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
472 |
|> map_filter (try (fn n => (n, short_var_name n))) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
473 |
|> split_list |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42375
diff
changeset
|
474 |
||>> (fn names => fold_map Name.variant names (Name.make_context all_names)) |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
475 |
|>> Symtab.make o (op ~~) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
476 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
477 |
fun rename_free n = the_default n (Symtab.lookup names n) |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
42375
diff
changeset
|
478 |
fun rename_abs n = Name.variant (short_var_name n) |
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
479 |
|
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
480 |
fun rename _ (Free (n, T)) = Free (rename_free n, T) |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
481 |
| rename nctxt (Abs (n, T, t)) = |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
482 |
let val (n', nctxt') = rename_abs n nctxt |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
483 |
in Abs (n', T, rename nctxt' t) end |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
484 |
| rename nctxt (t $ u) = rename nctxt t $ rename nctxt u |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
485 |
| rename _ t = t |
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
486 |
in rename nctxt t end |
33419 | 487 |
in |
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:
34959
diff
changeset
|
488 |
fun expr offset tds fds = |
33419 | 489 |
let |
490 |
fun binop t (u1, u2) = t $ u1 $ u2 |
|
491 |
fun binexp s f = scan_line' s |-- exp -- exp >> f |
|
492 |
||
493 |
and exp st = |
|
494 |
(scan_line' "true" >> K @{term True} || |
|
495 |
scan_line' "false" >> K @{term False} || |
|
496 |
scan_line' "not" |-- exp >> HOLogic.mk_not || |
|
497 |
scan_line "and" num :|-- scan_count exp >> |
|
498 |
mk_nary (curry HOLogic.mk_conj) @{term True} || |
|
499 |
scan_line "or" num :|-- scan_count exp >> |
|
500 |
mk_nary (curry HOLogic.mk_disj) @{term False} || |
|
38245 | 501 |
scan_line' "ite" |-- exp -- exp -- exp >> (fn ((c, t1), t2) => |
502 |
let val T = Term.fastype_of t1 |
|
503 |
in |
|
504 |
Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2 |
|
505 |
end) || |
|
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38245
diff
changeset
|
506 |
binexp "implies" (binop @{term HOL.implies}) || |
33419 | 507 |
scan_line "distinct" num :|-- scan_count exp >> |
508 |
(fn [] => @{term True} |
|
509 |
| ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) || |
|
510 |
binexp "=" HOLogic.mk_eq || |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
511 |
scan_line "var" var_name -- typ tds >> Free || |
33419 | 512 |
scan_line "fun" (str -- num) :|-- (fn (name, arity) => |
513 |
scan_lookup "constant" fds name -- scan_count exp arity >> |
|
514 |
Term.list_comb) || |
|
515 |
quants :|-- (fn (q, ((n, k), i)) => |
|
33445
f0c78a28e18e
shorter names for variables and verification conditions,
boehmes
parents:
33424
diff
changeset
|
516 |
scan_count (scan_line "var" var_name -- typ tds) n -- |
33419 | 517 |
scan_count (pattern exp) k -- |
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:
34959
diff
changeset
|
518 |
scan_count (attribute offset tds fds) i -- |
33419 | 519 |
exp >> (fn (((vs, ps), _), t) => |
520 |
fold_rev (mk_quant q) vs (mk_trigger ps t))) || |
|
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:
34959
diff
changeset
|
521 |
scan_line "label" (label offset) -- exp >> (fn (mk, t) => mk t) || |
33419 | 522 |
scan_line "int-num" num >> HOLogic.mk_number @{typ int} || |
523 |
binexp "<" (binop @{term "op < :: int => _"}) || |
|
524 |
binexp "<=" (binop @{term "op <= :: int => _"}) || |
|
525 |
binexp ">" (binop @{term "op < :: int => _"} o swap) || |
|
526 |
binexp ">=" (binop @{term "op <= :: int => _"} o swap) || |
|
527 |
binexp "+" (binop @{term "op + :: int => _"}) || |
|
33661 | 528 |
binexp "-" (binop @{term "op - :: int => _"}) || |
529 |
binexp "*" (binop @{term "op * :: int => _"}) || |
|
33419 | 530 |
binexp "/" (binop @{term boogie_div}) || |
531 |
binexp "%" (binop @{term boogie_mod}) || |
|
532 |
scan_line "select" num :|-- (fn arity => |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
533 |
exp -- (scan_count exp (arity - 1) >> HOLogic.mk_tuple) >> (op $)) || |
33419 | 534 |
scan_line "store" num :|-- (fn arity => |
535 |
exp -- (scan_count exp (arity - 2) >> HOLogic.mk_tuple) -- exp >> |
|
536 |
mk_store) || |
|
537 |
scan_line "bv-num" (num -- num) >> (fn (size, i) => |
|
538 |
HOLogic.mk_number (mk_wordT size) i) || |
|
539 |
scan_line "bv-extract" (num -- num) -- exp >> mk_extract || |
|
540 |
binexp "bv-concat" mk_concat || |
|
541 |
scan_fail "illegal expression") st |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
34011
diff
changeset
|
542 |
in exp >> (rename_variables o unique_labels) end |
33419 | 543 |
|
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:
34959
diff
changeset
|
544 |
and attribute offset tds fds = |
33419 | 545 |
let |
546 |
val attr_val = |
|
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:
34959
diff
changeset
|
547 |
scan_line' "expr-attr" |-- expr offset tds fds >> TermValue || |
33419 | 548 |
scan_line "string-attr" (Scan.repeat1 str) >> |
549 |
(StringValue o space_implode " ") || |
|
550 |
scan_fail "illegal attribute value" |
|
551 |
in |
|
552 |
scan_line "attribute" (str -- num) :|-- (fn (name, i) => |
|
553 |
scan_count attr_val i >> pair name) || |
|
554 |
scan_fail "illegal attribute" |
|
555 |
end |
|
556 |
end |
|
557 |
||
558 |
fun type_decls verbose = Scan.depend (fn thy => |
|
559 |
Scan.repeat (scan_line "type-decl" (str -- num -- num) :|-- (fn (ty, i) => |
|
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:
34959
diff
changeset
|
560 |
scan_count (attribute 0 Symtab.empty Symtab.empty) i >> K ty)) >> |
33419 | 561 |
(fn tys => declare_types verbose tys thy)) |
562 |
||
563 |
fun fun_decls verbose tds = Scan.depend (fn thy => |
|
564 |
Scan.repeat (scan_line "fun-decl" (str -- num -- num) :|-- |
|
565 |
(fn ((name, arity), i) => |
|
566 |
scan_count (typ tds) (arity - 1) -- typ tds -- |
|
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:
34959
diff
changeset
|
567 |
scan_count (attribute 0 tds Symtab.empty) i >> pair name)) >> |
33419 | 568 |
(fn fns => declare_functions verbose fns thy)) |
569 |
||
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
570 |
fun axioms verbose tds fds unique_axs = Scan.depend (fn thy => |
33419 | 571 |
Scan.repeat (scan_line "axiom" num :|-- (fn i => |
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:
34959
diff
changeset
|
572 |
expr 0 tds fds --| scan_count (attribute 0 tds fds) i)) >> |
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
573 |
(fn axs => (add_axioms verbose (unique_axs @ axs) thy, ()))) |
33419 | 574 |
|
575 |
fun var_decls tds fds = Scan.depend (fn thy => |
|
576 |
Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) => |
|
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:
34959
diff
changeset
|
577 |
typ tds -- scan_count (attribute 0 tds fds) i >> K ())) >> K (thy, ())) |
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:
34959
diff
changeset
|
578 |
|
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:
34959
diff
changeset
|
579 |
fun local_vc_offset offsets vc_name = |
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:
34959
diff
changeset
|
580 |
Integer.add ~1 (the_default 1 (AList.lookup (op =) offsets vc_name)) |
33419 | 581 |
|
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:
34959
diff
changeset
|
582 |
fun vcs verbose offsets tds fds = Scan.depend (fn thy => |
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:
34959
diff
changeset
|
583 |
Scan.repeat (scan_line "vc" (str -- num) :-- (fn (name, _) => |
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:
34959
diff
changeset
|
584 |
(expr (local_vc_offset offsets name) tds fds))) >> |
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:
34959
diff
changeset
|
585 |
(fn vcs => ((), add_vcs verbose vcs thy))) |
33419 | 586 |
|
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:
34959
diff
changeset
|
587 |
fun parse verbose offsets thy = Scan.pass thy |
33419 | 588 |
(type_decls verbose :|-- (fn tds => |
33893
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
589 |
fun_decls verbose tds :|-- (fn (unique_axs, fds) => |
24b648ea4834
respect "unique" attribute: generate distinctness axioms
boehmes
parents:
33661
diff
changeset
|
590 |
axioms verbose tds fds unique_axs |-- |
33419 | 591 |
var_decls tds fds |-- |
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:
34959
diff
changeset
|
592 |
vcs verbose offsets tds fds))) |
33419 | 593 |
|
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:
34959
diff
changeset
|
594 |
fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) path |
33419 | 595 |
|
596 |
end |