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