------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive lists
------------------------------------------------------------------------

module Codata.Musical.Colist where

open import Category.Monad
open import Codata.Musical.Notation
open import Codata.Musical.Conat using (Coℕ; zero; suc)
open import Data.Bool.Base using (Bool; true; false)
open import Data.BoundedVec.Inefficient as BVec
  using (BoundedVec; []; _∷_)
open import Data.Empty using ()
open import Data.Maybe.Base using (Maybe; nothing; just; Is-just)
open import Data.Nat.Base using (; zero; suc; _≥′_; ≤′-refl; ≤′-step)
open import Data.Nat.Properties using (s≤′s)
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Product as Prod using (; _×_; _,_)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
open import Level using (_⊔_)
open import Relation.Binary
import Relation.Binary.Construct.FromRel as Ind
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Negation

module ¬¬Monad {p} where
  open RawMonad (¬¬-Monad {p}) public
open ¬¬Monad  -- we don't want the RawMonad content to be opened publicly

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : (x : A) (xs :  (Colist A))  Colist A

{-# FOREIGN GHC
  data AgdaColist a    = Nil | Cons a (MAlonzo.RTE.Inf (AgdaColist a))
  type AgdaColist' l a = AgdaColist a
  #-}
{-# COMPILE GHC Colist = data AgdaColist' (Nil | Cons) #-}
{-# COMPILE UHC Colist = data __LIST__ (__NIL__ | __CONS__) #-}

module Colist-injective {a} {A : Set a} where

 ∷-injectiveˡ :  {x y : A} {xs ys}  (Colist A  x  xs)  y  ys  x  y
 ∷-injectiveˡ P.refl = P.refl

 ∷-injectiveʳ :  {x y : A} {xs ys}  (Colist A  x  xs)  y  ys  xs  ys
 ∷-injectiveʳ P.refl = P.refl

data Any {a p} {A : Set a} (P : A  Set p) :
         Colist A  Set (a  p) where
  here  :  {x xs} (px  : P x)           Any P (x  xs)
  there :  {x xs} (pxs : Any P ( xs))  Any P (x  xs)

module _  {a p} {A : Set a} {P : A  Set p} where

 here-injective :  {x xs p q}  (Any P (x  xs)  here p)  here q  p  q
 here-injective P.refl = P.refl

 there-injective :  {x xs p q}  (Any P (x  xs)  there p)  there q  p  q
 there-injective P.refl = P.refl

data All {a p} {A : Set a} (P : A  Set p) :
         Colist A  Set (a  p) where
  []  : All P []
  _∷_ :  {x xs} (px : P x) (pxs :  (All P ( xs)))  All P (x  xs)

module All-injective {a p} {A : Set a} {P : A  Set p} where

 ∷-injectiveˡ :  {x xs} {px qx pxs qxs} 
                (All P (x  xs)  px  pxs)  qx  qxs  px  qx
 ∷-injectiveˡ P.refl = P.refl

 ∷-injectiveʳ :  {x xs} {px qx pxs qxs} 
                (All P (x  xs)  px  pxs)  qx  qxs  pxs  qxs
 ∷-injectiveʳ P.refl = P.refl

------------------------------------------------------------------------
-- Some operations

null :  {a} {A : Set a}  Colist A  Bool
null []      = true
null (_  _) = false

length :  {a} {A : Set a}  Colist A  Coℕ
length []       = zero
length (x  xs) = suc ( length ( xs))

map :  {a b} {A : Set a} {B : Set b}  (A  B)  Colist A  Colist B
map f []       = []
map f (x  xs) = f x   map f ( xs)

fromList :  {a} {A : Set a}  List A  Colist A
fromList []       = []
fromList (x  xs) = x   fromList xs

take :  {a} {A : Set a} (n : )  Colist A  BoundedVec A n
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x  xs) = x  take n ( xs)

replicate :  {a} {A : Set a}  Coℕ  A  Colist A
replicate zero    x = []
replicate (suc n) x = x   replicate ( n) x

lookup :  {a} {A : Set a}    Colist A  Maybe A
lookup n       []       = nothing
lookup zero    (x  xs) = just x
lookup (suc n) (x  xs) = lookup n ( xs)

infixr 5 _++_

_++_ :  {a} {A : Set a}  Colist A  Colist A  Colist A
[]       ++ ys = ys
(x  xs) ++ ys = x   ( xs ++ ys)

-- Interleaves the two colists (until the shorter one, if any, has
-- been exhausted).

infixr 5 _⋎_

_⋎_ :  {a} {A : Set a}  Colist A  Colist A  Colist A
[]        ys = ys
(x  xs)  ys = x   (ys   xs)

concat :  {a} {A : Set a}  Colist (List⁺ A)  Colist A
concat []                     = []
concat ((x  [])        xss) = x   concat ( xss)
concat ((x  (y  xs))  xss) = x   concat ((y  xs)  xss)

[_] :  {a} {A : Set a}  A  Colist A
[ x ] = x   []

------------------------------------------------------------------------
-- Any lemmas

-- Any lemma for map.

Any-map :  {a b p} {A : Set a} {B : Set b} {P : B  Set p}
          {f : A  B} {xs} 
          Any P (map f xs)  Any (P  f) xs
Any-map {P = P} {f} {xs} = inverse to from from∘to to∘from
  where
  to :  {xs}  Any P (map f xs)  Any (P  f) xs
  to {[]}     ()
  to {x  xs} (here px) = here px
  to {x  xs} (there p) = there (to p)

  from :  {xs}  Any (P  f) xs  Any P (map f xs)
  from (here px) = here px
  from (there p) = there (from p)

  from∘to :  {xs} (p : Any P (map f xs))  from (to p)  p
  from∘to {[]}     ()
  from∘to {x  xs} (here px) = P.refl
  from∘to {x  xs} (there p) = P.cong there (from∘to p)

  to∘from :  {xs} (p : Any (P  f) xs)  to (from p)  p
  to∘from (here px) = P.refl
  to∘from (there p) = P.cong there (to∘from p)

-- Any lemma for _⋎_. This lemma implies that every member of xs or ys
-- is a member of xs ⋎ ys, and vice versa.

Any-⋎ :  {a p} {A : Set a} {P : A  Set p} xs {ys} 
        Any P (xs  ys)  (Any P xs  Any P ys)
Any-⋎ {P = P} = λ xs  record
  { to         = P.→-to-⟶ (to xs)
  ; from       = P.→-to-⟶ (from xs)
  ; inverse-of = record
    { left-inverse-of  = from∘to xs
    ; right-inverse-of = to∘from xs
    }
  }
  where
  to :  xs {ys}  Any P (xs  ys)  Any P xs  Any P ys
  to []       p         = inj₂ p
  to (x  xs) (here px) = inj₁ (here px)
  to (x  xs) (there p) = [ inj₂ , inj₁  there ]′ (to _ p)

  mutual

    from-left :  {xs ys}  Any P xs  Any P (xs  ys)
    from-left           (here px) = here px
    from-left {ys = ys} (there p) = there (from-right ys p)

    from-right :  xs {ys}  Any P ys  Any P (xs  ys)
    from-right []       p = p
    from-right (x  xs) p = there (from-left p)

  from :  xs {ys}  Any P xs  Any P ys  Any P (xs  ys)
  from xs = Sum.[ from-left , from-right xs ]

  from∘to :  xs {ys} (p : Any P (xs  ys))  from xs (to xs p)  p
  from∘to []                 p                          = P.refl
  from∘to (x  xs)           (here px)                  = P.refl
  from∘to (x  xs) {ys = ys} (there p)                  with to ys p | from∘to ys p
  from∘to (x  xs) {ys = ys} (there .(from-left q))     | inj₁ q | P.refl = P.refl
  from∘to (x  xs) {ys = ys} (there .(from-right ys q)) | inj₂ q | P.refl = P.refl

  mutual

    to∘from-left :  {xs ys} (p : Any P xs) 
                   to xs {ys = ys} (from-left p)  inj₁ p
    to∘from-left           (here px) = P.refl
    to∘from-left {ys = ys} (there p)
      rewrite to∘from-right ys p = P.refl

    to∘from-right :  xs {ys} (p : Any P ys) 
                    to xs (from-right xs p)  inj₂ p
    to∘from-right []                 p = P.refl
    to∘from-right (x  xs) {ys = ys} p
      rewrite to∘from-left {xs = ys} {ys =  xs} p = P.refl

  to∘from :  xs {ys} (p : Any P xs  Any P ys)  to xs (from xs p)  p
  to∘from xs = Sum.[ to∘from-left , to∘from-right xs ]

------------------------------------------------------------------------
-- Equality

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {a} {A : Set a} : (xs ys : Colist A)  Set a where
  []  :                                       []      []
  _∷_ :  x {xs ys} (xs≈ :  ( xs   ys))  x  xs  x  ys

-- The equality relation forms a setoid.

setoid :  {}  Set   Setoid _ _
setoid A = record
  { Carrier       = Colist A
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {[]}     = []
  refl {x  xs} = x   refl

  sym : Symmetric _≈_
  sym []        = []
  sym (x  xs≈) = x   sym ( xs≈)

  trans : Transitive _≈_
  trans []        []         = []
  trans (x  xs≈) (.x  ys≈) = x   trans ( xs≈) ( ys≈)

module ≈-Reasoning where
  import Relation.Binary.EqReasoning as EqR
  private
    open module R {a} {A : Set a} = EqR (setoid A) public

-- map preserves equality.

map-cong :  {a b} {A : Set a} {B : Set b}
           (f : A  B)  _≈_ =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x  xs≈) = f x   map-cong f ( xs≈)

-- Any respects pointwise implication (for the predicate) and equality
-- (for the colist).

Any-resp :  {a p q} {A : Set a} {P : A  Set p} {Q : A  Set q}
           {xs ys}  (∀ {x}  P x  Q x)  xs  ys 
           Any P xs  Any Q ys
Any-resp f (x  xs≈) (here px) = here (f px)
Any-resp f (x  xs≈) (there p) = there (Any-resp f ( xs≈) p)

-- Any maps pointwise isomorphic predicates and equal colists to
-- isomorphic types.

Any-cong :  {a p q} {A : Set a} {P : A  Set p} {Q : A  Set q}
           {xs ys}  P ↔̇ Q  xs  ys  Any P xs  Any Q ys
Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q xs≈ys = record
  { to         = P.→-to-⟶ (to xs≈ys)
  ; from       = P.→-to-⟶ (from xs≈ys)
  ; inverse-of = record
    { left-inverse-of  = resp∘resp          P↔Q       xs≈ys (sym xs≈ys)
    ; right-inverse-of = resp∘resp (Inv.sym P↔Q) (sym xs≈ys)     xs≈ys
    }
  }
  where
  open Setoid (setoid _) using (sym)

  to :  {xs ys}  xs  ys  Any P xs  Any Q ys
  to xs≈ys = Any-resp (Inverse.to P↔Q ⟨$⟩_) xs≈ys

  from :  {xs ys}  xs  ys  Any Q ys  Any P xs
  from xs≈ys = Any-resp (Inverse.from P↔Q ⟨$⟩_) (sym xs≈ys)

  resp∘resp :  {p q} {P : A  Set p} {Q : A  Set q} {xs ys}
              (P↔̇Q : P ↔̇ Q) (xs≈ys : xs  ys) (ys≈xs : ys  xs)
              (p : Any P xs) 
              Any-resp (Inverse.from P↔̇Q ⟨$⟩_) ys≈xs
                (Any-resp (Inverse.to P↔̇Q ⟨$⟩_) xs≈ys p)  p
  resp∘resp P↔̇Q (x  xs≈) (.x  ys≈) (here px) =
    P.cong here (Inverse.left-inverse-of P↔̇Q px)
  resp∘resp P↔̇Q (x  xs≈) (.x  ys≈) (there p) =
    P.cong there (resp∘resp P↔̇Q ( xs≈) ( ys≈) p)

------------------------------------------------------------------------
-- Indices

-- Converts Any proofs to indices into the colist. The index can also
-- be seen as the size of the proof.

index :  {a p} {A : Set a} {P : A  Set p} {xs}  Any P xs  
index (here px) = zero
index (there p) = suc (index p)

-- The position returned by index is guaranteed to be within bounds.

lookup-index :  {a p} {A : Set a} {P : A  Set p} {xs} (p : Any P xs) 
               Is-just (lookup (index p) xs)
lookup-index (here px) = just _
lookup-index (there p) = lookup-index p

-- Any-resp preserves the index.

index-Any-resp :
   {a p q} {A : Set a} {P : A  Set p} {Q : A  Set q}
    {f :  {x}  P x  Q x} {xs ys}
  (xs≈ys : xs  ys) (p : Any P xs) 
  index (Any-resp f xs≈ys p)  index p
index-Any-resp (x  xs≈) (here px) = P.refl
index-Any-resp (x  xs≈) (there p) =
  P.cong suc (index-Any-resp ( xs≈) p)

-- The left-to-right direction of Any-⋎ returns a proof whose size is
-- no larger than that of the input proof.

index-Any-⋎ :
   {a p} {A : Set a} {P : A  Set p} xs {ys} (p : Any P (xs  ys)) 
  index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) ⟨$⟩ p)
