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