ocaml64.drv 14.3 KB
Newer Older
1

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

4
printer "ocaml"
5

6
module BuiltIn
7 8
  syntax type int "Z.t"
end
9

10 11
module HighOrd
  syntax type (->) "%1 -> %2"
12
  syntax val  ( @ )  "%1 %2" prec 4 4 3
13 14
end

15
module option.Option
16
  syntax type      option  "%1 option"
17 18
  syntax val  None    "None"
  syntax val  Some    "Some %1" prec 4 3
19
end
20

21
module Bool
22
  syntax type     bool  "bool"
23 24
  syntax val True  "true"
  syntax val False "false"
25 26
end

27 28
module bool.Ite
  syntax val ite "if %1 then %2 else %3" prec 16 15 15 15
29 30
end

31 32 33 34 35 36
module bool.Bool
  syntax val andb  "%1 && %2"      prec 12 11 12
  syntax val orb   "%1 || %2"      prec 13 12 13
  syntax val xorb  "%1 <> %2"      prec 11 11 10
  syntax val notb  "not %1"        prec 4 3
  syntax val implb "not %1 || %2"  prec 13 3 13
37 38
end

39
module list.List
40
  syntax type     list "%1 list"
41 42
  syntax val Nil  "[]"
  syntax val Cons "%1 :: %2"        prec 9 8 9
43 44
end

45 46
module list.Length
  syntax val length "Z.of_int (List.length %1)" prec 4 3
47 48
end

49 50
module list.Append
  syntax val (++) "List.append %1 %2" prec 4 3 3
51
end
52

53 54
module list.Reverse
  syntax val reverse "List.rev %1" prec 4 3
55 56
end

57 58
module list.RevAppend
  syntax val rev_append "List.rev_append %1 %2" prec 4 3
59 60
end

61 62
module list.Combine
  syntax val combine "List.combine %1 %2" prec 4 3 3
63
end
64

65
module Ref
66
  syntax type     ref      "%1 ref"
67 68
  syntax val contents "!%1" prec 1 0
  syntax val      ref      "ref %1" prec 4 3
69 70 71
end

module ref.Ref
72 73
  syntax val      (!_)     "!%1"      prec 1 0
  syntax val      (:=)     "%1 := %2" prec 15 14 15
74
end
75

76
module ref.Refint
77 78 79 80 81
  syntax val incr "%1 := Z.succ !%1" prec 15 0
  syntax val decr "%1 := Z.pred !%1" prec 15 0
  syntax val (+=) "%1 := Z.add !%1 %2" prec 15 0 0
  syntax val (-=) "%1 := Z.sub !%1 %2" prec 15 0 0
  syntax val ( *= ) "%1 := Z.mul !%1 %2" prec 15 0 0
82
end
83

84
module null.Null
85

86 87 88 89 90
  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)"
91

92
end
93 94

module int.Int
95 96
  syntax val zero "Z.zero"
  syntax val one  "Z.one"
97

98 99 100 101 102
  syntax val (<)   "Z.lt %1 %2" prec 4 3 3
  syntax val (<=)  "Z.leq %1 %2" prec 4 3 3
  syntax val (>)   "Z.gt %1 %2" prec 4 3 3
  syntax val (>=)  "Z.geq %1 %2" prec 4 3 3
  syntax val (=)   "Z.equal %1 %2" prec 4 3 3
103

104 105 106 107
  syntax val  (+)   "Z.add %1 %2" prec 4 3 3
  syntax val  (-)   "Z.sub %1 %2" prec 4 3 3
  syntax val  ( * ) "Z.mul %1 %2" prec 4 3 3
  syntax val  (-_)  "Z.neg %1"    prec 4 3
108 109
end

110 111
module int.Abs
  syntax val abs "Z.abs %1" prec 4 3
112 113
end

114 115 116
module int.MinMax
  syntax val min "Z.min %1 %2" prec 4 3 3
  syntax val max "Z.max %1 %2" prec 4 3 3
117 118 119
end

module int.EuclideanDivision
120 121
  syntax val div "Z.ediv %1 %2" prec 4 3 3
  syntax val mod "Z.erem %1 %2" prec 4 3 3
122 123 124
end

module int.ComputerDivision
125 126
  syntax val div "Z.div %1 %2" prec 4 3 3
  syntax val mod "Z.rem %1 %2" prec 4 3 3
127 128 129 130 131 132 133 134 135 136 137 138 139 140
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"
141
  syntax val       length   "Stack.length %1" prec 4 3
142 143 144 145 146 147 148 149 150 151 152 153 154 155
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"
156
  syntax val       length    "Queue.length %1" prec 4 3
