[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

@@ -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

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

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