optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Feb 14 00:26:48 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Feb 14 17:46:28 2010 +0100
@@ -14,7 +14,7 @@
(* commands *)
-fun boogie_open (quiet, base_name) thy =
+fun boogie_open ((quiet, base_name), offsets) thy =
let
val path = Path.explode (base_name ^ ".b2i")
val _ = File.exists path orelse
@@ -22,7 +22,7 @@
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
"but another Boogie environment is still open.")
- in Boogie_Loader.load_b2i (not quiet) path thy end
+ in Boogie_Loader.load_b2i (not quiet) offsets path thy end
datatype vc_opts =
@@ -225,11 +225,15 @@
fun scan_arg f = Args.parens f
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
+val vc_offsets = Scan.optional (Args.bracks (OuterParse.list1
+ (OuterParse.string --| Args.colon -- OuterParse.nat))) []
+
val _ =
OuterSyntax.command "boogie_open"
"Open a new Boogie environment and load a Boogie-generated .b2i file."
OuterKeyword.thy_decl
- (scan_opt "quiet" -- OuterParse.name >> (Toplevel.theory o boogie_open))
+ (scan_opt "quiet" -- OuterParse.name -- vc_offsets >>
+ (Toplevel.theory o boogie_open))
val vc_name = OuterParse.name
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Feb 14 00:26:48 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sun Feb 14 17:46:28 2010 +0100
@@ -6,7 +6,7 @@
signature BOOGIE_LOADER =
sig
- val load_b2i: bool -> Path.T -> theory -> theory
+ val load_b2i: bool -> (string * int) list -> Path.T -> theory -> theory
end
structure Boogie_Loader: BOOGIE_LOADER =
@@ -414,11 +414,12 @@
fun make_label (line, col) = Free (label_name line col, @{typ bool})
fun labelled_by kind pos t = kind $ make_label pos $ t
- val label =
- $$$ "pos" |-- num -- num >> (fn (pos as (line, col)) =>
+ fun label offset =
+ $$$ "pos" |-- num -- num >> (fn (line, col) =>
if label_name line col = no_label_name then I
- else labelled_by @{term block_at} pos) ||
- $$$ "neg" |-- num -- num >> labelled_by @{term assert_at} ||
+ else labelled_by @{term block_at} (line - offset, col)) ||
+ $$$ "neg" |-- num -- num >> (fn (line, col) =>
+ labelled_by @{term assert_at} (line - offset, col)) ||
scan_fail "illegal label kind"
fun mk_store ((m, k), v) =
@@ -489,7 +490,7 @@
| rename _ t = t
in rename nctxt t end
in
-fun expr tds fds =
+fun expr offset tds fds =
let
fun binop t (u1, u2) = t $ u1 $ u2
fun binexp s f = scan_line' s |-- exp -- exp >> f
@@ -514,10 +515,10 @@
quants :|-- (fn (q, ((n, k), i)) =>
scan_count (scan_line "var" var_name -- typ tds) n --
scan_count (pattern exp) k --
- scan_count (attribute tds fds) i --
+ scan_count (attribute offset tds fds) i --
exp >> (fn (((vs, ps), _), t) =>
fold_rev (mk_quant q) vs (mk_trigger ps t))) ||
- scan_line "label" label -- exp >> (fn (mk, t) => mk t) ||
+ scan_line "label" (label offset) -- exp >> (fn (mk, t) => mk t) ||
scan_line "int-num" num >> HOLogic.mk_number @{typ int} ||
binexp "<" (binop @{term "op < :: int => _"}) ||
binexp "<=" (binop @{term "op <= :: int => _"}) ||
@@ -540,10 +541,10 @@
scan_fail "illegal expression") st
in exp >> (rename_variables o unique_labels) end
-and attribute tds fds =
+and attribute offset tds fds =
let
val attr_val =
- scan_line' "expr-attr" |-- expr tds fds >> TermValue ||
+ scan_line' "expr-attr" |-- expr offset tds fds >> TermValue ||
scan_line "string-attr" (Scan.repeat1 str) >>
(StringValue o space_implode " ") ||
scan_fail "illegal attribute value"
@@ -556,36 +557,40 @@
fun type_decls verbose = Scan.depend (fn thy =>
Scan.repeat (scan_line "type-decl" (str -- num -- num) :|-- (fn (ty, i) =>
- scan_count (attribute Symtab.empty Symtab.empty) i >> K ty)) >>
+ scan_count (attribute 0 Symtab.empty Symtab.empty) i >> K ty)) >>
(fn tys => declare_types verbose tys thy))
fun fun_decls verbose tds = Scan.depend (fn thy =>
Scan.repeat (scan_line "fun-decl" (str -- num -- num) :|--
(fn ((name, arity), i) =>
scan_count (typ tds) (arity - 1) -- typ tds --
- scan_count (attribute tds Symtab.empty) i >> pair name)) >>
+ scan_count (attribute 0 tds Symtab.empty) i >> pair name)) >>
(fn fns => declare_functions verbose fns thy))
fun axioms verbose tds fds unique_axs = Scan.depend (fn thy =>
Scan.repeat (scan_line "axiom" num :|-- (fn i =>
- expr tds fds --| scan_count (attribute tds fds) i)) >>
+ expr 0 tds fds --| scan_count (attribute 0 tds fds) i)) >>
(fn axs => (add_axioms verbose (unique_axs @ axs) thy, ())))
fun var_decls tds fds = Scan.depend (fn thy =>
Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) =>
- typ tds -- scan_count (attribute tds fds) i >> K ())) >> K (thy, ()))
+ typ tds -- scan_count (attribute 0 tds fds) i >> K ())) >> K (thy, ()))
+
+fun local_vc_offset offsets vc_name =
+ Integer.add ~1 (the_default 1 (AList.lookup (op =) offsets vc_name))
-fun vcs verbose tds fds = Scan.depend (fn thy =>
- Scan.repeat (scan_line "vc" (str -- num) --
- (expr tds fds)) >> (fn vcs => ((), add_vcs verbose vcs thy)))
+fun vcs verbose offsets tds fds = Scan.depend (fn thy =>
+ Scan.repeat (scan_line "vc" (str -- num) :-- (fn (name, _) =>
+ (expr (local_vc_offset offsets name) tds fds))) >>
+ (fn vcs => ((), add_vcs verbose vcs thy)))
-fun parse verbose thy = Scan.pass thy
+fun parse verbose offsets thy = Scan.pass thy
(type_decls verbose :|-- (fn tds =>
fun_decls verbose tds :|-- (fn (unique_axs, fds) =>
axioms verbose tds fds unique_axs |--
var_decls tds fds |--
- vcs verbose tds fds)))
+ vcs verbose offsets tds fds)))
-fun load_b2i verbose path thy = finite (parse verbose thy) path
+fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) path
end