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
|
(** {1 General functions related to OCaml extraction} *)
module Sys
use int.Int
use mach.int.Int63
val constant max_array_length : int63
axiom non_neg_max_array_length : 0 <= max_array_length
end
module Exceptions
exception Exit
exception Not_found
exception Invalid_argument string
end
module Pervasives
use int.Int
use mach.int.Int63
use export Exceptions
val succ (x: int63) : int63
requires { [@expl:integer overflow] in_bounds (to_int x + 1) }
ensures { to_int result = to_int x + 1 }
val pred (x: int63) : int63
requires { [@expl:integer overflow] in_bounds (to_int x - 1) }
ensures { to_int result = to_int x - 1 }
exception AssertFailure
val ocaml_assert (_b: bool) : unit
raises { AssertFailure }
end
module OCaml
use export int.Int
use mach.int.Int63 as Int63
use export int.MinMax
use export option.Option
use export Pervasives
use Sys
use mach.array.Array63 as Array
type array 'a = Array.array 'a
type int63 = Int63.int63
let function to_int (n: Int63.int63) : int = Int63.to_int n
end
|
