ocaml64.drv 6.87 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
68
  syntax val of_int "Why3extract.Why3__BigInt.to_int"
69 70
  syntax converter of_int "%1"

71
  syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
72 73

  syntax type     int63     "int"
Mário Pereira's avatar
Mário Pereira committed
74 75 76 77 78 79 80 81 82 83 84 85 86
  syntax val      ( + )     "( + ) %1 %2"
  syntax val      ( - )     "( - ) %1 %2"
  syntax val      (-_)      "( ~- ) %1 %2"
  syntax val      ( * )     "( * ) %1 %2"
  syntax val      ( / )     "( / ) %1 %2"
  syntax val      ( % )     "(mod) %1 %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"
87

88 89
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
90
end
91
module mach.int.Refint63
Mário Pereira's avatar
Mário Pereira committed
92 93 94
  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))"*)
95 96 97 98 99 100 101
  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
102

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

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

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

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

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

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

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

(** Arrays *)
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
Mário Pereira's avatar
Mário Pereira committed
202
*)
203 204

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

Mário Pereira's avatar
Mário Pereira committed
207 208 209 210 211 212 213 214 215 216
  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"
217
end
218

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

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

module ocaml.Pervasives
  syntax exception Exit "Pervasives.Exit"
end