------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion between coinductive data structures using "musical"
-- coinduction and the ones using sized types.
--
-- Warning: the combination of --sized-types and --guardedness is
-- known to be unsound, so use these conversions at your own risk.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types --guardedness #-}
module Codata.Musical.Conversion where
open import Level using (Level)
import Codata.Sized.Cofin as Sized
import Codata.Sized.Colist as Sized
import Codata.Sized.Conat as Sized
import Codata.Sized.Covec as Sized
import Codata.Sized.M as Sized
import Codata.Sized.Stream as Sized
open import Codata.Sized.Thunk
open import Codata.Musical.Cofin hiding (module Cofin)
open import Codata.Musical.Colist hiding (module Colist)
open import Codata.Musical.Conat
open import Codata.Musical.Covec hiding (module Covec)
open import Codata.Musical.M hiding (module M)
open import Codata.Musical.Notation
open import Codata.Musical.Stream hiding (module Stream)
open import Data.Product.Base using (_,_)
open import Data.Container.Core as C using (Container)
import Size
private
variable
a : Level
A : Set a
module Colist where
fromMusical : ∀ {i} → Colist A → Sized.Colist A i
fromMusical [] = Sized.[]
fromMusical (x ∷ xs) = x Sized.∷ λ where .force → fromMusical (♭ xs)
toMusical : Sized.Colist A Size.∞ → Colist A
toMusical Sized.[] = []
toMusical (x Sized.∷ xs) = x ∷ ♯ toMusical (xs .force)
module Conat where
fromMusical : ∀ {i} → Coℕ → Sized.Conat i
fromMusical zero = Sized.zero
fromMusical (suc n) = Sized.suc λ where .force → fromMusical (♭ n)
toMusical : Sized.Conat Size.∞ → Coℕ
toMusical Sized.zero = zero
toMusical (Sized.suc n) = suc (♯ toMusical (n .force))
module Cofin where
fromMusical : ∀ {n} → Cofin n → Sized.Cofin (Conat.fromMusical n)
fromMusical zero = Sized.zero
fromMusical (suc n) = Sized.suc (fromMusical n)
toMusical : ∀ {n} → Sized.Cofin n → Cofin (Conat.toMusical n)
toMusical Sized.zero = zero
toMusical (Sized.suc n) = suc (toMusical n)
module Covec where
fromMusical : ∀ {i n} → Covec A n → Sized.Covec A i (Conat.fromMusical n)
fromMusical [] = Sized.[]
fromMusical (x ∷ xs) = x Sized.∷ λ where .force → fromMusical (♭ xs)
toMusical : ∀ {n} → Sized.Covec A Size.∞ n → Covec A (Conat.toMusical n)
toMusical Sized.[] = []
toMusical (x Sized.∷ xs) = x ∷ ♯ toMusical (xs .force)
module M {s p} {C : Container s p} where
fromMusical : ∀ {i} → M C → Sized.M C i
fromMusical (inf t) = Sized.M.inf (C.map rec t) where
rec = λ x → λ where .force → fromMusical (♭ x)
toMusical : Sized.M C Size.∞ → M C
toMusical (Sized.M.inf (s , f)) = inf (s , λ p → ♯ toMusical (f p .force))
module Stream where
fromMusical : ∀ {i} → Stream A → Sized.Stream A i
fromMusical (x ∷ xs) = x Sized.∷ λ where .force → fromMusical (♭ xs)
toMusical : Sized.Stream A Size.∞ → Stream A
toMusical (x Sized.∷ xs) = x ∷ ♯ toMusical (xs .force)
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