drivers/ocaml-unsafe-int.drv

   1
   2 (** OCaml driver with Why3 type int being mapped to OCaml type int.
   3
   4     This is of course unsafe, yet useful to run your code when you
   5     have an independent argument for the absence of arithmetic
   6     overflows. *)
   7
   8 printer "ocaml-unsafe-int"
   9
  10 theory BuiltIn
  11   syntax type int "int"
  12   syntax predicate  (=)   "(%1 = %2)"
  13 end
  14
  15 (* import "ocaml-no-arith.drv" *)
  16
  17 (* int *)
  18
  19 theory int.Int
  20   syntax constant zero "0"
  21   syntax constant one  "1"
  22
  23   syntax predicate (<)  "(%1 < %2)"
  24   syntax predicate (<=) "(%1 <= %2)"
  25   syntax predicate (>)  "(%1 > %2)"
  26   syntax predicate (>=) "(%1 >= %2)"
  27
  28   syntax function (+)   "(%1 + %2)"
  29   syntax function (-)   "(%1 - %2)"
  30   syntax function ( * ) "(%1 * %2)"
  31   syntax function (-_)  "(- %1)"
  32 end
  33
  34 theory int.ComputerDivision
  35   syntax function div "(%1 / %2)"
  36   syntax function mod "(%1 mod %2)"
  37 end
  38
  39 (* FIXME: avoid Pervasives using a black list of reserved OCaml names *)
  40
  41 theory int.Abs
  42   syntax function abs "(Pervasives.abs %1)"
  43 end
  44
  45 theory int.MinMax
  46   syntax function min "(Pervasives.min %1 %2)"
  47   syntax function max "(Pervasives.max %1 %2)"
  48 end
  49
  50 (* TODO
  51    - int.EuclideanDivision
  52    - number.Gcd
  53 *)
  54
  55 theory int.Power
  56   prelude "let rec power x n = if n = 0 then 1 else x * power x (n-1)"
  57   syntax function power "(power %1 %2)"
  58 end
  59
  60 theory int.Fact
  61   prelude "let rec fact n = if n <= 1 then 1 else n * fact (n-1)"
  62   syntax function fact "(fact %1)"
  63 end
  64
  65 theory int.Fibonacci
  66   prelude "let rec fib n = if n <= 1 then n else fib (n-2) + fib (n-1)"
  67   syntax function fib "(fib %1)"
  68 end
  69
  70 (* WhyML *)
  71
  72 module Ref
  73   syntax type     ref      "%1 ref"
  74   syntax function contents "!%1"
  75   syntax val      ref      "ref %1"
  76 end
  77
  78 module ref.Ref
  79   syntax val      (!_)     "!%1"
  80   syntax val      (:=)     "%1 := %2"
  81 end
  82
  83 module stack.Stack
  84   syntax type      t        "(%1 Stack.t)"
  85   syntax val       create   "Stack.create"
  86   syntax val       push     "Stack.push"
  87   syntax exception Empty    "Stack.Empty"
  88   syntax val       pop      "Stack.pop"
  89   syntax val       top      "Stack.top"
  90   syntax val       safe_pop "Stack.pop"
  91   syntax val       safe_top "Stack.top"
  92   syntax val       clear    "Stack.clear"
  93   syntax val       copy     "Stack.copy"
  94   syntax val       is_empty "Stack.is_empty"
  95   syntax val       length   "Stack.length"
  96 end
  97
  98 module queue.Queue
  99   syntax type      t         "(%1 Queue.t)"
 100   syntax val       create    "Queue.create"
 101   syntax val       push      "Queue.push"
 102   syntax exception Empty     "Queue.Empty"
 103   syntax val       pop       "Queue.pop"
 104   syntax val       peek      "Queue.peek"
 105   syntax val       safe_pop  "Queue.pop"
 106   syntax val       safe_peek "Queue.peek"
 107   syntax val       clear     "Queue.clear"
 108   syntax val       copy      "Queue.copy"
 109   syntax val       is_empty  "Queue.is_empty"
 110   syntax val       length    "Queue.length"
 111   syntax val       transfer  "Queue.transfer"
 112 end
 113
 114 module array.Array
 115   syntax type array "(%1 array)"
 116
 117   syntax function ([]) "(%1.(%2))"
 118
 119   syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
 120
 121   syntax val ([])          "Array.unsafe_get"
 122   syntax val ([]<-)        "Array.unsafe_set"
 123   syntax val length        "Array.length"
 124   syntax val defensive_get "Array.get"
 125   syntax val defensive_set "Array.set"
 126   syntax val make          "Array.make"
 127   syntax val append        "Array.append"
 128   syntax val sub           "Array.sub"
 129   syntax val copy          "Array.copy"
 130   syntax val fill          "Array.fill"
 131   syntax val blit          "Array.blit"
 132 end
 133
 134 module matrix.Matrix
 135   syntax type matrix "(%1 array array)"
 136
 137   syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
 138
 139   syntax function rows     "(Array.length %1)"
 140   syntax function columns  "(Array.length %1.(0))"
 141   syntax val rows          "Array.length"
 142   syntax val columns       "(fun m -> Array.length m.(0))"
 143   syntax val get           "(fun m i j -> m.(i).(j))"
 144   syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
 145   syntax val defensive_get "(fun m i j -> m.(i).(j))"
 146   syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
 147   syntax val make          "Array.make_matrix"
 148   syntax val copy          "(Array.map Array.copy)"
 149 end
 150
 151 module mach.int.Int31
 152   syntax val of_int   "%1"
 153
 154   syntax function to_int "(%1)"
 155
 156   syntax type     int31     "int"
 157   syntax val      ( + )     "( + )"
 158   syntax val      ( - )     "( - )"
 159   syntax val      (-_)      "( ~- )"
 160   syntax val      ( * )     "( * )"
 161   syntax val      ( / )     "( / )"
 162   syntax val      ( % )     "(mod)"
 163   syntax val      (=)       "(=)"
 164   syntax val      (<=)      "(<=)"
 165   syntax val      (<)       "(<)"
 166   syntax val      (>=)      "(>=)"
 167   syntax val      (>)       "(>)"
 168 end
 169 module mach.int.Int63
 170   syntax val      of_int   "%1"
 171
 172   syntax function to_int "(%1)"
 173
 174   syntax type     int63     "int"
 175   syntax val      ( + )     "( + )"
 176   syntax val      ( - )     "( - )"
 177   syntax val      (-_)      "( ~- )"
 178   syntax val      ( * )     "( * )"
 179   syntax val      ( / )     "( / )"
 180   syntax val      ( % )     "(mod)"
 181   syntax val      (=)       "(=)"
 182   syntax val      (<=)      "(<=)"
 183   syntax val      (<)       "(<)"
 184   syntax val      (>=)      "(>=)"
 185   syntax val      (>)       "(>)"
 186 end
 187 module mach.int.Refint63
 188   syntax val incr "Pervasives.incr"
 189   syntax val decr "Pervasives.decr"
 190   syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
 191   syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
 192   syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
 193 end
 194 module mach.int.MinMax63
 195   syntax val min "Pervasives.min"
 196   syntax val max "Pervasives.max"
 197 end
 198
 199 (* TODO
 200    other mach.int.XXX modules *)
 201
 202 module mach.array.Array31
 203   syntax type array  "(%1 array)"
 204
 205   syntax val  make   "Array.make"
 206   syntax val  ([])   "Array.get"
 207   syntax val  ([]<-) "Array.set"
 208   syntax val  length "Array.length"
 209   syntax val  append "Array.append"
 210   syntax val  sub    "Array.sub"
 211   syntax val  copy   "Array.copy"
 212   syntax val  fill   "Array.fill"
 213   syntax val  blit   "Array.blit"
 214   syntax val  self_blit "Array.blit"
 215 end
 216 module mach.array.Array63
 217   syntax type array   "(%1 array)"
 218
 219   syntax val  make   "Array.make"
 220   syntax val  ([])   "Array.get"
 221   syntax val  ([]<-) "Array.set"
 222   syntax val  length "Array.length"
 223   syntax val  append "Array.append"
 224   syntax val  sub    "Array.sub"
 225   syntax val  copy   "Array.copy"
 226   syntax val  fill   "Array.fill"
 227   syntax val  blit   "Array.blit"
 228   syntax val  self_blit "Array.blit"
 229 end
 230 module mach.matrix.Matrix63
 231   syntax type matrix "(%1 array array)"
 232
 233   syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
 234
 235   syntax function rows     "(Array.length %1)"
 236   syntax function columns  "(Array.length %1.(0))"
 237   syntax val rows          "Array.length"
 238   syntax val columns       "(fun m -> Array.length m.(0))"
 239   syntax val get           "(fun m i j -> m.(i).(j))"
 240   syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
 241   syntax val defensive_get "(fun m i j -> m.(i).(j))"
 242   syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
 243   syntax val make          "Array.make_matrix"
 244   syntax val copy          "(Array.map Array.copy)"
 245 end