ocaml-unsafe-int.drv 6.99 KB
Newer Older
1 2 3

(** OCaml driver with Why3 type int being mapped to OCaml type int.

4 5
    This is of course unsafe, yet useful to run your code when you
    have an independent argument for the absence of arithmetic
6 7
    overflows. *)

8
printer "ocaml-unsafe-int"
9 10 11 12 13 14

theory BuiltIn
  syntax type int "int"
  syntax predicate  (=)   "(%1 = %2)"
end

15
(* import "ocaml-no-arith.drv" *)
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

(* int *)

theory int.Int
  syntax constant zero "0"
  syntax constant one  "1"

  syntax predicate (<)  "(%1 < %2)"
  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (>)  "(%1 > %2)"
  syntax predicate (>=) "(%1 >= %2)"

  syntax function (+)   "(%1 + %2)"
  syntax function (-)   "(%1 - %2)"
  syntax function ( * ) "(%1 * %2)"
  syntax function (-_)  "(- %1)"
end

theory int.ComputerDivision
  syntax function div "(%1 / %2)"
  syntax function mod "(%1 mod %2)"
end

(* FIXME: avoid Pervasives using a black list of reserved OCaml names *)

theory int.Abs
  syntax function abs "(Pervasives.abs %1)"
end

theory int.MinMax
  syntax function min "(Pervasives.min %1 %2)"
  syntax function max "(Pervasives.max %1 %2)"
end

50 51 52 53
(* TODO
   - int.EuclideanDivision
   - number.Gcd
*)
54 55

theory int.Power
56 57
  prelude "let rec power x n = if n = 0 then 1 else x * power x (n-1)"
  syntax function power "(power %1 %2)"
58 59 60
end

theory int.Fact
61 62
  prelude "let rec fact n = if n <= 1 then 1 else n * fact (n-1)"
  syntax function fact "(fact %1)"
63 64 65
end

theory int.Fibonacci
66 67
  prelude "let rec fib n = if n <= 1 then n else fib (n-2) + fib (n-1)"
  syntax function fib "(fib %1)"
68 69 70 71
end

(* WhyML *)

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

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

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 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
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"
  syntax val       length   "Stack.length"
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"
  syntax val       length    "Queue.length"
  syntax val       transfer  "Queue.transfer"
end

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

  syntax function ([]) "(%1.(%2))"

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

  syntax val ([])          "Array.unsafe_get"
  syntax val ([]<-)        "Array.unsafe_set"
  syntax val length        "Array.length"
  syntax val defensive_get "Array.get"
  syntax val defensive_set "Array.set"
  syntax val make          "Array.make"
  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"
end

134 135 136 137 138 139 140 141 142
module matrix.Matrix
  syntax type matrix "(%1 array array)"

  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"
  syntax val columns       "(fun m -> Array.length m.(0))"
143 144 145 146
  syntax val get           "(fun m i j -> m.(i).(j))"
  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
  syntax val defensive_get "(fun m i j -> m.(i).(j))"
  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
147 148 149 150
  syntax val make          "Array.make_matrix"
  syntax val copy          "(Array.map Array.copy)"
end

151
module mach.int.Int31
152
  syntax val of_int   "%1"
153 154 155 156 157 158 159 160 161 162

  syntax function to_int "(%1)"

  syntax type     int31     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
  syntax val      ( % )     "(mod)"
163
  syntax val      (=)       "(=)"
164 165 166 167 168
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end
169
module mach.int.Int63
170
  syntax val      of_int   "%1"
171 172 173 174 175 176 177 178 179 180

  syntax function to_int "(%1)"

  syntax type     int63     "int"
  syntax val      ( + )     "( + )"
  syntax val      ( - )     "( - )"
  syntax val      (-_)      "( ~- )"
  syntax val      ( * )     "( * )"
  syntax val      ( / )     "( / )"
  syntax val      ( % )     "(mod)"
181
  syntax val      (=)       "(=)"
182 183 184 185 186
  syntax val      (<=)      "(<=)"
  syntax val      (<)       "(<)"
  syntax val      (>=)      "(>=)"
  syntax val      (>)       "(>)"
end
187 188 189 190 191 192 193 194 195 196 197
module mach.int.Refint63
  syntax val incr "Pervasives.incr"
  syntax val decr "Pervasives.decr"
  syntax val (+=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"
  syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
  syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
end
module mach.int.MinMax63
  syntax val min "Pervasives.min"
  syntax val max "Pervasives.max"
end
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215

(* TODO
   other mach.int.XXX modules *)

module mach.array.Array31
  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
216
module mach.array.Array63
217
  syntax type array   "(%1 array)"
218 219 220 221 222 223 224 225 226 227 228 229

  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
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
module mach.matrix.Matrix63
  syntax type matrix "(%1 array array)"

  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"
  syntax val columns       "(fun m -> Array.length m.(0))"
  syntax val get           "(fun m i j -> m.(i).(j))"
  syntax val set           "(fun m i j v -> m.(i).(j) <- v)"
  syntax val defensive_get "(fun m i j -> m.(i).(j))"
  syntax val defensive_set "(fun m i j v -> m.(i).(j) <- v)"
  syntax val make          "Array.make_matrix"
  syntax val copy          "(Array.map Array.copy)"
end