src/HOL/Boogie/Tools/boogie_loader.ML
author boehmes
Fri Nov 06 21:53:20 2009 +0100 (2009-11-06)
changeset 33497 39c9d0785911
parent 33465 8c489493e65e
child 33661 31a129cc0d10
permissions -rw-r--r--
made SML/NJ happy
boehmes@33419
     1
(*  Title:      HOL/Boogie/Tools/boogie_loader.ML
boehmes@33419
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@33419
     3
boehmes@33419
     4
Loading and interpreting Boogie-generated files.
boehmes@33419
     5
*)
boehmes@33419
     6
boehmes@33419
     7
signature BOOGIE_LOADER =
boehmes@33419
     8
sig
boehmes@33419
     9
  val load_b2i: bool -> Path.T -> theory -> theory
boehmes@33419
    10
end
boehmes@33419
    11
boehmes@33419
    12
structure Boogie_Loader: BOOGIE_LOADER =
boehmes@33419
    13
struct
boehmes@33419
    14
boehmes@33419
    15
fun log verbose text args thy =
boehmes@33419
    16
  if verbose
boehmes@33419
    17
  then (Pretty.writeln (Pretty.big_list text (map Pretty.str args)); thy)
boehmes@33419
    18
  else thy
boehmes@33419
    19
boehmes@33419
    20
val isabelle_name =
boehmes@33419
    21
  let 
boehmes@33445
    22
    fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else
boehmes@33419
    23
      (case s of
boehmes@33419
    24
        "." => "_o_"
boehmes@33419
    25
      | "_" => "_n_"
boehmes@33419
    26
      | "$" => "_S_"
boehmes@33419
    27
      | "@" => "_G_"
boehmes@33419
    28
      | "#" => "_H_"
boehmes@33419
    29
      | "^" => "_T_"
boehmes@33419
    30
      | _   => ("_" ^ string_of_int (ord s) ^ "_"))
boehmes@33419
    31
  in prefix "b_" o translate_string purge end
boehmes@33419
    32
boehmes@33445
    33
val short_name =
boehmes@33445
    34
  translate_string (fn s => if Symbol.is_letdig s then s else "")
boehmes@33445
    35
boehmes@33445
    36
fun label_name line col = "L_" ^ string_of_int line ^ "_" ^ string_of_int col
boehmes@33445
    37
boehmes@33419
    38
datatype attribute_value = StringValue of string | TermValue of Term.term
boehmes@33419
    39
boehmes@33419
    40
boehmes@33419
    41
boehmes@33419
    42
local
boehmes@33419
    43
  fun lookup_type_name thy name arity =
boehmes@33419
    44
    let val intern = Sign.intern_type thy name
boehmes@33419
    45
    in
boehmes@33419
    46
      if Sign.declared_tyname thy intern
boehmes@33419
    47
      then
boehmes@33419
    48
        if Sign.arity_number thy intern = arity then SOME intern
boehmes@33419
    49
        else error ("Boogie: type already declared with different arity: " ^
boehmes@33419
    50
          quote name)
boehmes@33419
    51
      else NONE
boehmes@33419
    52
    end
boehmes@33419
    53
boehmes@33419
    54
  fun declare (name, arity) thy =
boehmes@33419
    55
    let val isa_name = isabelle_name name
boehmes@33419
    56
    in
