Skip to content

Instantly share code, notes, and snippets.

@gallais
Created Oct 17, 2018
Embed
What would you like to do?
module bins where
open import Size
open import Codata.Stream
open import Codata.Thunk
open import Data.List.Base as List using (List; _∷_; [])
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; [_])
open import Function
open import Relation.Unary
_<<>_ : {a b i} {A : Set a} {B : Set b}
List⁺ (A B) Stream A i Stream B i
fs <<> xs = concat (map (λ a List⁺.map (_$ a) fs) xs)
data Bin : Set where O I : Bin
allLetters : List⁺ Bin
allLetters = O ∷ I ∷ []
cofix : (A : Size Set) ∀[ Thunk A ⇒ A ] ∀[ A ]
cofix A f = f (λ where .force cofix A f)
bins : Stream (List⁺ Bin) _
bins = [ O ] ∷ λ where
.force cofix (Stream (List⁺ Bin)) $ λ bins [ I ] ∷ λ where
.force List⁺.map List⁺._∷⁺_ allLetters <<> bins .force
open import Agda.Builtin.Equality
import Data.Vec as Vec
open import Data.Nat
open import Data.Char
open import Data.String as String
showBin : Bin Char
showBin O = 'O'
showBin I = 'I'
lookAt : List String
lookAt k = List.map (String.fromList⁺ ∘′ List⁺.map showBin)
$ Vec.toList $′ take k bins
_ : lookAt 20"O""I"
"OI""II""OOI""IOI""OII""III"
"OOOI""IOOI""OIOI""IIOI""OOII""IOII""OIII""IIII"
"OOOOI""IOOOI""OIOOI""IIOOI" ∷ []
_ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment