ocaml64.drv 5.28 KB
Newer Older
1

2
(** OCaml driver for 64-bit architecture *)
3 4 5

import "ocaml-gen.drv"

6
(** Machine arithmetic *)
7

8 9 10 11 12 13 14 15 16 17 18 19
module mach.int.Int32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int32     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
20
  syntax val      ( % )     "(mod)"
21 22 23 24 25 26 27 28 29 30 31 32 33
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

module mach.int.UInt32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"
34
  syntax constant zero_unsigned "0"
35 36 37 38 39 40 41

  syntax type     uint32    "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
42
  syntax val      ( % )     "(mod)"
43 44 45 46 47 48
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
49 50 51 52 53 54 55 56 57 58 59 60 61 62


  syntax val      add_with_carry "(fun x y c ->
    let r = x + y + c in
    (r land 0xFFFFFFFF,r lsr 32))"

  syntax val      add3 "(fun x y z ->
    let r = x + y + z in
    (r land 0xFFFFFFFF,r lsr 32))"

  syntax val      mul_double "(fun x y ->
    let r = Int64.mul (Int64.of_int x) (Int64.of_int y) in
    (Int64.to_int (Int64.logand r 0xFFFFFFFFL),Int64.to_int (Int64.shift_right_logical r 32)))"

63 64 65 66 67 68 69 70 71 72 73 74 75 76
end

module mach.int.Int63
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int63     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
77
  syntax val      ( % )     "(mod)"
78 79 80 81 82 83
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
84 85 86

  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"
87 88 89 90 91 92 93 94 95 96 97 98 99 100
end

module mach.int.Int64
  syntax val of_int "Why3__BigInt.to_int64"
  syntax converter of_int "%1L"

  syntax function to_int "(Why3__BigInt.of_int64 %1)"

  syntax type     int64     "Int64.t"
  syntax val      (+)       "Int64.add"
  syntax val      (-)       "Int64.sub"
  syntax val      (-_)      "Int64.neg"
  syntax val      ( * )     "Int64.mul"
  syntax val      (/)       "Int64.div"
101
  syntax val      (%)       "Int64.mod"
102 103 104 105 106 107 108 109
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

110 111 112 113 114 115 116 117 118 119 120 121 122 123
module mach.peano.Peano
  syntax type t "int"
  syntax val to_int "Why3__BigInt.of_int"
  syntax val zero "(fun _ -> 0)"
  syntax val succ "succ"
  syntax val pred "pred"
  syntax val lt "(<)"
  syntax val le "(<=)"
  syntax val gt "(>)"
  syntax val ge "(>=)"
  syntax val eq "(=)"
  syntax val ne "(<>)"
  syntax val neg "(~-)"
  syntax val abs "abs"
124 125 126
  syntax val add "(fun x y _ _ -> x+y)"
  syntax val sub "(fun x y _ _ -> x-y)"
  syntax val mul "(fun x y _ _ -> x*y)"
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
  syntax val of_int "(fun n _ _ -> Why3__BigInt.to_int n)"
  syntax val div "(/)"
  syntax val mod "(mod)"
  syntax val max "max"
  syntax val min "min"
end

module mach.onetime.OneTime
  syntax type t "int"
  syntax val to_int "Why3__BigInt.of_int"
  syntax val zero "(fun _ -> 0)"
  syntax val succ "succ"
  syntax val pred "pred"
  syntax val lt "(<)"
  syntax val le "(<=)"
  syntax val gt "(>)"
  syntax val ge "(>=)"
  syntax val eq "(=)"
  syntax val ne "(<>)"
  syntax val to_peano "(fun x -> x)"
  syntax val transfer "(fun x -> x)"
  syntax val neg "(~-)"
  syntax val abs "abs"
  syntax val add "(+)"
  syntax val sub "(-)"
  syntax val split "(fun x y -> x - y, y)"
end

(** Bit vectors *)

theory bv.BV63
  syntax type      t      "int"
  syntax constant  zero   "0"
  syntax constant  ones    "-1"
  syntax function  bw_and "(%1 land %2)"
  syntax predicate eq     "(%1 = %2)"
  (* TODO ... *)
end

(* TODO
    bv.BV31 ?
    bv.BV32 -> int or int32 ?
    bv.BV64 -> int64 *)

(** Arrays *)
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201

module mach.array.Array32
  syntax type array  "(%1 array)"

  syntax val  make   "Array.make"
  syntax val  ([])   "Array.get"
  syntax val  ([]<-) "Array.set"
  syntax val  length "Array.length"
  syntax val  append "Array.append"
  syntax val  sub    "Array.sub"
  syntax val  copy   "Array.copy"
  syntax val  fill   "Array.fill"
  syntax val  blit   "Array.blit"
  syntax val  self_blit "Array.blit"
end

module mach.array.Array63
  syntax type array  "(%1 array)"

  syntax val  make   "Array.make"
  syntax val  ([])   "Array.get"
  syntax val  ([]<-) "Array.set"
  syntax val  length "Array.length"
  syntax val  append "Array.append"
  syntax val  sub    "Array.sub"
  syntax val  copy   "Array.copy"
  syntax val  fill   "Array.fill"
  syntax val  blit   "Array.blit"
  syntax val  self_blit "Array.blit"
end
202