module Lib.List where

open import Agda.Builtin.Equality
open import Lib.PropEq

open import Lib.Sigma
open import Lib.Star

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

data List′ (X : Set) : Set where
  nil : List′ X
  cons : X → List′ X → List′ X

_++_ : {X : Set} → List X → List X → List X
[] ++ ls' = ls'
(l ,- ls) ++ ls' = l ,- (ls ++ ls')
infixr  _++_

{-
data BList (X : Set) : Set where
  [] : BList X
  _-,_ : BList X → X → BList X
infixl 6 _-,_
-}

_⟨⟩⟨_ : {X : Set} → BList X → List X → BList X
lz ⟨⟩⟨ [] = lz
lz ⟨⟩⟨ (r ,- rs) = lz -, r ⟨⟩⟨ rs

infixl  _⟨⟩⟨_

_⟨⟩⟩_ : {X : Set} → BList X → List X → List X
[] ⟨⟩⟩ ls = ls
(bz -, b) ⟨⟩⟩ ls = bz ⟨⟩⟩ b ,- ls

infixr  _⟨⟩⟩_

rotate : { X : Set } → BList X → List X
rotate [] = []
rotate (lz -, l) = l ,- rotate lz

++assoc : {X : Set} {xs ys zs : List X} →  (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++assoc {xs = []} {ys} {zs} = refl
++assoc {xs = x ,- xs} {ys} {zs} = cong (x ,-_) (++assoc {xs = xs}{ys}{zs})

++[] : {X : Set}(xs : List X) → xs ++ [] ≡ xs
++[] [] = refl
++[] (x ,- xs) = cong (x ,-_) (++[] xs)
--{-# REWRITE ++assoc ++[] #-}

_+-_ : {X : Set} → List X → List X → List X
ls +- [] = ls
ls +- (x ,- ls') = (ls +- ls') ++ (x ,- [])

reverse : { X : Set } → List X → List X
reverse [] = []
reverse (x ,- xs) = reverse xs ++ (x ,- [])

[]+- : {X : Set}(xs ys : List X) → xs ++ ([] +- ys) ≡ xs +- ys
[]+- xs [] = ++[] xs
[]+- xs (y ,- ys) = trans (sym (++assoc {xs = xs} {[] +- ys} {y ,- []})) (cong (_++ y ,- []) ([]+- xs ys))

+-dist : {X : Set}(xs ys zs : List X) → (xs +- ys) +- zs ≡ xs +- (zs ++ ys)
+-dist xs ys [] = refl
+-dist xs ys (x ,- zs) = cong (_++ (x ,- [])) (+-dist xs ys zs)
--{-# REWRITE +-dist #-}

++singleton : {X : Set} {as bs : List X}{b : X} → (as ++ b ,- []) ++ bs ≡ as ++ b ,- bs
++singleton {as = []} {bs} = refl
++singleton {as = x ,- as} {bs} = cong (x ,-_) ++singleton


++cons : {X : Set} (as bs : List X)(b : X)
    → Σ X \ a' → Σ (List X) \ as' → (as ++ b ,- bs) ≡ (a' ,- (as' ++ bs))
++cons [] bs b = b , [] , refl
++cons (a' ,- as) bs b = a' , as ++ b ,- [] , cong (a' ,-_) (sym (++singleton {as = as}{bs}))

suc : (as bs : List One) → (as ++ ⟨⟩ ,- bs) ≡ ⟨⟩ ,- (as ++ bs)
suc [] bs = refl
suc (⟨⟩ ,- as) bs = cong (⟨⟩ ,-_) (suc as bs)


EqSet : {X : Set} (as bs : List X) → Set → Set
EqSet [] [] P = P
EqSet [] (b ,- bs) _ = One
EqSet (a ,- as) [] _ = One
EqSet (a ,- as) (b ,- bs) P = a ≡ b → as ≡ bs → P

eqSet : ∀{X}{as bs : List X}{P : Set} → as ≡ bs → EqSet as bs P → P
eqSet {as = []} {.[]} refl eq = eq
eqSet {as = x ,- as} {.(x ,- as)} refl p = p refl refl

++helper : {X : Set} {as bs : List X}
       → (Σ X \ a → Σ (List X) \ as' → as ≡ a ,- as')
       → as ++ bs ≡ bs
       → Zero
++helper {as = a' ,- as} {x ,- bs} (.a' , .as , refl) q with ++cons as bs x
... | (a'' , as' , q') = eqSet q (\ {refl ls → ++helper (a'' , as' , refl) (trans (sym q') ls) })


rCancel++ : {X : Set} (as as' bs : List X)
      → as ++ bs ≡ as' ++ bs
      → as       ≡ as'
rCancel++ [] [] bs q = refl
rCancel++ [] (a' ,- as') bs q with () <- ++helper (a' , as' , refl) (sym q)
rCancel++ (a ,- as) [] bs q with () <- ++helper (a , as , refl) q
rCancel++ (a ,- as) (a' ,- as') bs q
  = eqSet q (\ {refl ls → cong (a ,-_) (rCancel++ as as' bs ls)})

helper : ∀{X}{az : BList X}{cs : List X}{bs : List X}
     → (Σ X \c → Σ (List X) \ cs' → cs ≡ c ,- cs')
     → az ⟨⟩⟩ cs ++ bs ≡ bs
     → Zero
helper {az = []} {.(c ,- cs')} {[]} (c , cs' , refl) ()
helper {az = []} cs@{c ,- cs'} {b ,- bs} (.c , .cs' , refl) q with () <- ++helper {as = cs}{b ,- bs} (c , cs' , refl) q
helper {az = az -, a} {cs} {bs} (c , cs' , q') q
  = helper {az = az}{a ,- cs} {bs} (a , (c ,- cs') , cong (a ,-_) q') q

len : {X : Set} → List X → List One
len [] = []
len (_ ,- xs) = _ ,- len xs

nel : {X : Set} → BList X → List One
nel [] = []
nel (xz -, _) = _ ,- nel xz

len++ : {X : Set} (as bs : List X) → len (as ++ bs) ≡ len as ++ len bs
len++ [] bs = refl
len++ (a ,- as) bs = cong (⟨⟩ ,-_) (len++ as bs)

nel++ : {X : Set} (az : BList X)(bs : List X) → len (az ⟨⟩⟩ bs) ≡ nel az ++ len bs
nel++ [] bs = refl
nel++ (az -, a) bs rewrite nel++ az (a ,- bs) = suc (nel az) (len bs)

-- `∀ {A : Set} → A` like polymorphic Zero
noCycle : (x y : List One) → y ≡ ⟨⟩ ,- x ++ y → ∀ {A : Set} → A
noCycle x (⟨⟩ ,- y) q = noCycle x y (eqSet q (\ q' q'' → trans q'' (suc x y)))

rCancelChips : {X : Set}(az az' : BList X)(bs bs' cs : List X)
             → az ⟨⟩⟩ (bs ++ cs) ≡ az' ⟨⟩⟩ (bs' ++ cs)
             → len bs ≡ len bs'
             → az ≡ az' × bs ≡ bs'
rCancelChips [] [] bs bs' cs q q' = refl , rCancel++ bs bs' cs q
rCancelChips [] (az' -, x) bs bs' cs q q'
  with qlen <- cong len q
  rewrite len++ bs cs
        | nel++ az' (x ,- bs' ++ cs)
        | len++ bs' cs
        | q'
        | suc (nel az') (len bs' ++ len cs)
  = noCycle (nel az') (len bs' ++ len cs) qlen
rCancelChips (az -, x) [] bs bs' cs q q'
  with qlen <- sym (cong len q)
  rewrite len++ bs' cs
        | nel++ az (x ,- bs ++ cs)
        | len++ bs cs
        | q'
        | suc (nel az) (len bs' ++ len cs)
  = noCycle (nel az) (len bs' ++ len cs) qlen
rCancelChips (az -, a) (az' -, a') bs bs' cs q q'
  with refl , refl <- rCancelChips az az' (a ,- bs)(a' ,- bs') cs q (cong (⟨⟩ ,-_) q')
  = refl , refl