[ new ] System.Random bindings

CHANGELOG.md

@@ -125,6 +125,12 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* `System.Random` bindings:
+  ```agda
+  System.Random.Primitive
+  System.Random
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -259,6 +265,11 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
+* In `Data.Float.Base`:
+  ```agda
+  _≤_ : Rel Float _
+  ```
+
 * In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
@@ -378,6 +389,12 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  ```
+
+* In `Data.Word.Base`:
+  ```agda
+  _≤_ : Rel Word64 zero
+  ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
   ```

GenerateEverything.hs

@@ -76,6 +76,8 @@ unsafeModules = map modToFile
   , "System.FilePath.Posix.Primitive"
   , "System.Process"
   , "System.Process.Primitive"
+  , "System.Random"
+  , "System.Random.Primitive"
   , "Test.Golden"
   , "Text.Pretty.Core"
   , "Text.Pretty"

src/Data/Float/Base.agda

@@ -8,11 +8,12 @@
 
 module Data.Float.Base where
 
-open import Relation.Binary.Core using (Rel)
+open import Data.Bool.Base using (T)
 import Data.Word.Base as Word
 import Data.Maybe.Base as Maybe
 open import Function.Base using (_on_; _∘_)
 open import Agda.Builtin.Equality
+open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------
 -- Re-export built-ins publically
@@ -69,3 +70,8 @@ infix 4 _≈_
 
 _≈_ : Rel Float _
 _≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord
+
+
+infix 4 _≤_
+_≤_ : Rel Float _
+x ≤ y = T (x ≤ᵇ y)

src/Data/Word/Base.agda

@@ -31,3 +31,7 @@ _≈_ = _≡_ on toℕ
 infix 4 _<_
 _<_ : Rel Word64 zero
 _<_ = ℕ._<_ on toℕ
+
+infix 4 _≤_
+_≤_ : Rel Word64 zero
+_≤_ = ℕ._≤_ on toℕ

src/System/Random.agda

