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