-
Notifications
You must be signed in to change notification settings - Fork 258
[ new ] System.Random bindings #2368
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
5 commits
Select commit
Hold shift + click to select a range
06aa4cb
[ new ] System.Random bindings
gallais 667f77f
[ more ] Show functions, test
gallais 00c0dbe
[ fix ] Nat bug, more random generators, test case
gallais b2a6d60
[ fix ] missing file + local gitignore
gallais 7947cd4
[ fix ] forgot to update the CHANGELOG
gallais File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 #-} |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.