ocaml64.drv 12.9 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
module HighOrd
  syntax type (->) "%1 -> %2"
13
  syntax val  ( @ )  "%1 %2"
14 15
end

16
theory option.Option
17 18 19 20
  syntax type      option  "%1 option"
  syntax function  None    "None"
  syntax function  Some    "Some %1"
  syntax predicate is_none "%1 = None"
21
end
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 48
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
49
  syntax function length "Z.of_int (List.length %1)"
50 51 52 53 54
end

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

56 57 58 59 60 61 62 63 64 65 66
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
67

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

72
module Ref
73 74 75
  syntax type     ref      "%1 ref"
  syntax function contents "!%1"
  syntax val      ref      "ref %1"
76 77 78
end

module ref.Ref
79 80 81
  syntax val      (!_)     "!%1"
  syntax val      (:=)     "%1 := %2"
end
82

83
module ref.Refint
Mário Pereira's avatar
Mário Pereira committed
84 85 86 87 88
  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"
89
end
90

91
module null.Null
92

93 94 95 96 97
  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)"
98

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

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"
148
  syntax val       length   "Stack.length %1"
149 150 151 152 153 154 155 156 157 158 159 160 161 162
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"
163
  syntax val       length    "Queue.length %1"
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
  syntax val       transfer  "Queue.transfer"
end

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

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

185
module array.Init
Mário Pereira's avatar
Mário Pereira committed
186
  syntax val init "Array.init (Z.to_int %1) (fun i -> %2 (Z.of_int i))"
187 188
end

189 190 191 192 193
module matrix.Matrix
  syntax type matrix "%1 array array"

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

194 195
  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"
196
  syntax val rows          "Z.of_int (Array.length %1)"
197
  syntax val columns       "Z.of_int (Array.length %1.(0))"
198 199 200 201 202 203 204 205 206 207
  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
208

209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
module mach.int.Int32
  syntax type     int32     "int"

  syntax literal   int32    "%1"

  syntax val of_int "Z.to_int %1"
  syntax val to_int "Z.of_int %1"

  syntax constant min_int32 "Z.of_int 0x7fff_ffff"
  syntax constant max_int32 "Z.of_int (-0x8000_0000)"
  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      (=)       "%1 = %2"
  syntax val      (<=)      "%1 <= %2"
  syntax val      (<)       "%1 < %2"
  syntax val      (>=)      "%1 >= %2"
  syntax val      (>)       "%1 > %2"
end

232
module mach.int.Int63
233
  syntax type     int63     "int"
234

235 236
  syntax literal   int63    "%1"

237 238
  syntax val of_int "Z.to_int %1"
  syntax val to_int "Z.of_int %1"
239

Mário Pereira's avatar
Mário Pereira committed
240 241
  syntax constant min_int63 "Z.of_int min_int"
  syntax constant max_int63 "Z.of_int max_int"
242 243
  syntax constant min_int   "min_int"
  syntax constant max_int   "max_int"
244 245
  syntax constant zero      "0"
  syntax constant one       "1"
246 247 248 249 250 251 252 253 254 255 256
  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      (=)       "%1 = %2"
  syntax val      (<=)      "%1 <= %2"
  syntax val      (<)       "%1 < %2"
  syntax val      (>=)      "%1 >= %2"
  syntax val      (>)       "%1 > %2"
257

258 259
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
260
end
261

262
module mach.int.Random63
263
  syntax val s             "REMOVE"
264
  syntax val init          "Random.init %1"
265 266
  syntax val self_init     "Random.self_init %1"
  syntax val random_bool   "Random.bool %1"
267 268 269
  syntax val random_int63  "Random.int %1"
end

270 271 272 273
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 *)
274 275 276 277 278
  syntax val create       "REMOVE"
  syntax val init         "REMOVE"
  syntax val self_init    "REMOVE"
  syntax val random_bool  "REMOVE"
  syntax val random_int63 "REMOVE"
279 280
end

