Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/bfe.agda
Created Sep 1, 2019

Embed
What would you like to do?
{-# OPTIONS --safe --sized-types #-}
module Bits where
open import Agda.Primitive using (Level)
open import Agda.Builtin.Size
variable
a : Level
b : Level
A : Set a
B : Set b
infixr 5 ∹_
mutual
data _⋆ (A : Set a) : Set a where
[] : A ⋆
∹_ : A ⁺ A ⋆
record _⁺ (A : Set a) : Set a where
constructor _&_
inductive
field
head : A
tail : A ⋆
open _⁺
record Thunk (T : Size → Set a) (i : Size) : Set a where
coinductive
field force : {j : Size< i} T j
open Thunk
mutual
data Colist⋆ (A : Set a) (i : Size) : Set a where
[] : Colist⋆ A i
∹_ : Colist⁺ A i Colist⋆ A i
record Colist⁺ (A : Set a) (i : Size) : Set a where
coinductive
field
head : A
tail : Thunk (Colist⋆ A) i
open Colist⁺
infixr 4 _&_
record Tree (A : Set a) (i : Size) : Set a where
constructor _&_
inductive
field
root : A
forest : Thunk (Tree A) i ⋆
foldr : (A B B) B A ⋆ B
foldr f b [] = b
foldr f b (∹ xs) = f (head xs) (foldr f b (tail xs))
lwe : {i} Tree A i Colist⋆ (A ⁺) i
lwe r = f r []
where
f : {i} Tree A i Colist⋆ (A ⁺) i Colist⋆ (A ⁺) i
g : {i} Tree A i Colist⋆ (A ⁺) i Colist⁺ (A ⁺) i
f x qs = ∹ g x qs
head (head (g (x & xs) qs)) = x
tail (head (g (x & xs) [])) = []
tail (head (g (x & xs) (∹ qs))) = ∹ head qs
force (tail (g (x & xs) [])) = foldr (λ y f (y . force)) [] xs
force (tail (g (x & xs) (∹ qs))) = foldr (λ y f (y .force)) (tail qs .force) xs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.