157 158 159 160 161 162 163 164
  syntax val       transfer  "Queue.transfer"
end

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

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

165 166 167 168 169 170 171 172 173 174 175
  syntax val ([])          "%1.(Z.to_int %2)" prec 2 1 3
  syntax val ([]<-)        "%1.(Z.to_int %2) <- %3" prec 15 2 1 15
  syntax val length        "Z.of_int (Array.length %1)" prec 4 3
  syntax val defensive_get "%1.(Z.to_int %2)" prec 2 1 3
  syntax val defensive_set "%1.(Z.to_int %2) <- %3" prec 15 2 1 15
  syntax val make          "Array.make (Z.to_int %1) %2" prec 4 3 3
  syntax val append        "Array.append %1 %2" prec 4 3 3
  syntax val sub           "Array.sub %1 (Z.to_int %2) (Z.to_int %3)" prec 4 3 3 3
  syntax val copy          "Array.copy %1" prec 4 3
  syntax val fill          "Array.fill %1 (Z.to_int %2) (Z.to_int %3) %4" prec 4 3 3 3
  syntax val blit          "Array.blit %1 (Z.to_int %2) %3 (Z.to_int %4) (Z.to_int %5)" prec 4
176 177
end

178
module array.Init
179
  syntax val init "Array.init (Z.to_int %1) (fun i -> %2 (Z.of_int i))" prec 4 3 14
180 181
end

182 183 184 185 186
module matrix.Matrix
  syntax type matrix "%1 array array"

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

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

module mach.int.Int
198 199
  syntax val ( / ) "Z.div %1 %2" prec 4 3 3
  syntax val ( % ) "Z.rem %1 %2" prec 4 3 3
200
end
201

202 203 204 205 206
module mach.int.Int32
  syntax type     int32     "int"

  syntax literal   int32    "%1"

207 208
  syntax val of_int "Z.to_int %1" prec 4 3
  syntax val to_int "Z.of_int %1" prec 4 3
209

210 211 212 213 214 215 216 217 218 219 220 221 222
  syntax val min_int32 "Z.of_int 0x7fff_ffff"
  syntax val max_int32 "Z.of_int (-0x8000_0000)"
  syntax val      ( + )     "%1 + %2"   prec 8 8 7
  syntax val      ( - )     "%1 - %2"   prec 8 8 7
  syntax val      (-_)      "- %1"      prec 5 4
  syntax val      ( * )     "%1 * %2"   prec 8 8 7
  syntax val      ( / )     "%1 / %2"   prec 8 8 7
  syntax val      ( % )     "%1 mod %2" prec 8 8 7
  syntax val      (=)       "%1 = %2"   prec 11 11 10
  syntax val      (<=)      "%1 <= %2"  prec 11 11 10
  syntax val      (<)       "%1 < %2"   prec 11 11 10
  syntax val      (>=)      "%1 >= %2"  prec 11 11 10
  syntax val      (>)       "%1 > %2"   prec 11 11 10
223 224
end

225
module mach.int.Int63
226
  syntax type     int63     "int"
227

228 229
  syntax literal   int63    "%1"

230 231
  syntax val of_int "Z.to_int %1"
  syntax val to_int "Z.of_int %1"
232

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
  syntax val min_int63 "Z.of_int min_int"
  syntax val max_int63 "Z.of_int max_int"
  syntax val min_int   "min_int"
  syntax val max_int   "max_int"
  syntax val zero      "0"
  syntax val one       "1"
  syntax val      ( + )     "%1 + %2"   prec 8 8 7
  syntax val      ( - )     "%1 - %2"   prec 8 8 7
  syntax val      (-_)      "- %1"      prec 5 4
  syntax val      ( * )     "%1 * %2"   prec 8 8 7
  syntax val      ( / )     "%1 / %2"   prec 8 8 7
  syntax val      ( % )     "%1 mod %2" prec 8 8 7
  syntax val      (=)       "%1 = %2"   prec 11 11 10
  syntax val      (<=)      "%1 <= %2"  prec 11 11 10
  syntax val      (<)       "%1 < %2"   prec 11 11 10
  syntax val      (>=)      "%1 >= %2"  prec 11 11 10
  syntax val      (>)       "%1 > %2"   prec 11 11 10
250

251 252
(*  syntax val      to_bv     "(fun x -> x)"
  syntax val      of_bv     "(fun x -> x)"*)
253
end
254

255
module mach.int.Random63
256
  syntax val s             "REMOVE"
