module Graph where

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

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

open import Lib.List
open import Lib.Star

data Next : Set where
  edge    : Next
  corner  : Next

module Def (V E C : Set) where

  What : Next → Set
  What edge    = E
  What corner  = C

  after : Next → Next
  after edge = corner
  after corner = edge

  -- IxTy is the traversal state type
  TravTy : Set
  TravTy = List E × Next

  variable
    es es′ ds : List E
    as bs as′ bs′ ks ms zs : List E
    k l m : TravTy

  data Step : TravTy → TravTy → Set where
    corner  : (c : C) → Step (es , corner) (es , edge)
    push    : (e : E) → Step (es , edge) (e ,- es , corner)
    pop     : (e : E) → Step (e ,- es , edge) (es , corner)
    span    : (e : E) (v : V) → Star Step (es , corner) (es′ , edge)
              → Step (es , edge) (es′ , corner)

  data Pets : TravTy → TravTy → Set where
    corner  : (c : C) → Pets (es , corner) (es , edge)
    push    : (e : E) → Pets (es , edge) (e ,- es , corner)
    pop     : (e : E) → Pets (e ,- es , edge) (es , corner)
    span    : (e : E) (v : V) → Rats Pets (es , corner) (es′ , edge)
              → Pets (es , edge) (es′ , corner)

-- fish and chips
  _⟨*⟩⟨_ : Rats Pets k l → Star Step l m → Rats Pets k m
  _⟨*⟩⟩_ : Rats Pets k l → Star Step l m → Star Step k m

  [] ⟨*⟩⟩ ss = ss
  (pz -, corner c) ⟨*⟩⟩ ss = pz ⟨*⟩⟩ (corner c ,- ss)
  (pz -, push e) ⟨*⟩⟩ ss = pz ⟨*⟩⟩ (push e ,- ss)
  (pz -, pop e) ⟨*⟩⟩ ss = pz ⟨*⟩⟩ (pop e ,- ss)
  (pz -, span e v pz′) ⟨*⟩⟩ ss = pz ⟨*⟩⟩ (span e v (pz′ ⟨*⟩⟩ []) ,- ss)

  rs ⟨*⟩⟨ [] = rs
  rs ⟨*⟩⟨ (corner c ,- ss) = (rs -, corner c) ⟨*⟩⟨ ss
  rs ⟨*⟩⟨ (push e ,- ss) = (rs -, push e) ⟨*⟩⟨ ss
  rs ⟨*⟩⟨ (pop e ,- ss) = (rs -, pop e) ⟨*⟩⟨ ss
  rs ⟨*⟩⟨ (span e v ss′ ,- ss) = (rs -, span e v ([] ⟨*⟩⟨ ss′)) ⟨*⟩⟨ ss

  data Graph : Set where
    empty   : (r : C) →  Graph
    vertex  : (r : C) → (v : V) → Graph
    tree    : (r : C) → (v : V) → Star Step ([] , edge) ([] , corner) → Graph

  example : (r c : C) (v : V) (e : E) → Graph
  example r c v e = tree r v (push e ,- corner c ,- pop e ,- [])


  starRotation : Star Step k l → (One + E) → List E
  starRotation [] (inl ⟨⟩) = []
  starRotation [] (inr e) = e ,-  []
  starRotation (corner c    ,- s) oe  =       starRotation s oe
  starRotation (push e      ,- s) oe  = e ,-  starRotation s oe
  starRotation (pop e       ,- s) oe  = e ,-  starRotation s oe
  starRotation (span e _ _  ,- s) oe  = e ,-  starRotation s oe

  collect   : Star Step k l → (One + E) → List (List E)
  topLevel  : Star Step k l → (One + E) → List (List E)

  topLevel ss oe = starRotation ss oe ,- collect ss oe

  collect [] oe = []
  collect (span e vs sts ,- ss) oe = topLevel sts (inr e) ++ collect ss oe
  collect (_ ,- ss) oe = collect ss oe


  graphToRotations : Graph → List (List E)
  graphToRotations (empty _) = []
  graphToRotations (vertex r v) = [] ,- []
  graphToRotations (tree r v st) = topLevel st (inl ⟨⟩)