boehmes@33419
    57
      (case lookup_type_name thy isa_name arity of
boehmes@33419
    58
        SOME type_name => ((type_name, false), thy)
boehmes@33419
    59
      | NONE =>
boehmes@33419
    60
          let
boehmes@33419
    61
            val bname = Binding.name isa_name
boehmes@33419
    62
            val args = Name.variant_list [] (replicate arity "'")
boehmes@33419
    63
            val (T, thy') =
boehmes@33419
    64
              ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy
boehmes@33419
    65
            val type_name = fst (Term.dest_Type T)
boehmes@33419
    66
          in ((type_name, true), thy') end)
boehmes@33419
    67
    end
boehmes@33419
    68
boehmes@33419
    69
  fun type_names ((name, _), (new_name, new)) =
boehmes@33419
    70
    if new then SOME (new_name ^ " (was " ^ name ^ ")") else NONE
boehmes@33419
    71
in
boehmes@33419
    72
fun declare_types verbose tys =
boehmes@33419
    73
  fold_map declare tys #-> (fn tds =>
boehmes@33419
    74
  log verbose "Declared types:" (map_filter type_names (tys ~~ tds)) #>
boehmes@33419
    75
  rpair (Symtab.make (map fst tys ~~ map fst tds)))
boehmes@33419
    76
end
boehmes@33419
    77
boehmes@33419
    78
boehmes@33419
    79
boehmes@33419
    80
local
boehmes@33419
    81
  val quote_mixfix =
boehmes@33419
    82
    Symbol.explode #> map
boehmes@33419
    83
      (fn "_" => "'_"
boehmes@33419
    84
        | "(" => "'("
boehmes@33419
    85
        | ")" => "')"
boehmes@33419
    86
        | "/" => "'/"
boehmes@33419
    87
        | s => s) #>
boehmes@33419
    88
    implode
boehmes@33419
    89
boehmes@33419
    90
  fun mk_syntax name i =
boehmes@33419
    91
    let
boehmes@33419
    92
      val syn = quote_mixfix name
boehmes@33419
    93
      val args = concat (separate ",/ " (replicate i "_"))
boehmes@33419
    94
    in
boehmes@33419
    95
      if i = 0 then Mixfix (syn, [], 1000)
boehmes@33419
    96
      else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)
boehmes@33419
    97
    end
boehmes@33419
    98
boehmes@33419
    99
  fun process_attributes T =
boehmes@33419
   100
    let
boehmes@33419
   101
      fun const name = SOME (Const (name, T))
boehmes@33419
   102
boehmes@33419
   103
      fun choose builtin =
boehmes@33419
   104
        (case builtin of
boehmes@33419
   105
          "bvnot" => const @{const_name z3_bvnot}
boehmes@33419
   106
        | "bvand" => const @{const_name z3_bvand}
boehmes@33419
   107
        | "bvor" => const @{const_name z3_bvor}
boehmes@33419
   108
        | "bvxor" => const @{const_name z3_bvxor}
boehmes@33419
   109
        | "bvadd" => const @{const_name z3_bvadd}
boehmes@33419
   110
        | "bvneg" => const @{const_name z3_bvneg}
boehmes@33419
   111
        | "bvsub" => const @{const_name z3_bvsub}
boehmes@33419
   112
        | "bvmul" => const @{const_name z3_bvmul}
boehmes@33419
   113
        | "bvudiv" => const @{const_name z3_bvudiv}
boehmes@33419
   114
        | "bvurem" => const @{const_name z3_bvurem}
boehmes@33419
   115
        | "bvsdiv" => const @{const_name z3_bvsdiv}
boehmes@33419
   116
        | "bvsrem" => const @{const_name z3_bvsrem}
boehmes@33419
   117
        | "bvshl" => const @{const_name z3_bvshl}
boehmes@33419
   118
        | "bvlshr" => const @{const_name z3_bvlshr}
boehmes@33419
   119
        | "bvashr" => const @{const_name z3_bvashr}
boehmes@33419
   120
        | "bvult" => const @{const_name z3_bvult}
boehmes@33419
   121
        | "bvule" => const @{const_name z3_bvule}
boehmes@33419
   122
        | "bvugt" => const @{const_name z3_bvugt}
boehmes@33419
   123
        | "bvuge" => const @{const_name z3_bvuge}
boehmes@33419
   124
        | "bvslt" => const @{const_name z3_bvslt}
boehmes@33419
   125
        | "bvsle" => const @{const_name z3_bvsle}
boehmes@33419
   126
        | "bvsgt" => const @{const_name z3_bvsgt}
boehmes@33419
   127
        | "bvsge" => const @{const_name z3_bvsge}
boehmes@33419
   128
        | "sign_extend" => const @{const_name z3_sign_extend}
boehmes@33419
   129
        | _ => NONE)
boehmes@33419
   130
boehmes@33419
   131
      fun is_builtin att =
boehmes@33419
   132
        (case att of
boehmes@33419
   133
          ("bvbuiltin", [StringValue builtin]) => choose builtin
boehmes@33419
   134
        | ("bvint", [StringValue "ITE"]) => const @{const_name If}
boehmes@33419
   135
        | _ => NONE)
boehmes@33419
   136
    in get_first is_builtin end
boehmes@33419
   137
boehmes@33419
   138
  fun lookup_const thy name T =
boehmes@33465
   139
    let val intern = Sign.intern_const thy name
boehmes@33419
   140
    in
boehmes@33419
   141
      if Sign.declared_const thy intern
boehmes@33419
   142
      then
boehmes@33465
   143
        if Sign.typ_instance thy (T, Sign.the_const_type thy intern)
boehmes@33419
   144
        then SOME (Const (intern, T))
boehmes@33419
   145
        else error ("Boogie: function already declared with different type: " ^
boehmes@33419
   146
          quote name)
boehmes@33419
   147
      else NONE
boehmes@33419
   148
    end
boehmes@33419
   149
boehmes@33419
   150
  fun declare (name, ((Ts, T), atts)) thy =
boehmes@33419
   151
    let val isa_name = isabelle_name name and U = Ts ---> T
boehmes@33419
   152
    in
boehmes@33419
   153
      (case lookup_const thy isa_name U of
boehmes@33419
   154
        SOME t => (((name, t), false), thy)
boehmes@33419
   155
      | NONE => 
boehmes@33419
   156
          (case process_attributes U atts of
boehmes@33419
   157
            SOME t => (((name, t), false), thy)
boehmes@33419
   158
          | NONE =>
boehmes@33419
   159
              thy
boehmes@33419
   160
              |> Sign.declare_const ((Binding.name isa_name, U),
boehmes@33419
   161
                   mk_syntax name (length Ts))
boehmes@33419
   162
              |> apfst (rpair true o pair name)))
boehmes@33419
   163
    end
boehmes@33419
   164
boehmes@33419
   165
  fun const_names ((name, _), ((_, t), new)) =
boehmes@33419
   166
    if new then SOME (fst (Term.dest_Const t) ^ " (as " ^ name ^ ")") else NONE
boehmes@33419
   167
in
boehmes@33419
   168
fun declare_functions verbose fns =
boehmes@33419
   169
  fold_map declare fns #-> (fn fds =>
boehmes@33419
   170
  log verbose "Declared constants:" (map_filter const_names (fns ~~ fds)) #>
boehmes@33419
   171
  rpair (Symtab.make (map fst fds)))
