[ new ] System.Random bindings (#2368)

* [ new ] System.Random bindings

* [ more ] Show functions, test

* [ fix ] Nat bug, more random generators, test case

* [ fix ] missing file + local gitignore

* [ fix ] forgot to update the CHANGELOG

Author: gallais

CHANGELOG.md

@@ -125,6 +125,19 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* `System.Random` bindings:
+  ```agda
+  System.Random.Primitive
+  System.Random
+  ```
+
+* Show modules:
+  ```agda
+  Data.List.Show
+  Data.Vec.Show
+  Data.Vec.Bounded.Show
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -265,6 +278,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
@@ -385,6 +403,13 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  between : String → String → 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/List/Show.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Show where
+
+open import Data.List.Base using (List; map)
+open import Data.String.Base using (String; between; intersperse)
+open import Function.Base using (_∘_)
+
+show : ∀ {a} {A : Set a} → (A → String) → (List A → String)
+show s = between "[" "]" ∘ intersperse ", " ∘ map s

src/Data/String/Base.agda

@@ -102,11 +102,14 @@ unwords = intersperse " "
 unlines : List String → String
 unlines = intersperse "\n"
 
+between : String → String → String → String
+between left right middle = left ++ middle ++ right
+
 parens : String → String
-parens s = "(" ++ s ++ ")"
+parens = between "(" ")"
 
 braces : String → String
-braces s = "{" ++ s ++ "}"
+braces = between "{" "}"
 
 -- append that also introduces spaces, if necessary
 infixr 5 _<+>_

src/Data/Vec/Bounded/Show.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing bounded vectors
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Bounded.Show where
+
+open import Data.String.Base using (String)
+open import Data.Vec.Bounded.Base using (Vec≤)
+import Data.Vec.Show as Vec
+open import Function.Base using (_∘_)
+
+show : ∀ {a} {A : Set a} {n} → (A → String) → (Vec≤ A n → String)
+show s = Vec.show s ∘ Vec≤.vec

src/Data/Vec/Show.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing vectors
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Vec.Show where
+
+import Data.List.Show as List
+open import Data.String.Base using (String)
+open import Data.Vec.Base using (Vec; toList)
+open import Function.Base using (_∘_)
+
+show : ∀ {a} {A : Set a} {n} → (A → String) → (Vec A n → String)
+show s = List.show s ∘ toList

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,199 @@
+------------------------------------------------------------------------
+-- 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 (ℕ; z≤n) 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)
+
+  -- Careful: this can generate very long lists!
+  -- You may want to use Vec≤ instead.
+  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
+
+module Vec≤ {a} {A : Set a} (rIO : IO A) (n : ℕ) where
+
+  open import Data.Vec.Bounded.Base using (Vec≤; _,_)
+
+  randomIO : IO (Vec≤ A n)
+  randomIO = do
+    lift (len ∈[ _ , len≤n ]) ← lift! (ℕ.randomRIO 0 n z≤n)
+    vec ← Vec.randomIO rIO len
+    pure (vec , len≤n)
+
+module String where
+
+  open import Data.String.Base using (String; fromList)
+
+  -- Careful: this can generate very long lists!
+  -- You may want to use String≤ instead.
+  randomIO : IO String
+  randomIO = fromList <$> List.randomIO Char.randomIO
+
+module String≤ (n : ℕ) where
+
+  import Data.Vec.Bounded.Base as Vec≤
+  open import Data.String.Base using (String; fromList)
+
+  randomIO : IO String
+  randomIO = fromList ∘ Vec≤.toList <$> Vec≤.randomIO Char.randomIO n
+
+open import Data.Char.Base using (Char; _≤_)
+
+module RangedString≤ (a b : Char)  .(a≤b : a ≤ b) (n : ℕ) where
+
+  import Data.Vec.Bounded.Base as Vec≤
+  open import Data.String.Base using (String; fromList)
+
+  randomIO : IO String
+  randomIO =
+    fromList ∘ Vec≤.toList ∘ Vec≤.map InBounds.value
+    <$> Vec≤.randomIO (Char.randomRIO a b a≤b) n

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 = abs <$> randomIO #-}
+{-# COMPILE GHC randomRIO-Nat = randomRIO #-}
+{-# COMPILE GHC randomIO-Word64 = randomIO #-}
+{-# COMPILE GHC randomRIO-Word64 = randomRIO #-}