module Zipper 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
open import Graph


module ZiDef (V E C : Set) where

  open Def V E C

  -- ahead  -- upwards (clockwise), i.e. the things we have not yet visited
  -- behind -- downwards (clockwise), i.e. the things we have already visited

  record ZipTy : Set where
    constructor _⟨_⟩_
    field ahead   : List E
          here    : Next
          behind  : List E
  open ZipTy public

  record Layer (s t : ZipTy) : Set where
    constructor layer
    field v     : V
          rats  : Rats Pets (behind s , after (here s)) (behind t , here t)
          this  : What (here t)
          star  : Star Step (ahead t , after (here t)) (ahead s , here s)

  ConLayers : ∀ { t t′ } → Star Layer t t′ → Set
  ConLayers (cons refl { as ⟨ n ⟩ zs } s ss@(_ ,- _)) = n ≡ edge × ConLayers ss
  ConLayers (s ,- []) = One
  ConLayers [] = One

  catConn : ∀{t t′′ : ZipTy}{ t′@(as′ ⟨ n′ ⟩ bs′) : ZipTy } → (n′ ≡ edge)
          → (st : Star Layer t t′) (st′ : Star Layer t′ t′′)
          → ConLayers st → ConLayers st′
          → ConLayers (catStar st st′)
  catConn q [] st′ const const′ = const′
  catConn q (l ,- []) [] const const′ = ⟨⟩
  catConn q (l ,- []) (l′ ,- st′) const const′ = q , const′
  catConn q (l ,- (l′ ,- st)) st′ (q′ , const) const′ = q′ , catConn q (l′ ,- st) st′ const const′

   -- carryingR describes the elements to towards the old root
  CarryingR : ZipTy → Set
  CarryingR (es ⟨ edge ⟩ zs) = Step (es , edge) (zs , corner)
  CarryingR (es ⟨ corner ⟩ zs) = C × es ≡ zs


  layersToNewGraph : (t : ZipTy) → CarryingR t
       → (s : Star Layer t ([] ⟨ corner ⟩ [])) → ConLayers s
       → Graph
  layersToNewGraph .([] ⟨ corner ⟩ []) (s , refl) [] con = empty s

  layersToNewGraph (as ⟨ edge ⟩ zs) c (layer v rats this star ,- []) con
    = tree this v (catStar star (c ,- rats ⟨*⟩⟩ []))

  layersToNewGraph (as ⟨ edge ⟩ zs) c (cons refl {_ ⟨ .edge ⟩ _} (layer v rats this star) ss@(_ ,- _)) (refl , con)
    = layersToNewGraph _ (span this v (catStar star (c ,- rats ⟨*⟩⟩ []))) ss con

  layersToNewGraph (as ⟨ corner ⟩ .as) (c , refl) (layer v rats this star ,- []) con
    = tree this v (catStar star (corner c ,- rats ⟨*⟩⟩ []))

  layersToNewGraph (as ⟨ corner ⟩ .as) (c , refl) (cons refl {_ ⟨ .edge ⟩ _} (layer v rats this star) ss@(_ ,- _)) (refl , con)
    = layersToNewGraph _ (span this v (catStar star (corner c ,- rats ⟨*⟩⟩ []))) ss con


  record Reyal (s t : ZipTy) : Set where
    constructor reyal
    field v     : V
          this  : What (here s)
          star  : Star Step (ahead t , after (here t)) (ahead s , here s)
          rats  : Rats Pets (behind s , after (here s)) (behind t , here t)

  ConReyals : ∀{ t t′ } → Rats Reyal t t′ → Set
  ConReyals (snoc refl { _ ⟨ n ⟩ _ } (rz -, r) r0) =  ConReyals (rz -, r) × (n ≡ edge)
  ConReyals rz = One


  record Partition (as es : List E) : Set where
    constructor part
    field inner   : BList E
          across  : List E
          outer   : List E

          qpop   : as ≡ inner ⟨⟩⟩ across
          qpush  : es ≡ outer ++ across

    turned = outer ++ (rotate inner)
  open Partition public

  -- the things downwards in the zipper (*to* our right)
  {-
  CarryingL : List E → ZipTy → Set
  CarryingL as (es ⟨ edge ⟩ zs)
    = Σ (Partition as es × Partition as zs) λ (p , p′)
    → Σ (Star Layer (turned p ⟨ edge ⟩ turned p′) ([] ⟨ corner ⟩ [])) λ star
    → ConLayers star
  CarryingL as (es ⟨ corner ⟩ zs) -- we′re already at the focus
    = es ≡ [] × zs ≡ []
    × Σ (Star Layer ((rotate ([] <>< as)) ⟨ corner ⟩ (rotate ([] <>< as))) ([] ⟨ corner ⟩ [])) λ star
    → ConLayers star
  -}

  turnStar  : {n m : Next}
            → (p : Partition as es) → Star Step (es , n) (es′ , m)
            → Σ (Partition as es′) λ p′ → Star Step (turned p , n) (turned p′ , m)
  turnStar p [] = p , []
  turnStar p (corner c ,- star)
          with p′ , star′ ← turnStar p star
   = p′ , corner c ,- star′
  turnStar (part bz cs ds qpop refl) (push e ,- star)
          with p′ , star′ ← turnStar (part bz cs (e ,- ds) qpop refl) star
   = p′ , push e ,- star′
  turnStar (part bz (.e ,- cs) [] qpop refl) (pop e ,- star)
          with p′ , star′ ← turnStar (part (bz -, e) cs [] qpop refl) star
   = p′ , push e ,- star′
  turnStar (part bz cs (.e ,- ds) qpop refl) (pop e ,- star)
          with p′ , star′ ← turnStar (part bz cs ds qpop refl ) star
   = p′ , pop e ,- star′
  turnStar p (span e v s ,- star)
          with p′ , s′ ← turnStar p s
          with p′′ , star′ ← turnStar p′ star
   = p′′ , span e v s′ ,- star′
  turnStar (part bz [] [] qpop ()) (pop e ,- star)


  turnRats  : {n m : Next}
            → Rats Pets (es , n) (es′ , m) → (p : Partition as es′)
            → Σ (Partition as es) λ p′ → Rats Pets (turned p′ , n) (turned p , m)
  turnRats [] p = p , []
  turnRats (rats -, corner c) p
           with p′ , rats′ ← turnRats rats p
   = p′ , rats′ -, corner c
  turnRats (rats -, push e) (part bz (.e ,- cs) [] refl refl)
           with p′ , rats′ ← turnRats rats (part (bz -, e) cs [] refl refl)
   = p′ , rats′ -, pop e
  turnRats (rats -, push e) (part bz cs (.e ,- ds) qpop refl)
           with p′ , rats′ ← turnRats rats (part bz cs ds qpop refl)
   = p′ , rats′ -, push e
  turnRats (rats -, pop e) (part bz cs ds qpop refl)
           with p′ , rats′ ← turnRats rats (part bz cs (e ,- ds) qpop refl)
   = p′ , rats′ -, pop e
  turnRats (rats -, span e v r) p
           with p′ , r′ ← turnRats  r p
           with p′′ , rats′ ← turnRats rats p′
   = p′′ , rats′ -, span e v r′
  turnRats (rats -, push e) (part bz [] [] qpop ())


  ConM : (n : Next)
       → (rs : Rats Reyal ([] ⟨ corner ⟩ []) (as ⟨ n ⟩ bs))
       → (ss : Star Layer (as′ ⟨ n ⟩ bs′) ([] ⟨ corner ⟩ []))
       → Set
  ConM n (rs -, r) (s ,- ss) = n ≡ edge
  ConM n rs ss = One

  connect : ∀ { t t′ as zs }
          → (rs : Rats Reyal ([] ⟨ corner ⟩ []) t′) → (r : Reyal t′ t)
          → (ss : Star Layer (as ⟨ here t ⟩ zs) ([] ⟨ corner ⟩ []))
          → ConReyals (rs -, r) → ConM _ (rs -, r) ss → ConLayers ss
          → ConReyals rs
            × (∀ {bs ys} (s : Layer (bs ⟨ here t′ ⟩ ys) (as ⟨ here t ⟩ zs))
            → ConM _ rs (s ,- ss) × ConLayers (s ,- ss))
  fst      (connect []      r ss         conR      conM conS)     = ⟨⟩
  snd      (connect []      r []        conR      conM conS) s   = ⟨⟩ , ⟨⟩
  snd      (connect []      r (_ ,- ss)  conR      conM conS) s   = ⟨⟩ , conM , conS
  fst      (connect (_ -, _) r ss        (conR , q) conM conS)     = conR
  fst (snd (connect (_ -, _) r ss        (conR , q) conM conS) s)  = q
  snd (snd (connect (_ -, _) r []       (conR , q) conM conS) s)  = ⟨⟩
  snd (snd (connect (_ -, _) r (s ,- ss) (conR , q) conM conS) s′) = conM , conS


  turnLayers : (t@(es ⟨ n ⟩ zs) : ZipTy)
             → (rz : Rats Reyal ([] ⟨ corner ⟩ []) t)
             → ConReyals rz
             → What n
             → (pa : Partition as es) → (pb : Partition as zs)
             → (ss : Star Layer (turned pa ⟨ n ⟩ turned pb) ([] ⟨ corner ⟩ []))
             → ConLayers ss
             → ConM n rz ss
             → Graph
  turnLayers .([] ⟨ corner ⟩ []) [] conR this (part pd .[] [] qpop refl) (part pd′ .[] [] qpop′ refl) ss conS conM
    with (refl , refl) ← rCancelChips pd′ pd [] [] [] (trans (sym (qpop′)) qpop) refl
    = layersToNewGraph ((rotate pd ⟨ corner ⟩ rotate pd′)) (this , refl) ss conS
    -- at this point, `rotate pd` and `rotate pd′` are the same, and `this` is a corner (of type C)

  -- turn the next reyal into a layer (and update the Partition)
  turnLayers t (rz -, r@(reyal v this star rats)) cR this′ pa pb ss cS cM
   = let  (pa′ , star′)  = turnStar pa star
          (pb′ , rats′)  = turnRats rats pb
          (cR′ , cM′)    = connect rz r ss cR cM cS
          s         = layer v rats′ this′ star′
          (c , c′)  = cM′ s
      in turnLayers _ rz cR′ this pa′ pb′ (s ,- ss) c′ c

  turnLayers .([] ⟨ corner ⟩ []) [] conR
            this (part inner₁ .[] [] qpop₁ refl) (part inner₂ across₁ (x₅ ,- outer₁) qpop₂ ())
            ss conS conM

  turnLayers .([] ⟨ corner ⟩ []) [] conR
            this (part inner₁ across₁ (x₅ ,- outer₁) qpop₁ ()) (part inner₂ across₂ outer₂ qpop₂ qpush₂)
            ss conS conM



  toLayers : { n : Next }
           → (rz : Rats Reyal (as ⟨ edge ⟩ bs) (ks ⟨ n ⟩ ms)) → ConReyals rz
           → (focus : What n)
           → E × Σ (Star Layer (as ⟨ edge ⟩ bs) (ks ⟨ n ⟩ ms)) λ ss  → ConLayers ss

  toLayers [] con e = e , [] , ⟨⟩
  toLayers ([] -, reyal v this star rats) ⟨⟩ n = this , layer v rats n star ,- [] , ⟨⟩
  toLayers (rz@(_ -, _) -, reyal v this star rats) (con , refl) n
    = let (e , ls , con′) = toLayers rz con this
      in e , catStar ls (layer v rats n star ,- []) , catConn refl ls _ con′ ⟨⟩


  layersToSteps : (ss : Star Layer (zs ⟨ edge ⟩ as) (ms ⟨ corner ⟩ ms)) → ConLayers ss
                → Star Step (as , corner) (zs , edge)
  layersToSteps (layer v rats this star ,- []) con
    = rats ⟨*⟩⟩ (corner this ,- star)
  layersToSteps (layer v rats this star ,- ss@(_ ,- _)) (refl , con)
    = let st′ = layersToSteps ss con
      in rats ⟨*⟩⟩ (span this v st′ ,- star)


  starToGraph : ∀{ ms as bs } → C
              → (s : Layer ([] ⟨ corner ⟩ []) (as ⟨ edge ⟩ bs))
              → (ss : Star Layer (as ⟨ edge ⟩ bs) (ms ⟨ corner ⟩ ms))
              → ConLayers ss
              → Graph
  starToGraph c (layer v rats this star) ss@(layer v′ _ _ _ ,- _) con
    = let st = layersToSteps ss con
      in tree c v (rats ⟨*⟩⟩ (span this v′ st ,- star))



  data Zipper : List E → Set where
    empty     : C → Zipper []
    vertex    : C → V → Zipper []
    root      : C → V → Star Step ([] , edge) ([] , corner) → Zipper []
    root-vtx  : (r : Reyal ([] ⟨ corner ⟩ []) (es ⟨ corner ⟩ es)) → C → Zipper es
    reyals    : (r : Reyal ([] ⟨ corner ⟩ []) (ds ⟨ edge ⟩ ds))
              → (rz : Rats Reyal (ds ⟨ edge ⟩ ds) (es ⟨ corner ⟩ es))
              → ConReyals rz
              → C → Zipper es



  ziToNewRoot : {as : List E} → Zipper as → Graph
  ziToNewRoot (empty r) = empty r
  ziToNewRoot (vertex r v) = vertex r v
  ziToNewRoot (root r v st) = tree r v st

  ziToNewRoot { as } (root-vtx r@(reyal v this star rats) c)
    = turnLayers {as} (as ⟨ corner ⟩ as) ([] -, r) _ c
                 (part [] as [] refl refl)
                 (part [] as [] refl refl) [] _ _

  ziToNewRoot { as } (reyals r rz cR c)
    = turnLayers {as} (as ⟨ corner ⟩ as) (catRats ([] -, r) rz) (conr r rz cR) c
                 (part [] as [] refl refl)
                 (part [] as [] refl refl) [] ⟨⟩ (conm r rz)

    where

     conr : {ds : List E} {s t : ZipTy}
            (r : Reyal s (ds ⟨ edge ⟩ ds))
            (rz : Rats Reyal (ds ⟨ edge ⟩ ds) t)
            (cR : ConReyals rz)
            → ConReyals (catRats ([] -, r) rz)
     conr r [] ⟨⟩ = ⟨⟩
     conr r ([] -, r1) cR = ⟨⟩ , refl
     conr r (rz -, r2 -, r1) (cR , q) = conr r (rz -, r2) cR , q

     conm : (r : Reyal ([] ⟨ corner ⟩ []) (ds ⟨ edge ⟩ ds))
             (rz : Rats Reyal (ds ⟨ edge ⟩ ds) (as ⟨ corner ⟩ as))
             → ConM corner (catRats ([] -, r) rz) []
     conm r' (rz -, r) = ⟨⟩


  ziToOldRoot : { as : List E } → Zipper as → Graph
  ziToOldRoot (empty r) = empty r
  ziToOldRoot (vertex r v) = vertex r v
  ziToOldRoot (root r v st) = tree r v st
  ziToOldRoot (root-vtx (reyal v r star rats) c)
    = tree r v (rats ⟨*⟩⟩ (corner c ,- star))
  ziToOldRoot (reyals (reyal v r star rats) rz cR c)
    = let (e , ls , cS) = toLayers rz cR c
      in starToGraph r (layer v rats e star) ls cS

  -- example: move the root one corner along at the root node
  moveR : Graph → Graph
  moveR (empty r) = empty r
  moveR (vertex r v) = vertex r v
  moveR t@(tree r v (st ,- [])) = t
  moveR (tree r v (st ,- corner c ,- sts))
    =  ziToNewRoot (root-vtx (reyal v r sts ([] ⟨*⟩⟨ (st ,- []))) c)



