module Examples where

open import Agda.Builtin.Equality

open import Lib.One
open import Lib.Star

open import Graph
open import Zipper

open import Lib.Nat
open Def Nat Nat Nat
open ZiDef Nat Nat Nat
open Rewriting Nat Nat Nat

module Example (v1 v2 v3 v4 t1 t2 t3 e1 e2 r c1 c2 c3 c4 c5 c6 c7 c8 c9 : Nat) where

  ex-graph : Graph
  ex-graph
    = tree r v1
      (span t1 v2
               (  corner c1 ,- push e1
               ,- corner c2 ,- span t2 v3 (corner c3 ,- push e2 ,- corner c4 ,- [])
               ,- corner c5 ,- [])
      ,- corner c6 ,- pop e2
         ,- corner c7 ,- span t3 v4 (corner c8 ,- pop e1 ,- corner c9 ,- []) ,- [])

  ex-rot-graph : graphToRotations ex-graph
          ≡ (t1 ,- e2 ,- t3 ,- [])
         ,- (e1 ,- t2 ,- t1 ,- [])
         ,- (e2 ,- t2 ,- [])
         ,- (e1 ,- t3 ,- [])
         ,- []
  ex-rot-graph = refl

singleVtx : (r v1 : Nat) → Graph
singleVtx = vertex

rsSingleVtx : (r v1 : Nat) → List (List Nat)
rsSingleVtx r v1 = graphToRotations (singleVtx r  v1)

emptyGraph : (r : Nat) → Graph
emptyGraph = empty

emptyRot : (r : Nat) → List (List Nat)
emptyRot r = graphToRotations (emptyGraph r)

module Bouquet (r v1 e1 e2 c1 c2 c3 : Nat) where

  -- bouquet graph with two self-loops
  ex-bouquet : Graph
  ex-bouquet = tree r v1 (push e1 ,- corner c1
                       ,- push e2 ,- corner c2
                       ,- pop e2  ,- corner c3
                       ,- pop e1 ,- [])

  ex-rot-bouquet : List (List Nat)
  ex-rot-bouquet = graphToRotations ex-bouquet

  rot-bouquet : graphToRotations ex-bouquet ≡ (e1 ,- e2 ,- e2 ,- e1 ,- []) ,- []
  rot-bouquet = refl

module ZipperRootVtx (v1 e1 r c1 : Nat) where

  -- graph with one vertex and one self loop, the focus is on the corner that isn't the root

  zi-root-vtx : Zipper (e1 ,- [])
  zi-root-vtx = root-vtx (reyal v1 r (pop e1 ,- []) ([] -, push e1)) c1

  -- original tree
  ex-oldTree : Graph
  ex-oldTree = ziToOldRoot zi-root-vtx

  root-vtx-oldTree : ziToOldRoot zi-root-vtx
                   ≡ tree r v1 (push e1 ,- corner c1 ,- pop e1 ,- [])
  root-vtx-oldTree = refl

  -- rotation of original tree
  rot-oldTree : graphToRotations ex-oldTree ≡ (e1 ,- e1 ,- []) ,- []
  rot-oldTree = refl

  -- re-root tree to the corner in focus
  ex-newTree : Graph
  ex-newTree = ziToNewRoot zi-root-vtx

  root-vtx-newTree : ziToNewRoot zi-root-vtx
                   ≡ tree c1 v1 (push e1 ,- corner r ,- pop e1 ,- [])
  root-vtx-newTree = refl

  -- rotation of the new tree
  rot-newTree : graphToRotations ex-newTree ≡ (e1 ,- e1 ,- []) ,- []
  rot-newTree = refl

module ZipperReyals  (v1 v2 v3 : Nat)(t1 t2 : Nat) (e1 : Nat)(r c1 c2 c3 c4 c5 : Nat) where

  -- graph with three vertices and three edges (and six corners)

  zi-reyals : Zipper (e1 ,- [])
  zi-reyals
    = reyals (reyal v1 r [] [])
             ([] -, reyal v2 t1
                    (pop e1 ,- corner c5 ,- [])
                    ([] -, corner c1 -, span t2 v3 ([] -, corner c2 -, push e1 -, corner c3 )))
             ⟨⟩
             c4

  -- original tree
  ex-oldTree : Graph
  ex-oldTree = ziToOldRoot zi-reyals

  reyals-oldTree : ziToOldRoot zi-reyals
                 ≡ tree r v1
                        (span t1 v2 (corner c1
                                    ,- span t2 v3 (corner c2 ,- push e1  ,- corner c3 ,- [])
                                    ,- corner c4 ,- pop e1 ,- corner c5 ,- [])
                         ,- [])
  reyals-oldTree = refl

  -- re-rooted tree
  ex-newTree : Graph
  ex-newTree = ziToNewRoot zi-reyals

  reyals-newTree : ziToNewRoot zi-reyals
                 ≡ tree c4 v2
                        (push e1
                        ,- corner c5
                        ,- span t1 v1 (corner r ,- [])
                        ,- corner c1
                        ,- span t2 v3 (corner c2 ,- pop e1 ,- corner c3 ,- [])
                        ,- [])
  reyals-newTree = refl

  -- rotation system of the old tree
  rot-oldTree : graphToRotations ex-oldTree ≡ (t1 ,- []) ,- (t2 ,- e1 ,- t1 ,- []) ,- (e1 ,- t2 ,- []) ,- []
  rot-oldTree = refl


  -- rotation system of the new tree
  rot-newTree : graphToRotations ex-newTree ≡ (e1 ,- t1 ,- t2 ,- []) ,- (t1 ,- []) ,- (e1 ,- t2 ,- []) ,- []
  rot-newTree = refl


module RewritingExamples (v1 v2 v3 : Nat)(t1 t2 : Nat) (e1 : Nat)(r c1 c2 c3 c4 c5 : Nat)
                 (r′ v1′ e1′ e2′ c1′ c2′ c3′ : Nat) where

  open Bouquet
  open ZipperReyals

  rewritingEx = rewriteFocus (zi-reyals v1 v2 v3 t1 t2 e1 r c1 c2 c3 c4 c5) (ex-bouquet r′ v1′ e1′ e2′ c1′ c2′ c3′)


  re-example : rewriteFocus (zi-reyals v1 v2 v3 t1 t2 e1 r c1 c2 c3 c4 c5)
                               (ex-bouquet r′ v1′ e1′ e2′ c1′ c2′ c3′)
   ≡  reyals (reyal v1 r [] [])
            ([] -, reyal v2 t1
                     (push e1′ ,- corner c1′ ,- push e2′ ,- corner c2′
                   ,- pop e2′ ,- corner c3′ ,- pop e1′  ,- corner r′
                   ,- pop e1 ,- corner c5 ,- [])
            ([] -, corner c1 -, span t2 v3 ([] -, corner c2 -, push e1 -, corner c3)))
            ⟨⟩
            c4
  re-example = refl

  toGraph = ziToOldRoot rewritingEx