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