From 028c7273f9f9ab5f6dca1ca057d9a47c1b5b6440 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 10 Jan 2024 16:20:31 +0100
Subject: [PATCH] [Kernel] Optimizing Nat and Finite
Under the hood, it's just int. But only valid nat and finite can be
built through the given constructors.
---
src/kernel_services/analysis/filter/finite.ml | 40 ++++++-------------
src/kernel_services/analysis/filter/nat.ml | 20 ++++------
src/kernel_services/analysis/filter/nat.mli | 2 +-
3 files changed, 21 insertions(+), 41 deletions(-)
diff --git a/src/kernel_services/analysis/filter/finite.ml b/src/kernel_services/analysis/filter/finite.ml
index 06b52b28a72..0889718c22e 100644
--- a/src/kernel_services/analysis/filter/finite.ml
+++ b/src/kernel_services/analysis/filter/finite.ml
@@ -23,37 +23,21 @@
open Nat.Types
module Types = struct
- type 'n formal = First : 'n succ formal | Next : 'n formal -> 'n succ formal
- type 'n finite = { value : int ; formal : 'n formal }
+ type 'n finite = int
end
open Types
-let first = { value = 0 ; formal = First }
-let next { value ; formal } = { value = value + 1 ; formal = Next formal }
-let to_int { value ; _ } = value
-let ( == ) l r = l.value = r.value
+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
-let rec of_int : type n. n succ nat -> int -> n succ finite = fun limit n ->
- match limit with
- | Succ Zero -> first
- | Succ Succ _ when n <= 0 -> first
- | Succ Succ limit -> next (of_int (Succ limit) (n - 1))
+let of_int : type n. n succ nat -> int -> n succ finite =
+ fun limit n -> min (max 0 n) (Nat.to_int limit)
-let rec of_nat : type n. n succ nat -> n succ finite = function
- | Succ Zero -> first
- | Succ (Succ n) -> next (of_nat (Succ n))
-
-(* We use Obj.magic here to avoid the O(n) long but trivial proof *)
-let weaken : type n. n finite -> n succ finite =
- fun { value ; formal } -> { value ; formal = Obj.magic formal }
-
-(* Non tail-rec to perform the computation in the natural order *)
-let rec fold f n acc =
- match n with
- | { formal = First ; _ } as n -> f n acc
- | { formal = Next formal ; value } as n ->
- f n (fold f (weaken { value = value - 1 ; formal }) acc)
-
-let for_each (type n) acc (n : n nat) (f : n finite -> 'a -> 'a) =
- match n with Zero -> acc | Succ _ as n -> fold f (of_nat n) acc
+let for_each (type n) acc (limit : n nat) (f : n finite -> 'a -> 'a) =
+ let acc = ref acc in
+ for i = 0 to Nat.to_int limit - 1 do acc := f i !acc done ;
+ !acc
diff --git a/src/kernel_services/analysis/filter/nat.ml b/src/kernel_services/analysis/filter/nat.ml
index 79e401c8ae9..c85a25a5a47 100644
--- a/src/kernel_services/analysis/filter/nat.ml
+++ b/src/kernel_services/analysis/filter/nat.ml
@@ -23,29 +23,25 @@
module Types = struct
type zero = |
type 'n succ = |
- type 'n nat = Zero : zero nat | Succ : 'n nat -> 'n succ nat
+ type 'n nat = int
type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
end
open Types
-let zero = Zero
-let one = Succ Zero
-let succ n = (Succ n)
-let prev (Succ n) = n
-
-let to_int n =
- let rec aux : type n. int -> n nat -> int = fun acc ->
- function Zero -> acc | Succ n -> aux (acc + 1) n
- in aux 0 n
+let zero : zero nat = 0
+let one : zero succ nat = 1
+let succ : type n. n nat -> n succ nat = fun n -> n + 1
+let prev : type n. n succ nat -> n nat = fun n -> n - 1
+let to_int : type n. n nat -> int = fun n -> n
let of_int n =
- let next (PositiveOrNull n) = PositiveOrNull (Succ n) in
+ let next (PositiveOrNull n) = PositiveOrNull (succ n) in
let rec aux acc n = if n <= 0 then acc else aux (next acc) (n - 1) in
aux (PositiveOrNull zero) n
let of_strictly_positive_int n =
- let next (StrictlyPositive n) = StrictlyPositive (Succ n) in
+ let next (StrictlyPositive n) = StrictlyPositive (succ n) in
let rec aux acc n = if n <= 1 then acc else aux (next acc) (n - 1) in
aux (StrictlyPositive one) n
diff --git a/src/kernel_services/analysis/filter/nat.mli b/src/kernel_services/analysis/filter/nat.mli
index 38b41ab0918..4fbc1a1b7c1 100644
--- a/src/kernel_services/analysis/filter/nat.mli
+++ b/src/kernel_services/analysis/filter/nat.mli
@@ -23,7 +23,7 @@
module Types : sig
type zero = |
type 'n succ = |
- type 'n nat = Zero : zero nat | Succ : 'n nat -> 'n succ nat
+ type 'n nat
type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
end
--
GitLab