{-# OPTIONS --guardedness #-}

-- Take this example as motivation:
-- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring

open import Level
open import Agda.Builtin.Coinduction
module thesis.motivation where

module old-delay where
  private
    variable
      a : Level
  data _⊥ (A : Set a) : Set a where
    now : A → A ⊥
    later : ∞ (A ⊥) → A ⊥

  never : ∀ {A : Set a} → A ⊥
  never = later (♯ never)

module ReverseInput where
  open import Data.Char
  open import Data.Nat
  open import Data.List using (List; []; _∷_)
  open import Data.String
  open import Data.Unit.Polymorphic
  open import Codata.Musical.Costring
  open import Codata.Musical.Colist using ([]; _∷_)
  -- open import IO using (IO; seq; bind; return; Main; run; putStrLn)
  open import IO.Primitive
  open import IO.Primitive.Infinite using (getContents)
  open import Agda.Builtin.IO using ()

  open old-delay
  -- IDEA: start in haskell, then motivate in agda and define delay type
  -- next talk about bisimilarity.
  -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda

  private
    variable
      a : Level

  -- reverse : Costring → String ⊥
  -- reverse = go []
  --   where
  --   go : List Char → Costring → String ⊥
  --   go acc []       = now (fromList acc)
  --   go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))

  -- putStrLn⊥ : String ⊥ → IO {a} ⊤
  -- putStrLn⊥ (now   s) = putStrLn s
  -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s))

  -- main : Main
  -- main = run (bind (♯ {!  getContents !}) {!   !}) --(λ c → ♯ putStrLn⊥ (reverse c)))

-- NOTE: This is not very understandable... Better stick to the outdated syntax
module delay where
  mutual
    data _⊥ (A : Set) : Set where
      now : A → A ⊥
      later : A ⊥' → A ⊥
    
    record _⊥' (A : Set) : Set where
      coinductive
      field
        force : A ⊥
  open _⊥'

  mutual
    never : ∀ {A : Set} → A ⊥
    never = later never'

    never' : ∀ {A : Set} → A ⊥'
    force never' = never