257 258 259 260
  syntax val init          "Random.init %1" prec 4 3
  syntax val self_init     "Random.self_init %1" prec 4 3
  syntax val random_bool   "Random.bool %1" prec 4 3
  syntax val random_int63  "Random.int %1" prec 4 3
261 262
end

263 264 265 266
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 *)
267 268 269 270 271
  syntax val create       "REMOVE"
  syntax val init         "REMOVE"
  syntax val self_init    "REMOVE"
  syntax val random_bool  "REMOVE"
  syntax val random_int63 "REMOVE"
272 273
end

274 275
module mach.peano.Peano
  syntax type t      "int"
276 277
  syntax val  to_int "Z.of_int %1" prec 4 3
  syntax val  of_int "Z.to_int %1" prec 4 3
278
  syntax val  zero   "0"
279
  syntax val  one    "1"
280 281 282 283 284 285 286 287 288 289 290 291 292
  syntax val  succ   "%1 + 1"   prec 8 8
  syntax val  pred   "%1 - 1"   prec 8 8
  syntax val  lt     "%1 < %2"  prec 11 11 10
  syntax val  le     "%1 <= %2" prec 11 11 10
  syntax val  gt     "%1 > %2"  prec 11 11 10
  syntax val  ge     "%1 >= %2" prec 11 11 10
  syntax val  eq     "%1 = %2"  prec 11 11 10
  syntax val  ne     "%1 <> %2" prec 11 11 10
  syntax val  neg    "- %1"     prec 5 4
  syntax val  abs    "abs %1"   prec 4 3
  syntax val  add    "%1 + %2"  prec 8 8 7
  syntax val  sub    "%1 - %2"  prec 8 8 7
  syntax val  mul    "%1 * %2"  prec 7 7 6
293 294 295
end

module mach.peano.ComputerDivision
296 297
  syntax val  div    "%1 / %2"  prec 7 7 6
  syntax val  mod    "%1 mod %2" prec 7 7 6
298 299 300
end

module mach.peano.MinMax
301 302
  syntax val  max    "max %1 %2" prec 4 3 3
  syntax val  min    "min %1 %2" prec 4 3 3
303 304
end

305 306 307 308 309 310
module mach.peano.Int63
  syntax val  defensive_to_int63    "%1"
  syntax val  to_int63    "%1"
  syntax val  of_int63    "%1"
end

311 312
module mach.onetime.OneTime
  syntax type t      "int"
313
  syntax val  to_int "Z.of_int %1" prec 4 3
314 315
  syntax val  zero   "0"
  syntax val  one    "1"
316 317 318 319 320 321 322 323
  syntax val  succ   "%1 + 1"   prec 8 8
  syntax val  pred   "%1 - 1"   prec 8 8
  syntax val  lt     "%1 < %2"  prec 11 11 10
  syntax val  le     "%1 <= %2" prec 11 11 10
  syntax val  gt     "%1 > %2"  prec 11 11 10
  syntax val  ge     "%1 >= %2" prec 11 11 10
  syntax val  eq     "%1 = %2"  prec 11 11 10
  syntax val  ne     "%1 <> %2" prec 11 11 10
324 325

  syntax val transfer "%1"
326 327 328 329 330
  syntax val neg      "-%1"     prec 5 4
  syntax val abs      "abs %1"  prec 4 3
  syntax val add      "%1 + %2" prec 8 8 7
  syntax val sub      "%1 - %2" prec 8 8 7
  syntax val split    "(%1-%2, %2)" prec 0 13 13
331 332
end

333 334
module string.Char
  syntax type char "Pervasives.char"
335 336 337 338
  syntax val chr "Char.chr (Z.to_int %1)" prec 4 3
  syntax val code "Z.of_int (Char.code %1)" prec 4 3
  syntax val uppercase "Char.uppercase %1" prec 4 3
  syntax val lowercase "Char.lowercase %1" prec 4 3
339 340 341
end

module io.StdIO
342 343 344
  syntax val print_char "Pervasives.print_char %1" prec 4 3
  syntax val print_int "Pervasives.print_string (Z.to_string %1)" prec 4 3
  syntax val print_newline "Pervasives.print_newline %1" prec 4 3
345 346 347
end

module random.Random
348
  syntax val random_int    "Z.of_int (Random.int (Z.to_int %1))" prec 4 3
349 350
end

351
module mach.int.Refint63
352 353 354 355 356
  syntax val incr "incr %1" prec 4 3
  syntax val decr "decr %1" prec 4 3
  syntax val (+=) "%1 := !%1 + %2" prec 15 0 7
  syntax val (-=) "%1 := !%1 - %2" prec 15 0 7
  syntax val ( *= ) "%1 := !%1 * %2" prec 15 0 7