@@ -0,0 +1,158 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- *Pseudo-random* number generation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --guardedness #-}
+
+module System.Random where
+
+import System.Random.Primitive as Prim
+
+open import Data.Bool.Base using (T)
+open import Data.Nat.Base using (ℕ) hiding (module ℕ)
+open import Foreign.Haskell.Pair using (_,_)
+open import Function.Base using (_$_)
+open import IO.Base using (IO; lift; lift!; _>>=_; pure)
+import IO.Effectful as IO
+open import Level using (0ℓ; suc; _⊔_; lift)
+open import Relation.Binary.Core using (Rel)
+
+------------------------------------------------------------------------
+-- Ranged generation shall return proofs
+
+record InBounds {a r} {A : Set a} (_≤_ : Rel A r) (lo hi : A) : Set (a ⊔ r) where
+  constructor _∈[_,_]
+  field
+    value : A
+    .isLowerBound : lo ≤ value
+    .isUpperBound : value ≤ hi
+
+RandomRIO : ∀ {a r} {A : Set a} (_≤_ : Rel A r) → Set (suc (a ⊔ r))
+RandomRIO {A = A} _≤_ = (lo hi : A) → .(lo ≤ hi) → IO (InBounds _≤_ lo hi)
+
+------------------------------------------------------------------------
+-- Instances
+
+module Char where
+
+  open import Data.Char.Base using (Char; _≤_)
+
+  randomIO : IO Char
+  randomIO = lift Prim.randomIO-Char
+
+  randomRIO : RandomRIO _≤_
+  randomRIO lo hi _ = do
+    value ← lift (Prim.randomRIO-Char (lo , hi))
+    pure (value ∈[ trustMe , trustMe ])
+    where postulate trustMe : ∀ {A} → A
+
+module Float where
+
+  open import Data.Float.Base using (Float; _≤_)
+
+  randomIO : IO Float
+  randomIO = lift Prim.randomIO-Float
+
+  randomRIO : RandomRIO _≤_
+  randomRIO lo hi _ = do
+    value ← lift (Prim.randomRIO-Float (lo , hi))
+    pure (value ∈[ trustMe , trustMe ])
+    where postulate trustMe : ∀ {A} → A
+
+module ℤ where
+
+  open import Data.Integer.Base using (ℤ; _≤_)
+
+  randomIO : IO ℤ
+  randomIO = lift Prim.randomIO-Int
+
+  randomRIO : RandomRIO _≤_
+  randomRIO lo hi _ = do
+    value ← lift (Prim.randomRIO-Int (lo , hi))
+    pure (value ∈[ trustMe , trustMe ])
+    where postulate trustMe : ∀ {A} → A
+
+module ℕ where
+
+  open import Data.Nat.Base using (ℕ; _≤_)
+
+  randomIO : IO ℕ
+  randomIO = lift Prim.randomIO-Nat
+
+  randomRIO : RandomRIO _≤_
+  randomRIO lo hi _ = do
+    value ← lift (Prim.randomRIO-Nat (lo , hi))
+    pure (value ∈[ trustMe , trustMe ])
+    where postulate trustMe : ∀ {A} → A
+
+module Word64 where
+
+  open import Data.Word.Base using (Word64; _≤_)
+
+  randomIO : IO Word64
+  randomIO = lift Prim.randomIO-Word64
+
+  randomRIO : RandomRIO _≤_
+  randomRIO lo hi _ = do
+    value ← lift (Prim.randomRIO-Word64 (lo , hi))
+    pure (value ∈[ trustMe , trustMe ])
+    where postulate trustMe : ∀ {A} → A
+
+module Fin where
+
+  open import Data.Nat.Base as ℕ using (suc; NonZero; z≤n; s≤s)
+  import Data.Nat.Properties as ℕ
+  open import Data.Fin.Base using (Fin; _≤_; fromℕ<; toℕ)
+  import Data.Fin.Properties as Fin
+
+  randomIO : ∀ {n} → .{{NonZero n}} → IO (Fin n)
+  randomIO {n = n@(suc _)} = do
+    suc k ∈[ lo≤k , k≤hi ] ← ℕ.randomRIO 1 n (s≤s z≤n)
+    pure (fromℕ< k≤hi)
+
+  toℕ-cancel-InBounds : ∀ {n} {lo hi : Fin n} →
+                        InBounds ℕ._≤_ (toℕ lo) (toℕ hi) →
+                        InBounds _≤_ lo hi
+  toℕ-cancel-InBounds {n} {lo} {hi} (k ∈[ toℕlo≤k , k≤toℕhi ]) =
+    let
+      .k<n  : k ℕ.< n
+      k<n = ℕ.≤-<-trans k≤toℕhi (Fin.toℕ<n hi)
+
+      .lo≤k : lo ≤ fromℕ< k<n
+      lo≤k = Fin.toℕ-cancel-≤ $ let open ℕ.≤-Reasoning in begin
+        toℕ lo           ≤⟨ toℕlo≤k ⟩
+        k                ≡⟨ Fin.toℕ-fromℕ< k<n ⟨
+        toℕ (fromℕ< k<n) ∎
+
+      .k≤hi : fromℕ< k<n ≤ hi
+      k≤hi = Fin.toℕ-cancel-≤ $ let open ℕ.≤-Reasoning in begin
+        toℕ (fromℕ< k<n) ≡⟨ Fin.toℕ-fromℕ< k<n ⟩
+        k                ≤⟨ k≤toℕhi ⟩
+        toℕ hi           ∎
+
+    in fromℕ< k<n ∈[ lo≤k , k≤hi ]
+
+  randomRIO : ∀ {n} → RandomRIO {A = Fin n} _≤_
+  randomRIO {n} lo hi p = do
+    k ← ℕ.randomRIO (toℕ lo) (toℕ hi) (Fin.toℕ-mono-≤ p)
+    pure (toℕ-cancel-InBounds k)
+
+module List {a} {A : Set a} (rIO : IO A) where
+
+  open import Data.List.Base using (List; replicate)
+  open import Data.List.Effectful using (module TraversableA)
+
+  randomIO : IO (List A)
+  randomIO = do
+    lift n ← lift! ℕ.randomIO
+    TraversableA.sequenceA IO.applicative $ replicate n rIO
+
+module Vec {a} {A : Set a} (rIO : IO A) (n : ℕ) where
+
+  open import Data.Vec.Base using (Vec; replicate)
+  open import Data.Vec.Effectful using (module TraversableA)
+
+  randomIO : IO (Vec A n)
+  randomIO = TraversableA.sequenceA IO.applicative $ replicate n rIO

src/System/Random/Primitive.agda

@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Primitive System.Random simple bindings to Haskell functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible #-}
+
+module System.Random.Primitive where
+
+open import Agda.Builtin.IO using (IO)
+open import Agda.Builtin.Char using (Char)
+open import Agda.Builtin.Float using (Float)
+open import Agda.Builtin.Int using (Int)
+open import Agda.Builtin.Nat using (Nat)
+open import Agda.Builtin.Word using (Word64)
+open import Foreign.Haskell.Pair using (Pair)
+
+postulate
+  randomIO-Char : IO Char
+  randomRIO-Char : Pair Char Char → IO Char
+  randomIO-Int : IO Int
+  randomRIO-Int : Pair Int Int → IO Int
+  randomIO-Float : IO Float
+  randomRIO-Float : Pair Float Float → IO Float
+  randomIO-Nat : IO Nat
+  randomRIO-Nat : Pair Nat Nat → IO Nat
+  randomIO-Word64 : IO Word64
+  randomRIO-Word64 : Pair Word64 Word64 → IO Word64
+
+{-# FOREIGN GHC import System.Random #-}
+
+{-# COMPILE GHC randomIO-Char = randomIO #-}
+{-# COMPILE GHC randomRIO-Char = randomRIO #-}
+{-# COMPILE GHC randomIO-Int = randomIO #-}
+{-# COMPILE GHC randomRIO-Int = randomRIO #-}
+{-# COMPILE GHC randomIO-Float = randomIO #-}
+{-# COMPILE GHC randomRIO-Float = randomRIO #-}
+{-# COMPILE GHC randomIO-Nat = randomIO #-}
+{-# COMPILE GHC randomRIO-Nat = randomRIO #-}
+{-# COMPILE GHC randomIO-Word64 = randomIO #-}
+{-# COMPILE GHC randomRIO-Word64 = randomRIO #-}