[Kernel] Comments about complexity and behavior of Nat and Finite functions

src/kernel_services/analysis/filter/finite.ml

@@ -30,7 +30,6 @@ open Types
 
 let first : type n. n succ finite = 0
 let next : type n. n finite -> n succ finite = fun n -> n + 1
-let weaken : type n. n finite -> n succ finite = fun n -> n
 let ( == ) : type n. n finite -> n finite -> bool = fun l r -> l = r
 let to_int : type n. n finite -> int = fun n -> n
 

src/kernel_services/analysis/filter/finite.mli

@@ -23,14 +23,22 @@
 open Nat.Types
 
 module Types : sig type 'n finite end
-
 open Types
 
 val first : 'n succ finite
 val next : 'n finite -> 'n succ finite
 val ( == ) : 'n finite -> 'n finite -> bool
 
-val weaken : 'n finite -> 'n succ finite
+(* The call [of_int limit n] returns a finite value representing the n-nd
+   element of a finite set of cardinal limit. If n is strictly negative then it
+   returns the first element. If n is greater or equal to the limit then it
+   returns the last element. This function complexity is O(1). *)
 val of_int : 'n succ nat -> int -> 'n succ finite
+
+(* The call [to_int n] returns an integer equal to n. This function complexity
+   is O(1). *)
 val to_int : 'n finite -> int
+
+(* The call [for_each acc limit f] folds over each finite elements of a set of
+   cardinal limit, computing f at each step. The function complexity is O(n). *)
 val for_each : 'a -> 'n nat -> ('n finite -> 'a -> 'a) -> 'a

src/kernel_services/analysis/filter/nat.mli

@@ -34,6 +34,15 @@ val zero : zero nat
 val one  : zero succ nat
 val succ : 'n nat -> 'n succ nat
 val prev : 'n succ nat -> 'n nat
+
+(* The call [to_int n] returns an integer equal to n. This function complexity
+   is O(1). *)
 val to_int : 'n nat -> int
+
+(* Returns a positive or null natural. If the given parameter is stricly
+   negative then 0 is returned. This function complexity is O(n). *)
 val of_int : int -> positive_or_null
+
+(* Returns a strictly positive natural. If the given parameter is less or equal
+   than zero, then 1 is returned. This function complexity is O(n). *)
 val of_strictly_positive_int : int -> strictly_positive