ocaml64.drv 10.5 KB
Newer Older
1

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

4
printer "ocaml"
5

6 7 8 9
theory BuiltIn
  syntax type int "Z.t"
  syntax predicate  (=)   "%1 = %2"
end
10

11 12 13 14 15
module HighOrd
  syntax type (->) "%1 -> %2"
  syntax val  (@)  "%1 %2"
end

16 17 18 19 20
theory option.Option
  syntax type     option "%1 option"
  syntax function None   "None"
  syntax function Some   "Some %1"
end
21

22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
theory Bool
  syntax type     bool  "bool"
  syntax function True  "true"
  syntax function False "false"
end

theory bool.Ite
  syntax function ite "(if %1 then %2 else %3)"
end

theory bool.Bool
  syntax function andb  "%1 && %2"
  syntax function orb   "%1 || %2"
  syntax function xorb  "%1 <> %2"
  syntax function notb  "not %1"
  syntax function implb "not %1 || %2"
end

theory list.List
  syntax type     list "%1 list"
  syntax function Nil  "[]"
  syntax function Cons "%1 :: %2"
  syntax predicate is_nil "%1 = []"
end

theory list.Length
48
  syntax function length "Z.of_int (List.length %1)"
49 50 51 52 53
end

theory list.Mem
  syntax predicate mem "List.mem %1 %2"
end
54

55 56 57 58 59 60 61 62 63 64 65
theory list.Append
  syntax function (++) "List.append %1 %2"
end

theory list.Reverse
  syntax function reverse "List.rev %1"
end

theory list.RevAppend
  syntax function rev_append "List.rev_append %1 %2"
end
66

67 68 69
theory list.Combine
  syntax function combine "List.combine %1 %2"
end
70

71 72 73 74 75 76 77
module ref.Ref
  syntax type     ref      "%1 ref"
  syntax function contents "!%1"
  syntax val      ref      "ref %1"
  syntax val      (!_)     "!%1"
  syntax val      (:=)     "%1 := %2"
end
78

79
module ref.Refint
Mário Pereira's avatar
Mário Pereira committed
80 81 82 83 84
  syntax val incr "%1 := Z.succ (!%1)"
  syntax val decr "%1 := Z.pred (!%1)"
  syntax val (+=) "%1 := Z.add (!%1) %2"
  syntax val (-=) "%1 := Z.sub (!%1) %2"
  syntax val ( *= ) "%1 := Z.mul (!%1) %2"
85
end
86

87
module null.Null
88

89 90 91 92 93
  syntax type t           "%1"
  syntax val  create_null "(fun () -> Obj.magic (ref 0))"
  syntax val  eq_null     "(==)"
  syntax val  create      "(fun x -> x)"
  syntax val  get         "(fun x -> x)"
94

95
end
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 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 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187

module int.Int
  syntax constant zero "Z.zero"
  syntax constant one  "Z.one"

  syntax predicate (<)   "Z.lt %1 %2"
  syntax predicate (<=)  "Z.leq %1 %2"
  syntax predicate (>)   "Z.gt %1 %2"
  syntax predicate (>=)  "Z.geq %1 %2"
  syntax val       (=)   "Z.equal %1 %2"

  syntax function  (+)   "Z.add %1 %2"
  syntax function  (-)   "Z.sub %1 %2"
  syntax function  ( * ) "Z.mul %1 %2"
  syntax function  (-_)  "Z.neg %1"
end

theory int.Abs
  syntax function abs "Z.abs %1"
end

theory int.MinMax
  syntax function min "Z.min %1 %2"
  syntax function max "Z.max %1 %2"
end

module int.EuclideanDivision
  syntax val div "Z.ediv %1 %2"
  syntax val mod "Z.erem %1 %2"
end

module int.ComputerDivision
  syntax val div "Z.div %1 %2"
  syntax val mod "Z.rem %1 %2"
end

module stack.Stack
  syntax type      t        "%1 Stack.t"
  syntax val       create   "Stack.create"
  syntax val       push     "Stack.push"
  syntax exception Empty    "Stack.Empty"
  syntax val       pop      "Stack.pop"
  syntax val       top      "Stack.top"
  syntax val       safe_pop "Stack.pop"
  syntax val       safe_top "Stack.top"
  syntax val       clear    "Stack.clear"
  syntax val       copy     "Stack.copy"
  syntax val       is_empty "Stack.is_empty"
  syntax val       length   "Z.of_int (Stack.length %1)"
