module Lib.Star where

open import Agda.Builtin.Equality

open import Lib.Zero
open import Lib.One
open import Lib.Two

open import Lib.Nat

data Dir : Set where
  cons : Dir
  snoc : Dir

other : Dir → Dir
other cons = snoc
other snoc = cons

data FCat (d : Dir) { X : Set } (R : X → X → Set) (x : X) : X → Set where
  nil' : { y : X } → x ≡ y → FCat d R x y
  cons : d ≡ cons → { y z : X } → R x y → FCat d R y z → FCat d R x z
  snoc : d ≡ snoc → { y z : X } → FCat d R x y → R y z → FCat d R x z

fCat : ∀{d X R R'} → ({s t : X} → R s t → R' s t)
      → {s t : X} → FCat d R s t → FCat d R' s t
fCat f (nil' x) = nil' x
fCat f (cons d x xs) = cons d (f x) (fCat f xs)
fCat f (snoc d xz x) = snoc d (fCat f xz) (f x)

Star = FCat cons
Rats = FCat snoc

pattern [] = nil' refl
pattern _,-_ x xs = cons refl x xs
pattern _-,_ xz x = snoc refl xz x

infixr  _,-_
infixl  _-,_

List : Set → Set
List A = Star { One } (\ _ _ → A) ⟨⟩ ⟨⟩

BList : Set → Set
BList A = Rats { One } (\ _ _ → A) ⟨⟩ ⟨⟩

concat : {d : Dir}{X : Set}{R : X → X → Set}{x y z : X}
       → FCat d R x y → FCat d R y z
       → FCat d R x z
concat [] bs = bs
concat (a ,- as) bs = a ,- concat as bs
concat az@(_ -, _) [] = az
concat az@(_ -, _) (bz -, b) = concat az bz -, b

catStar = concat {cons}
catRats = concat {snoc}

ratsToStar : {X : Set}{R : X → X → Set}{x y : X} → Rats R x y → Star R x y
ratsToStar [] = []
ratsToStar (rats -, r) = catStar (ratsToStar rats) (r ,- [])

starToRats : {X : Set}{R : X → X → Set}{x y : X} → Star R x y → Rats R x y
starToRats [] = []
starToRats (s ,- star) = catRats ([] -, s) (starToRats star)

{-
_<*><_ : {X : Set}{R : X → X → Set}{x y z : X} → Rats R x y → Star R y z → Rats R x z
_<*><_ rz nil = rz
_<*><_ rz (s ,- st) = (rz -, s) <*>< st

_<*>>_ : {X : Set}{R : X → X → Set}{x y z : X} → Rats R x y → Star R y z → Star R x z
_<*>>_ lin ss = ss
_<*>>_ (rz -, x) ss = rz <*>> (x ,- ss)
-}