357 358
end
module mach.int.MinMax63
359 360
  syntax val min "Pervasives.min %1 %2" prec 4 3 3
  syntax val max "Pervasives.max %1 %2" prec 4 3 3
361
end
362

363 364 365 366
module mach.array.Array32
  syntax type      array         "(%1 array)"

  syntax exception OutOfBounds   "Invalid_argument \"index out of bounds\""
367 368 369 370 371 372 373 374 375 376 377 378
  syntax val       make          "Array.make %1 %2" prec 4 3 3
  syntax val       ([])          "%1.(%2)" prec 2 1 18
  syntax val       ([]<-)        "%1.(%2) <- %3" prec 15 1 18 15
  syntax val       defensive_get "%1.(%2)" prec 2 1 18
  syntax val       defensive_set "%1.(%2) <- %3" prec 15 1 18 15
  syntax val       length        "Array.length %1" prec 4
  syntax val       append        "Array.append %1 %2" prec 4
  syntax val       sub           "Array.sub %1 %2 %3" prec 4
  syntax val       copy          "Array.copy %1" prec 4
  syntax val       fill          "Array.fill %1 %2 %3 %4" prec 4
  syntax val       blit          "Array.blit %1 %2 %3 %4 %5" prec 4
  syntax val       self_blit     "Array.blit %1 %2 %1 %3 %4" prec 4
379 380
end

381
module mach.array.Array63
382 383 384
  syntax type      array         "(%1 array)"

  syntax exception OutOfBounds   "Invalid_argument \"index out of bounds\""
385 386 387 388 389 390 391 392 393 394 395 396 397
  syntax val       make          "Array.make %1 %2" prec 4
  syntax val       ([])          "%1.(%2)" prec 2 1 18
  syntax val       ([]<-)        "%1.(%2) <- %3" prec 15 1 18 15
  syntax val       defensive_get "%1.(%2)" prec 2 1 18
  syntax val       defensive_set "%1.(%2) <- %3" prec 15 1 18 15
  syntax val       length        "Array.length %1" prec 4
  syntax val       append        "Array.append %1 %2" prec 4
  syntax val       sub           "Array.sub %1 %2 %3" prec 4
  syntax val       copy          "Array.copy %1" prec 4
  syntax val       fill          "Array.fill %1 %2 %3 %4" prec 4
  syntax val       blit          "Array.blit %1 %2 %3 %4 %5" prec 4
  syntax val       self_blit     "Array.blit %1 %2 %1 %3 %4" prec 4
  syntax val       init          "Array.init %1 %2" prec 4
398
end
399

400 401
module mach.array.ArrayInt63
  syntax type array63 "(int array)"
402 403 404 405 406
  syntax val  make   "Array.make %1 %2" prec 4
  syntax val  ([])   "%1.(%2)" prec 2 1 18
  syntax val  ([]<-) "%1.(%2) <- %3" prec 15 1 18 15
  syntax val  length "Array.length %1" prec 4
  syntax val  copy   "Array.copy %1" prec 4
407
end
408 409 410 411

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

412 413
  (* syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")" *)

414 415 416 417 418 419 420 421 422 423
  syntax val rows     "Array.length %1" prec 4
  syntax val columns  "Array.length %1.(0)" prec 4 1
  syntax val rows          "Array.length %1" prec 4 
  syntax val columns       "Array.length %1.(0)" prec 4 1
  syntax val get           "%1.(%2).(%3)" prec 2 1 18 18
  syntax val set           "%1.(%2).(%3) <- %4" prec 15 1 18 18 15
  syntax val defensive_get "%1.(%2).(%3)" prec 2 1 18 18
  syntax val defensive_set "%1.(%2).(%3) <- %4" prec 15 1 18 18 15
  syntax val make          "Array.make_matrix %1 %2 %3" prec 4
  syntax val copy          "Array.map Array.copy %1" prec 4
424
end
Mário Pereira's avatar
Mário Pereira committed
425 426 427 428 429 430

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

module ocaml.Pervasives
431 432
  syntax exception Exit             "Pervasives.Exit"
  syntax exception Not_found        "Not_found"
433
  syntax exception AssertFailure    "REMOVE"
434
  syntax val       ocaml_assert     "assert %1" prec 4
435
  syntax exception Invalid_argument "Invalid_argument \"\""
436 437
  syntax val       succ             "succ %1" prec 4
  syntax val       pred             "pred %1" prec 4
Mário Pereira's avatar
Mário Pereira committed
438
end