stdlib/ocaml.mlw

   1 (** {1 General functions related to OCaml extraction} *)
   2
   3 module Sys
   4
   5   use int.Int
   6   use mach.int.Int63
   7
   8   val constant max_array_length : int63
   9   axiom non_neg_max_array_length : 0 <= max_array_length
  10
  11 end
  12
  13 module Exceptions
  14
  15   exception Exit
  16   exception Not_found
  17   exception Invalid_argument string
  18
  19 end
  20
  21 module Pervasives
  22
  23   use int.Int
  24   use mach.int.Int63
  25
  26   use export Exceptions
  27
  28   val succ (x: int63) : int63
  29     requires { [@expl:integer overflow] in_bounds (to_int x + 1) }
  30     ensures  { to_int result = to_int x + 1 }
  31
  32   val pred (x: int63) : int63
  33     requires { [@expl:integer overflow] in_bounds (to_int x - 1) }
  34     ensures  { to_int result = to_int x - 1 }
  35
  36   exception AssertFailure
  37
  38   val ocaml_assert (_b: bool) : unit
  39     raises { AssertFailure }
  40
  41 end
  42
  43 module OCaml
  44
  45   use export int.Int
  46   use mach.int.Int63 as Int63
  47   use export int.MinMax
  48   use export option.Option
  49   use export Pervasives
  50   use Sys
  51
  52   use mach.array.Array63 as Array
  53   type array 'a = Array.array 'a
  54
  55   type int63 = Int63.int63
  56
  57   let function to_int (n: Int63.int63) : int = Int63.to_int n
  58
  59 end