blob: 775f1870386649d3ea770064ecdc6d22f793835a (
plain)
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
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
type comparison = Eq | Lt | Gt
type 'a carry = C0 of 'a | C1 of 'a
(*s Unsigned Int *)
type uint
(* Conversion with int *)
val to_int : uint -> int
val of_int : int -> uint
val of_uint : int -> uint
(* Conversion with string *)
val to_string : uint -> string
val of_string : string -> uint
(* logical operations *)
val l_sl : uint -> uint -> uint
val l_sr : uint -> uint -> uint
val l_and : uint -> uint -> uint
val l_or : uint -> uint -> uint
val l_xor : uint -> uint -> uint
(* arithmetic operations *)
val add : uint -> uint -> uint
val sub : uint -> uint -> uint
val mul : uint -> uint -> uint
val mulc : uint -> uint -> uint * uint
val div : uint -> uint -> uint
val rem : uint -> uint -> uint
val lt : uint -> uint -> bool
val le : uint -> uint -> bool
val eq : uint -> uint -> bool
val compare : uint -> uint -> comparison
val head0 : uint -> uint
val tail0 : uint -> uint
val addc : uint -> uint -> uint carry
val addcarryc : uint -> uint -> uint carry
val subc : uint -> uint -> uint carry
val subcarryc : uint -> uint -> uint carry
val diveucl : uint -> uint -> uint * uint
val diveucl_21 : uint -> uint -> uint -> uint * uint
val addmuldiv : uint -> uint -> uint -> uint
val foldi_cont :
(uint -> ('a -> 'b) -> 'a -> 'b) -> uint -> uint -> ('a -> 'b) -> 'a -> 'b
val foldi_down_cont :
(uint -> ('a -> 'b) -> 'a -> 'b) -> uint -> uint -> ('a -> 'b) -> 'a -> 'b
val print_uint : uint -> uint
(*s Persistant array *)
type 'a parray
val of_array : 'a array -> 'a parray
val parray_make : uint -> 'a -> 'a parray
val parray_get : 'a parray -> uint -> 'a
val parray_default : 'a parray -> 'a
val parray_length : 'a parray -> uint
val parray_set : 'a parray -> uint -> 'a -> 'a parray
val parray_copy : 'a parray -> 'a parray
val parray_reroot : 'a parray -> 'a parray
|
