ocaml64.drv 6.49 KB
Newer Older
1

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

import "ocaml-gen.drv"

6
(** Machine arithmetic *)
7

8
module mach.int.Int32
9
  syntax val of_int "Why3extract.Why3__BigInt.to_int"
10 11
  syntax converter of_int "%1"

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

  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
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

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

33
  syntax function to_int "(Why3extract.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
end

module mach.int.Int63
66
  syntax val of_int "Why3extract.Why3__BigInt.to_int"
67 68
  syntax converter of_int "%1"

69
  syntax function to_int "(Why3extract.Why3__BigInt.of_int %1)"
70 71 72 73 74 75 76

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

module mach.int.Int64
101
  syntax val of_int "Why3extract.Why3__BigInt.to_int64"
102 103
  syntax converter of_int "%1L"

104
  syntax function to_int "(Why3extract.Why3__BigInt.of_int64 %1)"
105 106 107 108 109 110 111

  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
module mach.peano.Peano
  syntax type t "int"
123
  syntax val to_int "Why3extract.Why3__BigInt.of_int"
124 125 126 127 128 129 130 131 132 133 134
  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
  syntax val of_int "(fun n _ _ -> Why3extract.Why3__BigInt.to_int n)"
139 140 141 142 143 144 145 146
  syntax val div "(/)"
  syntax val mod "(mod)"
  syntax val max "max"
  syntax val min "min"
end

module mach.onetime.OneTime
  syntax type t "int"
147
  syntax val to_int "Why3extract.Why3__BigInt.of_int"
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
  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
Mário Pereira's avatar
Mário Pereira committed
200
  syntax type array "(%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

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