boehmes@33419
   172
end
boehmes@33419
   173
boehmes@33419
   174
boehmes@33419
   175
boehmes@33419
   176
local
boehmes@33419
   177
  fun name_axioms axs =
boehmes@33419
   178
    let fun mk_name idx = "axiom_" ^ string_of_int (idx + 1)
boehmes@33419
   179
    in map_index (fn (idx, t) => (mk_name idx, HOLogic.mk_Trueprop t)) axs end
boehmes@33419
   180
boehmes@33419
   181
  fun only_new_boogie_axioms thy =
boehmes@33419
   182
    let val baxs = map Thm.prop_of (Boogie_Axioms.get (ProofContext.init thy))
boehmes@33419
   183
    in filter_out (member (op aconv) baxs o snd) end
boehmes@33419
   184
in
boehmes@33419
   185
fun add_axioms verbose axs thy =
boehmes@33419
   186
  let val axs' = only_new_boogie_axioms thy (name_axioms axs)
boehmes@33419
   187
  in
boehmes@33419
   188
    thy
boehmes@33419
   189
    |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) axs')
boehmes@33419
   190
    |-> Context.theory_map o fold Boogie_Axioms.add_thm
boehmes@33419
   191
    |> log verbose "The following axioms were added:" (map fst axs')
boehmes@33419
   192
    |> Context.theory_map (fn context => fold Split_VC_SMT_Rules.add_thm
boehmes@33419
   193
         (Boogie_Axioms.get (Context.proof_of context)) context)
boehmes@33419
   194
  end
boehmes@33419
   195
end
boehmes@33419
   196
boehmes@33419
   197
boehmes@33419
   198
boehmes@33445
   199
local
boehmes@33445
   200
  fun burrow_distinct eq f xs =
boehmes@33445
   201
    let
boehmes@33445
   202
      val ys = distinct eq xs
boehmes@33445
   203
      val tab = ys ~~ f ys
boehmes@33445
   204
    in map (the o AList.lookup eq tab) xs end
boehmes@33445
   205
boehmes@33445
   206
  fun indexed names =
boehmes@33445
   207
    let
boehmes@33445
   208
      val dup = member (op =) (duplicates (op =) (map fst names))
boehmes@33445
   209
      fun make_name (n, i) = n ^ (if dup n then "_" ^ string_of_int i else "")
boehmes@33445
   210
    in map make_name names end
boehmes@33445
   211
boehmes@33445
   212
  fun rename idx_names =
boehmes@33445
   213
    idx_names
boehmes@33445
   214
    |> burrow_fst (burrow_distinct (op =)
boehmes@33445
   215
         (map short_name #> ` (duplicates (op =)) #-> Name.variant_list))
boehmes@33445
   216
    |> indexed
boehmes@33445
   217
in
boehmes@33419
   218
fun add_vcs verbose vcs thy =
boehmes@33419
   219
  let
boehmes@33445
   220
    val vcs' =
boehmes@33445
   221
      vcs
boehmes@33445
   222
      |> burrow_fst rename
boehmes@33445
   223
      |> map (apsnd HOLogic.mk_Trueprop)
boehmes@33419
   224
  in
boehmes@33419
   225
    thy
boehmes@33419
   226
    |> Boogie_VCs.set vcs'
boehmes@33419
   227
    |> log verbose "The following verification conditions were loaded:"
boehmes@33419
   228
         (map fst vcs')
boehmes@33419
   229
  end
boehmes@33445
   230
end
boehmes@33419
   231
boehmes@33419
   232
boehmes@33419
   233
boehmes@33419
   234
local
boehmes@33419
   235
  fun mk_bitT i T =
boehmes@33419
   236
    if i = 0
boehmes@33419
   237
    then Type (@{type_name "Numeral_Type.bit0"}, [T])
boehmes@33419
   238
    else Type (@{type_name "Numeral_Type.bit1"}, [T])
boehmes@33419
   239
boehmes@33419
   240
  fun mk_binT size = 
boehmes@33419
   241
    if size = 0 then @{typ "Numeral_Type.num0"}
boehmes@33419
   242
    else if size = 1 then @{typ "Numeral_Type.num1"}
boehmes@33419
   243
    else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
boehmes@33419
   244
in
boehmes@33419
   245
fun mk_wordT size =
boehmes@33419
   246
  if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
boehmes@33419
   247
  else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], [])
boehmes@33419
   248
end
boehmes@33419
   249
boehmes@33419
   250
local
boehmes@33419
   251
  fun dest_binT T =
boehmes@33419
   252
    (case T of
boehmes@33419
   253
      Type (@{type_name "Numeral_Type.num0"}, _) => 0
boehmes@33419
   254
    | Type (@{type_name "Numeral_Type.num1"}, _) => 1
boehmes@33419
   255
    | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
boehmes@33419
   256
    | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
boehmes@33419
   257
    | _ => raise TYPE ("dest_binT", [T], []))
boehmes@33419
   258
in
boehmes@33419
   259
val dest_wordT = (fn
boehmes@33419
   260
    Type (@{type_name "word"}, [T]) => dest_binT T
boehmes@33419
   261
  | T => raise TYPE ("dest_wordT", [T], []))
boehmes@33419
   262
end
boehmes@33419
   263
boehmes@33419
   264
fun mk_arrayT (Ts, T) = Type (@{type_name "fun"}, [HOLogic.mk_tupleT Ts, T])
boehmes@33419
   265
boehmes@33419
   266
boehmes@33419
   267
boehmes@33419
   268
datatype token = Token of string | Newline | EOF
boehmes@33419
   269
boehmes@33419
   270
fun tokenize path =
boehmes@33419
   271
  let
boehmes@33419
   272
    fun blank c = (c = #" " orelse c = #"\t" orelse c = #"\n" orelse c = #"\r")
boehmes@33419
   273
    fun split line (i, tss) = (i + 1,
boehmes@33419
   274
      map (pair i) (map Token (String.tokens blank line) @ [Newline]) :: tss)
boehmes@33419
   275
  in apsnd (flat o rev) (File.fold_lines split path (1, [])) end
boehmes@33419
   276
boehmes@33419
   277
fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
boehmes@33419
   278
boehmes@33419
   279
fun scan_err msg [] = "Boogie (at end of input): " ^ msg
boehmes@33419
   280
  | scan_err msg ((i, _) :: _) = "Boogie (at line " ^ string_of_int i ^ "): " ^
boehmes@33419
   281
      msg
boehmes@33419
   282
boehmes@33419
   283
fun scan_fail msg = Scan.fail_with (scan_err msg)
boehmes@33419
   284
boehmes@33419
   285
fun finite scan path =
boehmes@33419
   286
  let val (i, ts) = tokenize path
boehmes@33419
   287
  in
boehmes@33419
   288
    (case Scan.error (Scan.finite (stopper i) scan) ts of
boehmes@33419
   289
      (x, []) => x
boehmes@33419
   290
    | (_, ts) => error (scan_err "unparsed input" ts))
boehmes@33419
   291
  end
boehmes@33419
   292
boehmes@33419
   293
fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
boehmes@33419
   294
boehmes@33419
   295
fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
boehmes@33497
   296
fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
boehmes@33497
   297
fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st
boehmes@33419
   298
boehmes@33419
   299
fun scan_line key scan =
boehmes@33419
   300
  $$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false)
boehmes@33419
   301
fun scan_line' key = scan_line key (Scan.succeed ())
boehmes@33419
   302
boehmes@33419
   303
fun scan_count scan i =
boehmes@33419
   304
  if i > 0 then scan ::: scan_count scan (i - 1) else Scan.succeed []
boehmes@33419
   305
boehmes@33419
   306
fun scan_lookup kind tab key =
boehmes@33419
   307
  (case Symtab.lookup tab key of
boehmes@33419
   308
    SOME value => Scan.succeed value
boehmes@33419
   309
  | NONE => scan_fail ("undefined " ^ kind ^ ": " ^ quote key))
boehmes@33419
   310
boehmes@33419
   311
fun typ tds =
boehmes@33419
   312
  let
boehmes@33419
   313
    fun tp st =
boehmes@33419
   314
     (scan_line' "bool" >> K @{typ bool} ||
boehmes@33419
   315
      scan_line' "int" >> K @{typ int} ||
boehmes@33419
   316
      scan_line "bv" num >> mk_wordT ||
boehmes@33419
   317
      scan_line "type-con" (str -- num) :|-- (fn (name, arity) =>
boehmes@33419
   318
        scan_lookup "type constructor" tds name -- scan_count tp arity >>
boehmes@33419
   319
        Type) ||
boehmes@33419
   320
      scan_line "array" num :|-- (fn arity =>
boehmes@33419
   321
        scan_count tp (arity - 1) -- tp >> mk_arrayT) ||
boehmes@33419
   322
      scan_fail "illegal type") st
boehmes@33419
   323
  in tp end
boehmes@33419
   324
boehmes@33419
   325
local
boehmes@33419
   326
  fun mk_nary _ t [] = t
boehmes@33419
   327
    | mk_nary f _ (t :: ts) = fold f ts t
boehmes@33419
   328
boehmes@33419
   329
  fun mk_distinct T ts =
boehmes@33419
   330
    Const (@{const_name distinct}, HOLogic.listT T --> @{typ bool}) $ 
boehmes@33419
   331
      HOLogic.mk_list T ts
boehmes@33419
   332
boehmes@33419
   333
  fun quant name f = scan_line name (num -- num -- num) >> pair f
boehmes@33419
   334
  val quants =
boehmes@33419
   335
    quant "forall" HOLogic.all_const ||
boehmes@33419
   336
    quant "exists" HOLogic.exists_const ||
boehmes@33419
   337
    scan_fail "illegal quantifier kind"
boehmes@33445
   338
  fun mk_quant q (n, T) t = q T $ Term.absfree (n, T, t)
boehmes@33419
   339
boehmes@33419
   340
  val patternT = @{typ pattern}
boehmes@33419
   341
  fun mk_pattern _ [] = raise TERM ("mk_pattern", [])
boehmes@33419
   342
    | mk_pattern n [t] = Const (n, Term.fastype_of t --> patternT) $ t
boehmes@33419
   343
    | mk_pattern n (t :: ts) =
boehmes@33419
   344
        let val T = patternT --> Term.fastype_of t --> patternT
boehmes@33419
   345
        in Const (@{const_name andpat}, T) $ mk_pattern n ts $ t end
boehmes@33419
   346
  fun patt n c scan =
boehmes@33419
   347
    scan_line n num :|-- scan_count scan >> (mk_pattern c)
boehmes@33419
   348
  fun pattern scan =
boehmes@33419
   349
    patt "pat" @{const_name pat} scan ||
boehmes@33419
   350
    patt "nopat" @{const_name nopat} scan ||
boehmes@33419
   351
    scan_fail "illegal pattern kind"
boehmes@33419
   352
  fun mk_trigger [] t = t
boehmes@33419
   353
    | mk_trigger ps t = @{term trigger} $ HOLogic.mk_list patternT ps $ t
boehmes@33419
   354
boehmes@33419
   355
  val label_kind =
boehmes@33419
   356
    $$$ "pos" >> K @{term block_at} ||
boehmes@33419
   357
    $$$ "neg" >> K @{term assert_at} ||
boehmes@33419
   358
    scan_fail "illegal label kind"
boehmes@33419
   359
boehmes@33419
   360
  fun mk_select (m, k) =
boehmes@33419
   361
    let
boehmes@33419
   362
      val mT = Term.fastype_of m and kT = Term.fastype_of k
boehmes@33419
   363
      val vT = Term.range_type mT
boehmes@33419
   364
    in Const (@{const_name boogie_select}, mT --> kT --> vT) $ m $ k end
boehmes@33419
   365
boehmes@33419
   366
  fun mk_store ((m, k), v) =
boehmes@33419
   367
    let
boehmes@33419
   368
      val mT = Term.fastype_of m and kT = Term.fastype_of k
boehmes@33419
   369
      val vT = Term.fastype_of v
boehmes@33419
   370
    in
boehmes@33419
   371
      Const (@{const_name boogie_store}, mT --> kT --> vT --> mT) $ m $ k $ v
boehmes@33419
   372
    end
boehmes@33419
   373
  
boehmes@33419
   374
  fun mk_extract ((msb, lsb), t) =
boehmes@33419
   375
    let
boehmes@33419
   376
      val dT = Term.fastype_of t and rT = mk_wordT (msb - lsb)
boehmes@33419
   377
      val nT = @{typ nat}
boehmes@33419
   378
      val mk_nat_num = HOLogic.mk_number @{typ nat}
boehmes@33419
   379
      val m = HOLogic.mk_number @{typ nat}
boehmes@33419
   380
    in
boehmes@33419
   381
      Const (@{const_name boogie_bv_extract}, [nT, nT, dT] ---> rT) $
boehmes@33419
   382
        mk_nat_num msb $ mk_nat_num lsb $ t
boehmes@33419
   383
    end
boehmes@33419
   384
boehmes@33419
   385
  fun mk_concat (t1, t2) =
boehmes@33419
   386
    let
boehmes@33419
   387
      val T1 = Term.fastype_of t1 and T2 = Term.fastype_of t2
boehmes@33419
   388
      val U = mk_wordT (dest_wordT T1 + dest_wordT T2)
boehmes@33419
   389
    in Const (@{const_name boogie_bv_concat}, [T1, T2] ---> U) $ t1 $ t2 end
boehmes@33445
   390
boehmes@33445
   391
  val var_name = str >> prefix "V"
boehmes@33445
   392
  val dest_var_name = unprefix "V"
boehmes@33445
   393
  fun rename_variables t =
boehmes@33445
   394
    let
boehmes@33445
   395
      fun make_context names = Name.make_context (duplicates (op =) names)
boehmes@33445
   396
      fun short_var_name n = short_name (dest_var_name n)
boehmes@33445
   397
boehmes@33445
   398
      val (names, nctxt) =
boehmes@33445
   399
        Term.add_free_names t []
boehmes@33445
   400
        |> map_filter (try (fn n => (n, short_var_name n)))
boehmes@33445
   401
        |> split_list
boehmes@33445
   402
        ||>> (fn names => Name.variants names (make_context names))
boehmes@33445
   403
        |>> Symtab.make o (op ~~)
boehmes@33445
   404
boehmes@33445
   405
      fun rename_free n = the_default n (Symtab.lookup names n)
boehmes@33445
   406
      fun rename_abs n = yield_singleton Name.variants (short_var_name n)
boehmes@33445
   407
boehmes@33445
   408
      fun rename _ (Free (n, T)) = Free (rename_free n, T)
boehmes@33445
   409
        | rename nctxt (Abs (n, T, t)) =
boehmes@33445
   410
            let val (n', nctxt') = rename_abs n nctxt
boehmes@33445
   411
            in Abs (n', T, rename nctxt' t) end
boehmes@33445
   412
        | rename nctxt (t $ u) = rename nctxt t $ rename nctxt u
boehmes@33445
   413
        | rename _ t = t
boehmes@33445
   414
    in rename nctxt t end
boehmes@33419
   415
in
boehmes@33419
   416
fun expr tds fds =
boehmes@33419
   417
  let
boehmes@33419
   418
    fun binop t (u1, u2) = t $ u1 $ u2
boehmes@33419
   419
    fun binexp s f = scan_line' s |-- exp -- exp >> f
boehmes@33419
   420
boehmes@33419
   421
    and exp st =
boehmes@33419
   422
     (scan_line' "true" >> K @{term True} ||
boehmes@33419
   423
      scan_line' "false" >> K @{term False} ||
boehmes@33419
   424
      scan_line' "not" |-- exp >> HOLogic.mk_not ||
boehmes@33419
   425
      scan_line "and" num :|-- scan_count exp >> 
boehmes@33419
   426
        mk_nary (curry HOLogic.mk_conj) @{term True} ||
boehmes@33419
   427
      scan_line "or" num :|-- scan_count exp >>
boehmes@33419
   428
        mk_nary (curry HOLogic.mk_disj) @{term False} ||
boehmes@33419
   429
      binexp "implies" (binop @{term "op -->"}) ||
boehmes@33419
   430
      scan_line "distinct" num :|-- scan_count exp >>
boehmes@33419
   431
        (fn [] => @{term True}
boehmes@33419
   432
          | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
boehmes@33419
   433
      binexp "=" HOLogic.mk_eq ||
boehmes@33445
   434
      scan_line "var" var_name -- typ tds >> Free ||
boehmes@33419
   435
      scan_line "fun" (str -- num) :|-- (fn (name, arity) =>
boehmes@33419
   436
        scan_lookup "constant" fds name -- scan_count exp arity >>
boehmes@33419
   437
        Term.list_comb) ||
boehmes@33419
   438
      quants :|-- (fn (q, ((n, k), i)) =>
boehmes@33445
   439
        scan_count (scan_line "var" var_name -- typ tds) n --
boehmes@33419
   440
        scan_count (pattern exp) k --
boehmes@33419
   441
        scan_count (attribute tds fds) i --
boehmes@33419
   442
        exp >> (fn (((vs, ps), _), t) =>
boehmes@33419
   443
          fold_rev (mk_quant q) vs (mk_trigger ps t))) ||
boehmes@33419
   444
      scan_line "label" (label_kind -- num -- num) -- exp >>
boehmes@33419
   445
        (fn (((l, line), col), t) =>
boehmes@33419
   446
          if line = 0 orelse col = 0 then t
boehmes@33445
   447
          else l $ Free (label_name line col, @{typ bool}) $ t) ||
boehmes@33419
   448
      scan_line "int-num" num >> HOLogic.mk_number @{typ int} ||
boehmes@33419
   449
      binexp "<" (binop @{term "op < :: int => _"}) ||
boehmes@33419
   450
      binexp "<=" (binop @{term "op <= :: int => _"}) ||
boehmes@33419
   451
      binexp ">" (binop @{term "op < :: int => _"} o swap) ||
boehmes@33419
   452
      binexp ">=" (binop @{term "op <= :: int => _"} o swap) ||
boehmes@33419
   453
      binexp "+" (binop @{term "op + :: int => _"}) ||
boehmes@33419
   454
      binexp "-" (binop @{term "op + :: int => _"}) ||
boehmes@33419
   455
      binexp "*" (binop @{term "op + :: int => _"}) ||
boehmes@33419
   456
      binexp "/" (binop @{term boogie_div}) ||
boehmes@33419
   457
      binexp "%" (binop @{term boogie_mod}) ||
boehmes@33419
   458
      scan_line "select" num :|-- (fn arity =>
boehmes@33419
   459
        exp -- (scan_count exp (arity - 1) >> HOLogic.mk_tuple) >>
boehmes@33419
   460
          mk_select) ||
boehmes@33419
   461
      scan_line "store" num :|-- (fn arity =>
boehmes@33419
   462
        exp -- (scan_count exp (arity - 2) >> HOLogic.mk_tuple) -- exp >> 
boehmes@33419
   463
          mk_store) ||
boehmes@33419
   464
      scan_line "bv-num" (num -- num) >> (fn (size, i) =>
boehmes@33419
   465
        HOLogic.mk_number (mk_wordT size) i) ||
boehmes@33419
   466
      scan_line "bv-extract" (num -- num) -- exp >> mk_extract ||
boehmes@33419
   467
      binexp "bv-concat" mk_concat ||
boehmes@33419
   468
      scan_fail "illegal expression") st
boehmes@33445
   469
  in exp >> rename_variables end
boehmes@33419
   470
boehmes@33419
   471
and attribute tds fds =
boehmes@33419
   472
  let
boehmes@33419
   473
    val attr_val = 
boehmes@33419
   474
      scan_line' "expr-attr" |-- expr tds fds >> TermValue ||
boehmes@33419
   475
      scan_line "string-attr" (Scan.repeat1 str) >>
boehmes@33419
   476
        (StringValue o space_implode " ") ||
boehmes@33419
   477
      scan_fail "illegal attribute value"
boehmes@33419
   478
  in
boehmes@33419
   479
    scan_line "attribute" (str -- num) :|-- (fn (name, i) =>
boehmes@33419
   480
      scan_count attr_val i >> pair name) ||
boehmes@33419
   481
    scan_fail "illegal attribute"
boehmes@33419
   482
  end
boehmes@33419
   483
end
boehmes@33419
   484
boehmes@33419
   485
fun type_decls verbose = Scan.depend (fn thy => 
boehmes@33419
   486
  Scan.repeat (scan_line "type-decl" (str -- num -- num) :|-- (fn (ty, i) =>
boehmes@33419
   487
    scan_count (attribute Symtab.empty Symtab.empty) i >> K ty)) >>
boehmes@33419
   488
    (fn tys => declare_types verbose tys thy))
boehmes@33419
   489
boehmes@33419
   490
fun fun_decls verbose tds = Scan.depend (fn thy =>
boehmes@33419
   491
  Scan.repeat (scan_line "fun-decl" (str -- num -- num) :|--
boehmes@33419
   492
    (fn ((name, arity), i) =>
boehmes@33419
   493
      scan_count (typ tds) (arity - 1) -- typ tds --
boehmes@33419
   494
      scan_count (attribute tds Symtab.empty) i >> pair name)) >>
boehmes@33419
   495
    (fn fns => declare_functions verbose fns thy))
boehmes@33419
   496
boehmes@33419
   497
fun axioms verbose tds fds = Scan.depend (fn thy =>
boehmes@33419
   498
  Scan.repeat (scan_line "axiom" num :|-- (fn i =>
boehmes@33419
   499
    expr tds fds --| scan_count (attribute tds fds) i)) >>
boehmes@33419
   500
    (fn axs => (add_axioms verbose axs thy, ())))
boehmes@33419
   501
boehmes@33419
   502
fun var_decls tds fds = Scan.depend (fn thy =>
boehmes@33419
   503
  Scan.repeat (scan_line "var-decl" (str -- num) :|-- (fn (_, i) =>
boehmes@33419
   504
    typ tds -- scan_count (attribute tds fds) i >> K ())) >> K (thy, ()))
boehmes@33419
   505
boehmes@33419
   506
fun vcs verbose tds fds = Scan.depend (fn thy =>
boehmes@33419
   507
  Scan.repeat (scan_line "vc" (str -- num) -- 
boehmes@33419
   508
    (expr tds fds >> Sign.cert_term thy)) >>
boehmes@33419
   509
    (fn vcs => ((), add_vcs verbose vcs thy)))
boehmes@33419
   510
boehmes@33419
   511
fun parse verbose thy = Scan.pass thy
boehmes@33419
   512
 (type_decls verbose :|-- (fn tds =>
boehmes@33419
   513
  fun_decls verbose tds :|-- (fn fds =>
boehmes@33419
   514
  axioms verbose tds fds |--
boehmes@33419
   515
  var_decls tds fds |--
boehmes@33419
   516
  vcs verbose tds fds)))
boehmes@33419
   517
boehmes@33419
   518
fun load_b2i verbose path thy = finite (parse verbose thy) path
boehmes@33419
   519
boehmes@33419
   520
end