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