From 7f4bd5d12a01c668abc99b31778b4f730699d26d Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 10 Jan 2024 16:36:54 +0100
Subject: [PATCH] [Kernel] Comments about complexity and behavior of Nat and
Finite functions
---
src/kernel_services/analysis/filter/finite.ml | 1 -
src/kernel_services/analysis/filter/finite.mli | 12 ++++++++++--
src/kernel_services/analysis/filter/nat.mli | 9 +++++++++
3 files changed, 19 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/analysis/filter/finite.ml b/src/kernel_services/analysis/filter/finite.ml
index 0889718c22e..f992d181c71 100644
--- a/src/kernel_services/analysis/filter/finite.ml
+++ b/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
diff --git a/src/kernel_services/analysis/filter/finite.mli b/src/kernel_services/analysis/filter/finite.mli
index 64f56b9c068..1f2a6b986a7 100644
--- a/src/kernel_services/analysis/filter/finite.mli
+++ b/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
diff --git a/src/kernel_services/analysis/filter/nat.mli b/src/kernel_services/analysis/filter/nat.mli
index 4fbc1a1b7c1..9942dfbee1a 100644
--- a/src/kernel_services/analysis/filter/nat.mli
+++ b/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
--
GitLab