index-Any-⋎ []                 p         = ≤′-refl
index-Any-⋎ (x  xs)           (here px) = ≤′-refl
index-Any-⋎ (x  xs) {ys = ys} (there p)
  with Inverse.to (Any-⋎ ys) ⟨$⟩ p | index-Any-⋎ ys p
... | inj₁ q | q≤p = ≤′-step q≤p
... | inj₂ q | q≤p = s≤′s    q≤p

------------------------------------------------------------------------
-- Memberships, subsets, prefixes

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

_∈_ :  {a}  {A : Set a}  A  Colist A  Set a
x  xs = Any (_≡_ x) xs

-- xs ⊆ ys means that xs is a subset of ys.

infix 4 _⊆_

_⊆_ :  {a}  {A : Set a}  Colist A  Colist A  Set a
xs  ys =  {x}  x  xs  x  ys

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {a} {A : Set a} : Colist A  Colist A  Set a where
  []  :  {ys}                             []      ys
  _∷_ :  x {xs ys} (p :  ( xs   ys))  x  xs  x  ys

-- Any can be expressed using _∈_ (and vice versa).

Any-∈ :  {a p} {A : Set a} {P : A  Set p} {xs} 
        Any P xs   λ x  x  xs × P x
Any-∈ {P = P} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶  { (x , x∈xs , p)  from x∈xs p })
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = λ { (x , x∈xs , p)  to∘from x∈xs p }
    }
  }
  where
  to :  {xs}  Any P xs   λ x  x  xs × P x
  to (here  p) = _ , here P.refl , p
  to (there p) = Prod.map id (Prod.map there id) (to p)

  from :  {x xs}  x  xs  P x  Any P xs
  from (here P.refl) p = here p
  from (there x∈xs)  p = there (from x∈xs p)

  to∘from :  {x xs} (x∈xs : x  xs) (p : P x) 
            to (from x∈xs p)  (x , x∈xs , p)
  to∘from (here P.refl) p = P.refl
  to∘from (there x∈xs)  p =
    P.cong (Prod.map id (Prod.map there id)) (to∘from x∈xs p)

  from∘to :  {xs} (p : Any P xs) 
            let (x , x∈xs , px) = to p in from x∈xs px  p
  from∘to (here _)  = P.refl
  from∘to (there p) = P.cong there (from∘to p)