end

module queue.Queue
  syntax type      t         "%1 Queue.t"
  syntax val       create    "Queue.create"
  syntax val       push      "Queue.push"
  syntax exception Empty     "Queue.Empty"
  syntax val       pop       "Queue.pop"
  syntax val       peek      "Queue.peek"
  syntax val       safe_pop  "Queue.pop"
  syntax val       safe_peek "Queue.peek"
  syntax val       clear     "Queue.clear"
  syntax val       copy      "Queue.copy"
  syntax val       is_empty  "Queue.is_empty"
  syntax val       length    "(Z.of_int (Queue.length %1))"
  syntax val       transfer  "Queue.transfer"
end

module array.Array
  syntax type array "%1 array"

  syntax function ([]) "%1.(Z.to_int %2)"

  (* syntax exception OutOfBounds "Why3__Array.OutOfBounds" *) (* FIXME *)

  syntax val ([])          "%1.(Z.to_int %2)"
  syntax val ([]<-)        "%1.(Z.to_int %2) <- %3"
  syntax val length        "Z.of_int (Array.length %1)"
  syntax val defensive_get "%1.(Z.to_int %2)"
  syntax val defensive_set "%1.(Z.to_int %2) <- %3"
  syntax val make          "Array.make (Z.to_int %1) %2"
  syntax val append        "Array.append %1 %2"
  syntax val sub           "Array.sub %1 (Z.to_int %2) (Z.to_int %3)"
  syntax val copy          "Array.copy %1"
  syntax val fill          "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4"
  syntax val blit          "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)"
end

module matrix.Matrix
  syntax type matrix "%1 array array"

  (* syntax exception OutOfBounds "Why3__Matrix.OutOfBounds" *) (* FIXME *)

188 189
  syntax val get           "%1.(Z.to_int %2).(Z.to_int %3)"
  syntax val set           "%1.(Z.to_int %2).(Z.to_int %3) <- %4"
190
  syntax val rows          "Z.of_int (Array.length %1)"
191
  syntax val columns       "Z.of_int (Array.length %1.(0))"
192 193 194 195 196 197 198 199 200 201
  syntax val defensive_get "%1.(Z.to_int %2).(Z.to_int %3)"
  syntax val defensive_set "%1.(Z.to_int %2).(Z.to_int %3) <- %4"
  syntax val make          "Array.make_matrix (Z.to_int %1) (Z.to_int %2) %3"
  syntax val copy          "Array.map Array.copy %1"
end

module mach.int.Int
  syntax val ( / ) "Z.div %1 %2"
  syntax val ( % ) "Z.rem %1 %2"
end
202 203

module mach.int.Int63
Mário Pereira's avatar
Mário Pereira committed
204
  syntax val of_int "Z.to_int %1"
205 206
  syntax converter of_int "%1"

207
  syntax function to_int "Z.of_int %1"
208 209

  syntax type     int63     "int"
Mário Pereira's avatar
Mário Pereira committed
210 211
  syntax constant min_int63 "Z.of_int min_int"
  syntax constant max_int63 "Z.of_int max_int"
212 213
  syntax constant min_int   "min_int"
  syntax constant max_int   "max_int"
214 215
  syntax constant zero      "0"
  syntax constant one       "1"
216 217 218 219 220 221 222 223 224 225 226 227 228
  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"
229

230 231
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
232
end
233

234 235
module mach.int.Random63
  syntax val init          "Random.init %1"
236 237
  syntax val self_init     "Random.self_init %1"
  syntax val random_bool   "Random.bool %1"
238 239 240
  syntax val random_int63  "Random.int %1"
end

241 242 243 244 245 246 247 248 249 250 251
module mach.int.State63
  (* the most appropriate way to do this would be to have
     something similar to [remove] from smt drivers:
     remove val create *)
  syntax val create       "SHOULD_NOT_BE_HERE"
  syntax val init         "SHOULD_NOT_BE_HERE"
  syntax val self_init    "SHOULD_NOT_BE_HERE"
  syntax val random_bool  "SHOULD_NOT_BE_HERE"
  syntax val random_int63 "SHOULD_NOT_BE_HERE"
