bfe.agda

{-# 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