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