[ refactor ] make step a manifest field of Data.Nat.LCG.Generator (#2937)

Author: jamesmckinna

CHANGELOG.md

@@ -24,6 +24,10 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The function `Data.Nat.LCG.step` is now a manifest field of the record type
+  `Generator`, as per the discussion on #2936 and upstream issues/PRs. This is
+  consistent with a minimal API for such LCGs, and should be backwards compatible.
+
 * The types of `Data.Vec.Base.{truncate|padRight}` have been weakened so
   that the argument of type `m ≤ n` is marked as irrelevant. This should be
   backwards compatible, but does change the intensional behaviour of these

src/Data/Nat/PseudoRandom/LCG.agda

@@ -9,9 +9,9 @@
 
 module Data.Nat.PseudoRandom.LCG where
 
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ; _+_; _*_; _^_; NonZero)
 open import Data.Nat.DivMod using (_%_)
-open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Base using (List; iterate)
 
 ------------------------------------------------------------------------
 -- Type and generator
@@ -22,14 +22,13 @@ record Generator : Set where
         modulus        : ℕ
         .{{modulus≢0}} : NonZero modulus
 
-step : Generator → ℕ → ℕ
-step gen@record{} x =
-  let open Generator gen in
-  ((multiplier * x + increment) % modulus)
+  step : ℕ → ℕ
+  step x = (multiplier * x + increment) % modulus
+
+open Generator public using (step)
 
 list : ℕ → Generator → ℕ → List ℕ
-list zero    gen x = []
-list (suc k) gen x = x ∷ list k gen (step gen x)
+list k gen x = iterate (step gen) x k
 
 ------------------------------------------------------------------------
 -- Examples of parameters

src/Data/Nat/PseudoRandom/LCG/Unsafe.agda

@@ -8,16 +8,15 @@
 
 {-# OPTIONS --cubical-compatible --sized-types #-}
 
-open import Codata.Sized.Stream using (Stream; unfold)
+open import Codata.Sized.Stream using (Stream; iterate)
 open import Data.Nat.PseudoRandom.LCG using (Generator; step)
 open import Data.Nat.Base using (ℕ)
-open import Data.Product.Base using (<_,_>)
-open import Function.Base using (id)
+open import Function.Base using (_∘_)
 
 module Data.Nat.PseudoRandom.LCG.Unsafe where
 
 ------------------------------------------------------------------------
 -- An infinite stream of random numbers
 
 stream : Generator → ℕ → Stream ℕ _
-stream gen = unfold < step gen , id >
+stream = iterate ∘ step