ocaml64.drv 6.76 KB
Newer Older
1

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

import "ocaml-gen.drv"

6
(** Machine arithmetic *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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      (>)       "(>)"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84

85 86
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
87
end
88 89 90 91 92 93 94 95 96 97 98
module mach.int.Refint63
  syntax val incr "Pervasives.incr"
  syntax val decr "Pervasives.decr"
  syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
  syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
  syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
end
module mach.int.MinMax63
  syntax val min "Pervasives.min"
  syntax val max "Pervasives.max"
end
99 100 101 102 103 104 105 106 107 108 109 110 111

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"
112
  syntax val      (%)       "Int64.mod"
113 114 115 116 117 118 119 120
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

121 122 123 124 125 126 127 128 129 130 131 132 133 134
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"
135 136 137
  syntax val add "(fun x y _ _ -> x+y)"
  syntax val sub "(fun x y _ _ -> x-y)"
  syntax val mul "(fun x y _ _ -> x*y)"
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
  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 *)

168
(*theory bv.BV63
169 170 171 172 173 174
  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 ... *)
175
end*)
176 177 178 179 180 181 182

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

(** Arrays *)
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199

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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200
  syntax type array63 "(%1 array)"
201 202 203 204 205 206 207 208 209 210 211 212

  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
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
module mach.array.Array63
  syntax type array63 "(%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.matrix.Matrix63
  syntax type matrix "(%1 array array)"

  syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"

  syntax function rows     "(Array.length %1)"
  syntax function columns  "(Array.length %1.(0))"
  syntax val rows          "Array.length"
  syntax val columns       "(fun m -> Array.length m.(0))"
  syntax val get           "(fun m i j -> m.(i).(j))"
  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
  syntax val defensive_get "(fun m i j -> m.(i).(j))"
  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
  syntax val make          "Array.make_matrix"
  syntax val copy          "(Array.map Array.copy)"
end