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