-- Prefixes are subsets.

⊑⇒⊆ :  {a}  {A : Set a}  _⊑_ {A = A}  _⊆_
⊑⇒⊆ []          ()
⊑⇒⊆ (x  xs⊑ys) (here ≡x)    = here ≡x
⊑⇒⊆ (_  xs⊑ys) (there x∈xs) = there (⊑⇒⊆ ( xs⊑ys) x∈xs)

-- The prefix relation forms a poset.

⊑-Poset :  {}  Set   Poset _ _ _
⊑-Poset A = record
  { Carrier        = Colist A
  ; _≈_            = _≈_
  ; _≤_            = _⊑_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Setoid.isEquivalence (setoid A)
      ; reflexive     = reflexive
      ; trans         = trans
      }
    ; antisym  = antisym
    }
  }
  where
  reflexive : _≈_  _⊑_
  reflexive []        = []
  reflexive (x  xs≈) = x   reflexive ( xs≈)

  trans : Transitive _⊑_
  trans []        _          = []
  trans (x  xs≈) (.x  ys≈) = x   trans ( xs≈) ( ys≈)

  antisym : Antisymmetric _≈_ _⊑_
  antisym []       []        = []
  antisym (x  p₁) (.x  p₂) = x   antisym ( p₁) ( p₂)

