# HG changeset patch # User boehmes # Date 1266165988 -3600 # Node ID acace7e303574f252688dc3b0a0eaae7ea989fb7 # Parent 33976519c88892755db633f8520f5445cf2a6c3f optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program diff -r 33976519c888 -r acace7e30357 src/HOL/Boogie/Tools/boogie_commands.ML --- 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 diff -r 33976519c888 -r acace7e30357 src/HOL/Boogie/Tools/boogie_loader.ML --- 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