281
module set.Fset
282 283 284 285 286 287 288 289 290 291 292 293
  syntax val mem      "REMOVE"
  syntax val (==)     "REMOVE"
  syntax val subset   "REMOVE"
  syntax val is_empty "REMOVE"
  syntax val empty    "REMOVE"
  syntax val add      "REMOVE"
  syntax val remove   "REMOVE"
  syntax val union    "REMOVE"
  syntax val inter    "REMOVE"
  syntax val diff     "REMOVE"
  syntax val choose   "REMOVE"
  syntax val cardinal "REMOVE"
294 295
end

296 297 298 299 300
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"
301
  syntax val  one    "1"
302 303 304 305 306 307 308 309 310 311 312 313 314
  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"
315 316 317
end

module mach.peano.ComputerDivision
318 319
  syntax val  div    "%1 / %2"
  syntax val  mod    "%1 mod %2"
320 321 322
end

module mach.peano.MinMax
323 324 325 326
  syntax val  max    "max %1 %2"
  syntax val  min    "min %1 %2"
end

327 328 329 330 331 332 333 334 335 336 337
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
338
  syntax val  eq     "%1 = %2"
339 340 341 342 343 344 345 346 347 348
  syntax val  ne     "%1 <> %2"

  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

349 350 351 352 353 354 355 356 357 358
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"
MARCHE Claude's avatar
MARCHE Claude committed
359 360
  syntax val print_int "Pervasives.print_string (Z.to_string %1)"
  syntax val print_newline "Pervasives.print_newline %1"
361 362 363 364 365 366
end

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

367
module mach.int.Refint63
368 369
  syntax val incr "incr %1"
  syntax val decr "decr %1"
370 371 372
  syntax val (+=) "%1 := !%1 + %2"
  syntax val (-=) "%1 := !%1 - %2"
  syntax val ( *= ) "%1 := !%1 * %2"
373 374
end
module mach.int.MinMax63
Mário Pereira's avatar
Mário Pereira committed
375 376
  syntax val min "Pervasives.min %1 %2"
  syntax val max "Pervasives.max %1 %2"
377
end
378

379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396
module mach.array.Array32
  syntax type      array         "(%1 array)"

  syntax exception OutOfBounds   "Invalid_argument \"index out of bounds\""
  syntax val       make          "Array.make %1 %2"
  syntax val       ([])          "%1.(%2)"
  syntax val       ([]<-)        "%1.(%2) <- %3"
  syntax val       defensive_get "%1.(%2)"
  syntax val       defensive_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"
end

397
module mach.array.Array63
398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413
  syntax type      array         "(%1 array)"

  syntax exception OutOfBounds   "Invalid_argument \"index out of bounds\""
  syntax val       make          "Array.make %1 %2"
  syntax val       ([])          "%1.(%2)"
  syntax val       ([]<-)        "%1.(%2) <- %3"
  syntax val       defensive_get "%1.(%2)"
  syntax val       defensive_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"
  syntax val       init          "Array.init %1 %2"
414
end
415

416 417 418 419 420 421 422 423
module mach.array.ArrayInt63
  syntax type array63 "(int array)"
  syntax val  make   "Array.make %1 %2"
  syntax val  ([])   "%1.(%2)"
  syntax val  ([]<-) "%1.(%2) <- %3"
  syntax val  length "Array.length %1"
  syntax val  copy   "Array.copy %1"
end
424 425 426 427

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

428 429 430 431 432
  (* 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"
433 434 435 436 437
  syntax val columns       "Array.length %1.(0)"
  syntax val get           "%1.(%2).(%3)"
  syntax val set           "%1.(%2).(%3) <- %4"
  syntax val defensive_get "%1.(%2).(%3)"
  syntax val defensive_set "%1.(%2).(%3) <- %4"
438 439
  syntax val make          "Array.make_matrix %1 %2 %3"
  syntax val copy          "Array.map Array.copy %1"
440
end
Mário Pereira's avatar
Mário Pereira committed
441 442 443 444 445 446

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

module ocaml.Pervasives
447 448
  syntax exception Exit             "Pervasives.Exit"
  syntax exception Not_found        "Not_found"
449
  syntax exception AssertFailure    "REMOVE"
450
  syntax val       ocaml_assert     "assert (%1)"
451
  syntax exception Invalid_argument "Invalid_argument \"\""
452 453
  syntax val       succ             "succ %1"
  syntax val       pred             "pred %1"
Mário Pereira's avatar
Mário Pereira committed
454
end