module ⊑-Reasoning where
  import Relation.Binary.PartialOrderReasoning as POR
  private
    open module R {a} {A : Set a} = POR (⊑-Poset A)
      public renaming (_≤⟨_⟩_ to _⊑⟨_⟩_)

-- The subset relation forms a preorder.

⊆-Preorder :  {}  Set   Preorder _ _ _
⊆-Preorder A = Ind.preorder (setoid A) _∈_
                  xs≈ys  ⊑⇒⊆ (⊑P.reflexive xs≈ys))
  where module ⊑P = Poset (⊑-Poset A)

module ⊆-Reasoning where
  import Relation.Binary.PreorderReasoning as PreR
  private
    open module R {a} {A : Set a} = PreR (⊆-Preorder A)
      public renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

  infix 1 _∈⟨_⟩_

  _∈⟨_⟩_ :  {a} {A : Set a} (x : A) {xs ys} 
           x  xs  xs IsRelatedTo ys  x  ys
  x ∈⟨ x∈xs  xs⊆ys = (begin xs⊆ys) x∈xs

-- take returns a prefix.

take-⊑ :  {a} {A : Set a} n (xs : Colist A) 
         let toColist = fromList {a}  BVec.toList in
         toColist (take n xs)  xs
take-⊑ zero    xs       = []
take-⊑ (suc n) []       = []
take-⊑ (suc n) (x  xs) = x   take-⊑ n ( xs)

