module CyclicTags where

open import Data.Colist as Col
open import Data.Vec as V
open import Data.Fin as F
open import Data.Nat
open import Data.Maybe
open import Coinduction
open import Data.Unit
open import IO

-- Simple type for cyclic tags isomorphic to booleans
data Tag : Set where
  `0 `1 `∣ : Tag -- Tags 0 and 1 including a separator

weak-incr : ∀ {n} -> Fin (suc n) -> Maybe (Fin (suc n))
weak-incr {zero} f = nothing
weak-incr {suc n} zero = just (suc zero)
weak-incr {suc n} (suc f) with weak-incr f
weak-incr {suc n} (suc f) | just x = just (suc x)
weak-incr {suc n} (suc f) | nothing = nothing

mod-incr : ∀ {n} -> (Fin (suc n)) -> (Fin (suc n))
mod-incr f with weak-incr f
mod-incr f | just x = x
mod-incr f | nothing = zero

cycle' : ∀ {n} -> Fin (suc n) -> Vec (Colist Tag) (suc n) -> Colist Tag -> Colist Tag
cycle' i p []        =  []
cycle' i p (`0 ∷ xs) = `0 ∷ ♯ cycle' (mod-incr i) p (♭ xs)
cycle' i p (`1 ∷ xs) = `1 ∷ ♯ cycle' (mod-incr i) p (♭ xs Col.++ V.lookup i p Col.++ `∣ ∷ ♯ [])
cycle' i p (`∣  ∷ xs) = `∣ ∷ ♯ cycle' i p (♭ xs)

cycle : ∀ {n} (productions : Vec (Colist Tag) (suc n)) -> (queue : Colist Tag) -> Colist Tag
cycle = cycle' zero

putTags : Colist Tag -> IO ⊤
putTags [] = return tt
putTags (`0 ∷ xs) = ♯ putStrLn "0" >> ♯ putTags (♭ xs)
putTags (`1 ∷ xs) = ♯ putStrLn "1" >> ♯ putTags (♭ xs)
putTags (`∣ ∷ xs) = ♯ putStrLn "\n" >> ♯ putTags (♭ xs)

main = run (putTags (cycle productions (`1 ∷ ♯ (`∣ ∷ ♯ []))))
  where productions =   (`0 ∷ ♯ (`1 ∷ ♯ (`1 ∷ ♯ [])))
                      ∷ (`1 ∷ ♯ (`0 ∷ ♯ []))
                      ∷ (`1 ∷ ♯ (`0 ∷ ♯ (`1 ∷ ♯ [])))
                      ∷ []