------------------------------------------------------------------------
-- 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)