ocaml64.drv 2.35 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 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 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

(* 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      ( / )     "( / )"
  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)"

  syntax type     uint32    "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
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      ( / )     "( / )"
  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"
  syntax val      eq        "(=)"
  syntax val      ne        "(<>)"
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end