end

252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
module mach.peano.Peano
  syntax type t      "int"
  syntax val  to_int "Z.of_int %1"
  syntax val  of_int "Z.to_int %1"
  syntax val  zero   "0"
  syntax val  succ   "%1 + 1"
  syntax val  pred   "%1 - 1"
  syntax val  lt     "%1 < %2"
  syntax val  le     "%1 <= %2"
  syntax val  gt     "%1 > %2"
  syntax val  ge     "%1 >= %2"
  syntax val  eq     "%1 = %2"
  syntax val  ne     "%1 <> %2"
  syntax val  neg    "- %1"
  syntax val  abs    "abs %1"
  syntax val  add    "%1 + %2"
  syntax val  sub    "%1 - %2"
  syntax val  mul    "%1 * %2"
  syntax val  div    "%1 / %2"
  syntax val  mod    "%1 mod %2"
  syntax val  max    "max %1 %2"
  syntax val  min    "min %1 %2"
end

276 277 278 279 280 281 282 283 284 285 286
module mach.onetime.OneTime
  syntax type t      "int"
  syntax val  to_int "Z.of_int %1"
  syntax val  zero   "0"
  syntax val  one    "1"
  syntax val  succ   "%1 + 1"
  syntax val  pred   "%1 - 1"
  syntax val  lt     "%1 < %2"
  syntax val  le     "%1 <= %2"
  syntax val  gt     "%1 > %2"
  syntax val  ge     "%1 >= %2"
Mário Pereira's avatar
Mário Pereira committed
287
  syntax val  eq     "%1 = %2"
288 289 290 291 292 293 294 295 296 297 298 299
  syntax val  ne     "%1 <> %2"

  syntax converter to_peano "%1"

  syntax val transfer "%1"
  syntax val neg      "-%1"
  syntax val abs      "abs %1"
  syntax val add      "%1 + %2"
  syntax val sub      "%1 - %2"
  syntax val split    "(%1-%2, %2)"
end

300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
module string.Char
  syntax type char "Pervasives.char"
  syntax val chr "Char.chr (Z.to_int %1)"
  syntax val code "Z.of_int (Char.code %1)"
  syntax function uppercase "Char.uppercase %1"
  syntax function lowercase "Char.lowercase %1"
end

module io.StdIO
  syntax val print_char "Pervasives.print_char %1"
  syntax val print_int "Pervasives.print_int (Z.to_int %1)"
  syntax val print_newline "Pervasives.print_newline"
end

module random.Random
  syntax val random_int    "Z.of_int (Random.int (Z.to_int %1))"
end

318
module mach.int.Refint63
319 320
  syntax val incr "incr %1"
  syntax val decr "decr %1"
Mário Pereira's avatar
Mário Pereira committed
321
  syntax val (+=) "%1 := !%1 + %2" (*"(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"*)
322 323 324 325
  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
Mário Pereira's avatar
Mário Pereira committed
326 327
  syntax val min "Pervasives.min %1 %2"
  syntax val max "Pervasives.max %1 %2"
328
end
329

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

Mário Pereira's avatar
Mário Pereira committed
333 334 335 336 337 338 339 340 341 342
  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"
343
end
344 345 346 347

module mach.matrix.Matrix63
  syntax type matrix "(%1 array array)"

348 349 350 351 352 353 354 355 356 357 358 359
  (* 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 %1"
  syntax val columns       "Array.length m.(0)"
  syntax val get           "m.(%1).(%2)"
  syntax val set           "m.(%1).(%2) <- %3"
  syntax val defensive_get "m.(%1).(%2)"
  syntax val defensive_set "m.(%1).(%2) <- %3"
  syntax val make          "Array.make_matrix %1 %2 %3"
  syntax val copy          "Array.map Array.copy %1"
360
end
Mário Pereira's avatar
Mário Pereira committed
361 362 363 364 365 366

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

module ocaml.Pervasives
367 368 369 370
  syntax exception Exit             "Pervasives.Exit"
  syntax exception Not_found        "Not_found"
  syntax val ocaml_assert           "assert (%1)"
  syntax exception Invalid_argument "Invalid_argument \"\""
371 372
  syntax val succ                   "succ %1"
  syntax val pred                   "pred %1"
Mário Pereira's avatar
Mário Pereira committed
373
end