aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uint31.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2014-04-05 17:49:10 -0400
committerGravatar Maxime Dénès <mail@maximedenes.fr>2014-04-09 01:05:48 -0400
commita231329d7eb0163b97732d4361c25a346f5c09b4 (patch)
treef3cab5a782549d643ad781411df7215e856a3db6 /kernel/uint31.mli
parenteb15c59bb2f79f0154a0c37e43cdf4e90235c053 (diff)
Uint31 support.
Diffstat (limited to 'kernel/uint31.mli')
-rw-r--r--kernel/uint31.mli39
1 files changed, 39 insertions, 0 deletions
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
new file mode 100644
index 000000000..2094df6fa
--- /dev/null
+++ b/kernel/uint31.mli
@@ -0,0 +1,39 @@
+type t
+
+ (* conversion to int *)
+val to_int : t -> int
+val of_int : int -> t
+val of_uint : int -> t
+
+ (* convertion to a string *)
+val to_string : t -> string
+val of_string : string -> t
+
+ (* logical operations *)
+val l_sl : t -> t -> t
+val l_sr : t -> t -> t
+val l_and : t -> t -> t
+val l_xor : t -> t -> t
+val l_or : t -> t -> t
+
+ (* Arithmetic operations *)
+val add : t -> t -> t
+val sub : t -> t -> t
+val mul : t -> t -> t
+val div : t -> t -> t
+val rem : t -> t -> t
+
+ (* Specific arithmetic operations *)
+val mulc : t -> t -> t * t
+val div21 : t -> t -> t -> t * t
+
+ (* comparison *)
+val lt : t -> t -> bool
+val eq : t -> t -> bool
+val le : t -> t -> bool
+val compare : t -> t -> int
+
+ (* head and tail *)
+val head0 : t -> t
+val tail0 : t -> t
+