module Rewriting (V E C : Set) where

  open Def V E C
  open ZiDef V E C


  castStep : { as bs cs : List E } { c d : Next }
           → Step (as , c) (bs , d)
           → Step (concat as cs , c) (concat bs cs , d)

  castStar : {as bs cs : List E} {c d : Next}
           → Star Step (as , c) (bs , d)
           → Star Step (concat as cs , c)(concat bs cs , d)

  castStep (Def.corner c) = corner c
  castStep (Def.push e) = push e
  castStep (Def.pop e) = pop e
  castStep (Def.span e v ss) = span e v (castStar ss)

  castStar [] = []
  castStar (s ,- ss) = castStep s ,- castStar ss

  rewriteFocus : { es : List E } → Zipper es → Graph → Zipper es
  rewriteFocus (empty r) (empty r′) = empty r′
  rewriteFocus (empty r) (vertex r′ v) = vertex r′ v
  rewriteFocus (empty r) (tree r′ v ss) = root r′ v ss
  rewriteFocus (vertex r v) (empty r′) = vertex r′ v
  rewriteFocus (vertex r v) (vertex r′ v′) = vertex r′ v′
  rewriteFocus (vertex r v) (tree r′ v′ ss) = root r′ v′ ss
  rewriteFocus (root r v ss) (empty r′) = root r v ss
  rewriteFocus (root r v ss) (vertex r′ v′) = root r v′ ss


  rewriteFocus (root r v ss) (tree r′ v′ ss′) = root r v (concat ss′ (corner r′ ,- ss))
  rewriteFocus (root-vtx rey c) (empty r′) = root-vtx rey r′
  rewriteFocus (root-vtx rey c) (vertex r′ v′) = root-vtx rey r′
  rewriteFocus (root-vtx (reyal v this star rats) c) (tree r′ v′ ss)
    = root-vtx (reyal v′ this (concat (castStar ss) (corner r′ ,- star)) rats) c
  rewriteFocus (reyals r rz cR c) (empty r′) = reyals r rz cR r′
  rewriteFocus (reyals (reyal v this star rats) rz cR c) (vertex r′ v′) = reyals (reyal v′ this star rats) rz cR r′
  -- need to refine the reyal structure further because of ConReyals:
  rewriteFocus (ZiDef.reyals r ([] -, ZiDef.reyal v this star rats) ⟨⟩ c) (Def.tree r′ v′ ss′)
    = reyals r ([] -, reyal v this (concat (castStar ss′) (corner r′ ,- star)) rats) ⟨⟩ c
  rewriteFocus (ZiDef.reyals r (rz -, rey′ -, ZiDef.reyal v this star rats) (cR , h) c) (Def.tree r′ v′ ss′)
    = reyals r (rz -, rey′ -, reyal v this (concat (castStar ss′) (corner r′ ,- star)) rats) (cR , h) c