src/HOL/Library/Old_SMT/old_smt_word.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 58825 2065f49da190
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_word.ML
boehmes@41060
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@41060
     3
boehmes@41060
     4
SMT setup for words.
boehmes@41060
     5
*)
boehmes@41060
     6
wenzelm@58825
     7
structure Old_SMT_Word: sig end =
boehmes@41060
     8
struct
boehmes@41060
     9
thomas@47567
    10
open Word_Lib
boehmes@41060
    11
boehmes@41060
    12
(* SMT-LIB logic *)
boehmes@41060
    13
boehmes@41060
    14
fun smtlib_logic ts =
boehmes@41060
    15
  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
boehmes@41060
    16
  then SOME "QF_AUFBV"
boehmes@41060
    17
  else NONE
boehmes@41060
    18
boehmes@41060
    19
boehmes@41060
    20
(* SMT-LIB builtins *)
boehmes@41060
    21
boehmes@41060
    22
local
blanchet@58058
    23
  val smtlibC = Old_SMTLIB_Interface.smtlibC
boehmes@41061
    24
boehmes@41061
    25
  val wordT = @{typ "'a::len word"}
boehmes@41061
    26
boehmes@41060
    27
  fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
boehmes@41060
    28
  fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
boehmes@41060
    29
boehmes@41061
    30
  fun word_typ (Type (@{type_name word}, [T])) =
boehmes@41060
    31
        Option.map (index1 "BitVec") (try dest_binT T)
boehmes@41061
    32
    | word_typ _ = NONE
boehmes@41060
    33
boehmes@41061
    34
  fun word_num (Type (@{type_name word}, [T])) i =
boehmes@41060
    35
        Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
boehmes@41061
    36
    | word_num _ _ = NONE
boehmes@41060
    37
boehmes@41281
    38
  fun if_fixed pred m n T ts =
boehmes@41127
    39
    let val (Us, U) = Term.strip_type T
boehmes@41127
    40
    in
boehmes@41281
    41
      if pred (U, Us) then
boehmes@41281
    42
        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
boehmes@41127
    43
      else NONE
boehmes@41127
    44
    end
boehmes@41061
    45
boehmes@41281
    46
  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
boehmes@41281
    47
  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
boehmes@41281
    48
boehmes@41061
    49
  fun add_word_fun f (t, n) =
wenzelm@46124
    50
    let val (m, _) = Term.dest_Const t
blanchet@58058
    51
    in Old_SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
boehmes@41281
    52
boehmes@41281
    53
  fun hd2 xs = hd (tl xs)
boehmes@41061
    54
boehmes@41281
    55
  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
boehmes@41281
    56
boehmes@41281
    57
  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
boehmes@41281
    58
    | dest_nat t = raise TERM ("not a natural number", [t])
boehmes@41281
    59
boehmes@41281
    60
  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
boehmes@41281
    61
    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
boehmes@41061
    62
boehmes@41281
    63
  fun shift m n T ts =
boehmes@41281
    64
    let val U = Term.domain_type T
boehmes@41281
    65
    in
boehmes@41281
    66
      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
boehmes@41281
    67
        (true, SOME i) =>
boehmes@41281
    68
          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
boehmes@41281
    69
      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
boehmes@41281
    70
    end
boehmes@41060
    71
boehmes@41281
    72
  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
boehmes@41281
    73
boehmes@41281
    74
  fun extract m n T ts =
boehmes@41281
    75
    let val U = Term.range_type (Term.range_type T)
boehmes@41060
    76
    in
boehmes@41281
    77
      (case (try (dest_nat o hd) ts, try dest_wordT U) of
boehmes@41281
    78
        (SOME lb, SOME i) =>
boehmes@41281
    79
          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
boehmes@41060
    80
      | _ => NONE)
boehmes@41060
    81
    end
boehmes@41060
    82
boehmes@41281
    83
  fun mk_extend c ts = Term.list_comb (Const c, ts)
boehmes@41061
    84
boehmes@41281
    85
  fun extend m n T ts =
boehmes@41281
    86
    let val (U1, U2) = Term.dest_funT T
boehmes@41281
    87
    in
boehmes@41281
    88
      (case (try dest_wordT U1, try dest_wordT U2) of
boehmes@41281
    89
        (SOME i, SOME j) =>
boehmes@41281
    90
          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
boehmes@41281
    91
          else NONE
boehmes@41281
    92
      | _ => NONE)
boehmes@41281
    93
    end
boehmes@41060
    94
boehmes@41281
    95
  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
boehmes@41281
    96
boehmes@41281
    97
  fun rotate m n T ts =
boehmes@41281
    98
    let val U = Term.domain_type (Term.range_type T)
boehmes@41127
    99
    in
boehmes@41281
   100
      (case (can dest_wordT U, try (dest_nat o hd) ts) of
boehmes@41281
   101
        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
boehmes@41281
   102
      | _ => NONE)
boehmes@41127
   103
    end
boehmes@41060
   104
in
boehmes@41060
   105
boehmes@41061
   106
val setup_builtins =
blanchet@58058
   107
  Old_SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
boehmes@41281
   108
  fold (add_word_fun if_fixed_all) [
boehmes@41061
   109
    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
boehmes@41061
   110
    (@{term "plus :: 'a::len word => _"}, "bvadd"),
boehmes@41061
   111
    (@{term "minus :: 'a::len word => _"}, "bvsub"),
boehmes@41061
   112
    (@{term "times :: 'a::len word => _"}, "bvmul"),
boehmes@41061
   113
    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
boehmes@41061
   114
    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
boehmes@41061
   115
    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
boehmes@41061
   116
    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
boehmes@41061
   117
    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
boehmes@41061
   118
  fold (add_word_fun shift) [
boehmes@41061
   119
    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
boehmes@41061
   120
    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
boehmes@41061
   121
    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
boehmes@41061
   122
  add_word_fun extract
boehmes@41061
   123
    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
boehmes@41061
   124
  fold (add_word_fun extend) [
boehmes@41061
   125
    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
boehmes@41061
   126
    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
boehmes@41061
   127
  fold (add_word_fun rotate) [
boehmes@41061
   128
    (@{term word_rotl}, "rotate_left"),
boehmes@41061
   129
    (@{term word_rotr}, "rotate_right") ] #>
boehmes@41281
   130
  fold (add_word_fun if_fixed_args) [
boehmes@41061
   131
    (@{term "less :: 'a::len word => _"}, "bvult"),
boehmes@41061
   132
    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
boehmes@41061
   133
    (@{term word_sless}, "bvslt"),
boehmes@41061
   134
    (@{term word_sle}, "bvsle") ]
boehmes@41060
   135
boehmes@41060
   136
end
boehmes@41060
   137
boehmes@41060
   138
boehmes@41060
   139
(* setup *)
boehmes@41060
   140
wenzelm@58825
   141
val _ = 
wenzelm@58825
   142
  Theory.setup
wenzelm@58825
   143
    (Context.theory_map
wenzelm@58825
   144
      (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins))
boehmes@41060
   145
boehmes@41060
   146
end