ocaml64.drv 6.92 KB
Newer Older
1

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

import "ocaml-gen.drv"

6
(** Machine arithmetic *)
7

Mário Pereira's avatar
Mário Pereira committed
8
(*
9
module mach.int.Int32
10
  syntax val of_int "Why3extract.Why3__BigInt.to_int"
11 12
  syntax converter of_int "%1"

13
  syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
14 15 16 17 18 19 20

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

module mach.int.UInt32
31
  syntax val of_int "Why3extract.Why3__BigInt.to_int"
32 33
  syntax converter of_int "%1"

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

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


  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)))"

64
end
Mário Pereira's avatar
Mário Pereira committed
65
*)
66 67

module mach.int.Int63
Mário Pereira's avatar
Mário Pereira committed
68
  syntax val of_int "Z.to_int %1"
69 70
  syntax converter of_int "%1"

71
  syntax function to_int "Z.of_int %1"
72 73

  syntax type     int63     "int"
Mário Pereira's avatar
Mário Pereira committed
74 75
  syntax constant min_int63 "Z.of_int min_int"
  syntax constant max_int63 "Z.of_int max_int"
76 77 78 79 80 81 82 83 84 85 86 87 88
  syntax val      ( + )     "%1 + %2"
  syntax val      ( - )     "%1 - %2"
  syntax val      (-_)      "- %1"
  syntax val      ( * )     "%1 * %2"
  syntax val      ( / )     "%1 / %2"
  syntax val      ( % )     "%1 mod %2"
  syntax val      eq        "%1 = %2"
  syntax val      ne        "%1 <> %2"
  syntax val      (=)       "%1 = %2"
  syntax val      (<=)      "%1 <= %2"
  syntax val      (<)       "%1 < %2"
  syntax val      (>=)      "%1 >= %2"
  syntax val      (>)       "%1 > %2"
89

90 91
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
92
end
93
module mach.int.Refint63
Mário Pereira's avatar
Mário Pereira committed
94 95 96
  syntax val incr "Pervasives.incr %1"
  syntax val decr "Pervasives.decr %1"
  syntax val (+=) "%1 := !%1 + %2" (*"(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"*)
97 98 99 100 101 102 103
  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
104

Mário Pereira's avatar
Mário Pereira committed
105
(*
106
module mach.int.Int64
107
  syntax val of_int "Why3extract.Why3__BigInt.to_int64"
108 109
  syntax converter of_int "%1L"

110
  syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
111 112 113 114 115 116 117

  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"
118
  syntax val      (%)       "Int64.mod"
119 120 121 122 123 124 125 126
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

127 128
module mach.peano.Peano
  syntax type t "int"
129
  syntax val to_int "Why3extract.Why3__BigInt.of_int"
130 131 132 133 134 135 136 137 138 139 140
  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"
141 142 143
  syntax val add "(fun x y _ _ -> x+y)"
  syntax val sub "(fun x y _ _ -> x-y)"
  syntax val mul "(fun x y _ _ -> x*y)"
144
  syntax val of_int "(fun n _ _ -> Why3extract.Why3__BigInt.to_int n)"
145 146 147 148 149 150 151 152
  syntax val div "(/)"
  syntax val mod "(mod)"
  syntax val max "max"
  syntax val min "min"
end

module mach.onetime.OneTime
  syntax type t "int"
153
  syntax val to_int "Why3extract.Why3__BigInt.of_int"
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
  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 *)

174
(*theory bv.BV63
175 176 177 178 179 180
  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 ... *)
181
end*)
182 183 184 185 186 187 188

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

(** Arrays *)
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203

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
Mário Pereira's avatar
Mário Pereira committed
204
*)
205 206

module mach.array.Array63
Mário Pereira's avatar
Mário Pereira committed
207
  syntax type array "(%1 array)"
208

Mário Pereira's avatar
Mário Pereira committed
209 210 211 212 213 214 215 216 217 218
  syntax val  make   "Array.make %1 %2"
  syntax val  ([])   "Array.get %1 %2"
  syntax val  ([]<-) "Array.set %1 %2 %3"
  syntax val  length "Array.length %1"
  syntax val  append "Array.append %1 %2"
  syntax val  sub    "Array.sub %1 %2 %3"
  syntax val  copy   "Array.copy %1"
  syntax val  fill   "Array.fill %1 %2 %3 %4"
  syntax val  blit   "Array.blit %1 %2 %3 %4 %5"
  syntax val  self_blit "Array.blit %1 %2 %1 %3 %4"
219
end
220

Mário Pereira's avatar
Mário Pereira committed
221
(*
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
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
Mário Pereira's avatar
Mário Pereira committed
238 239 240 241 242 243 244 245
*)

module ocaml.Sys
  syntax val max_array_length "Sys.max_array_length"
end

module ocaml.Pervasives
  syntax exception Exit "Pervasives.Exit"
246
  syntax val ocaml_assert "assert (%1)"
Mário Pereira's avatar
Mário Pereira committed
247
end