------------------------------------------------------------------------
-- 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.Word64.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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4