------------------------------------------------------------------------
-- Finiteness and infiniteness

-- Finite xs means that xs has finite length.

data Finite {a} {A : Set a} : Colist A  Set a where
  []  : Finite []
  _∷_ :  x {xs} (fin : Finite ( xs))  Finite (x  xs)

module Finite-injective {a} {A : Set a} where

 ∷-injective :  {x : A} {xs p q}  (Finite (x  xs)  x  p)  x  q  p  q
 ∷-injective P.refl = P.refl

-- Infinite xs means that xs has infinite length.

data Infinite {a} {A : Set a} : Colist A  Set a where
  _∷_ :  x {xs} (inf :  (Infinite ( xs)))  Infinite (x  xs)

module Infinite-injective {a} {A : Set a} where

 ∷-injective :  {x : A} {xs p q}  (Infinite (x  xs)  x  p)  x  q  p  q
 ∷-injective P.refl = P.refl

-- Colists which are not finite are infinite.

not-finite-is-infinite :
   {a} {A : Set a} (xs : Colist A)  ¬ Finite xs  Infinite xs
not-finite-is-infinite []       hyp with hyp []
... | ()
not-finite-is-infinite (x  xs) hyp =
  x   not-finite-is-infinite ( xs) (hyp  _∷_ x)

-- Colists are either finite or infinite (classically).

finite-or-infinite :
   {a} {A : Set a} (xs : Colist A)  ¬ ¬ (Finite xs  Infinite xs)
finite-or-infinite xs = helper <$> excluded-middle
  where
  helper : Dec (Finite xs)  Finite xs  Infinite xs
  helper (yes fin) = inj₁ fin
  helper (no ¬fin) = inj₂ $ not-finite-is-infinite xs ¬fin

-- Colists are not both finite and infinite.

not-finite-and-infinite :
   {a} {A : Set a} {xs : Colist A}  Finite xs  Infinite xs  
not-finite-and-infinite []        ()
not-finite-and-infinite (x  fin) (.x  inf) =
  not-finite-and-infinite fin ( inf)