ocaml64.drv 3.74 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

(* OCaml driver for 64-bit architecture *)

import "ocaml-gen.drv"

module mach.int.Int32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int32     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
18
  syntax val      ( % )     "(mod)"
19 20 21 22 23 24 25 26 27 28 29 30 31
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

module mach.int.UInt32
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"
32
  syntax constant zero_unsigned "0"
33 34 35 36 37 38 39

  syntax type     uint32    "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
40
  syntax val      ( % )     "(mod)"
41 42 43 44 45 46
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
47 48 49 50 51 52 53 54 55 56 57 58 59 60


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

61 62 63 64 65 66 67 68 69 70 71 72 73 74
end

module mach.int.Int63
  syntax val of_int "Why3__BigInt.to_int"
  syntax converter of_int "%1"

  syntax function to_int "(Why3__BigInt.of_int %1)"

  syntax type     int63     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
75
  syntax val      ( % )     "(mod)"
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

module mach.int.Int64
  syntax val of_int "Why3__BigInt.to_int64"
  syntax converter of_int "%1L"

  syntax function to_int "(Why3__BigInt.of_int64 %1)"

  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"
96
  syntax val      (%)       "Int64.mod"
97 98 99 100 101 102 103 104
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end

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

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