FingerStar.agda

module FingerStar where

open import Level using (_⊔_)
open import Algebra

open import Data.Empty
open import Data.Product hiding (map)
open import Data.Nat hiding (compare; _⊔_)
open import Data.Nat.Properties
open import Data.Vec renaming (map to mapVec) hiding ([_])

open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR

open import Data.Star

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_)

z = Level.zero

record Category o m e : Set (Level.suc o ⊔ Level.suc m ⊔ Level.suc e) where
  field
    Obj : Set o
    Hom : Obj → Obj → Set m
    _≈_ : ∀ {i j} → Hom i j → Hom i j → Set e

    id  : ∀ {i} → Hom i i
    _∘_ : ∀ {i j k} → Hom j k → Hom i j → Hom i k

  infixr 1 _∘_
  infix  0 _≈_

data Maybe {i a} {I : Set i} (A : I → I → Set a) : I → I → Set (i ⊔ a) where
  nothing : ∀ {i} → Maybe A i i
  just    : ∀ {i j} (x : A i j) → Maybe A i j

maybe : ∀ {i a p} {I : Set i} {A : I → I → Set a} {P : I → I → Set p} {i j} → P i i → (∀ {i j} → A i j → P i j) → Maybe A i j → P i j
maybe z f nothing  = z
maybe z f (just x) = f x

data Digit {i a} {I : Set i} (A : I → I → Set a) : I → I → Set (i ⊔ a) where
  one   : ∀ {i j}       (x : A i j) → Digit A i j
  two   : ∀ {i j k}     (x : A i j) (y : A j k) → Digit A i k
  three : ∀ {i j k l}   (x : A i j) (y : A j k) (z : A k l) → Digit A i l
  four  : ∀ {i j k l m} (x : A i j) (y : A j k) (z : A k l) (w : A l m) → Digit A i m

toStar : ∀ {i a} {I : Set i} {A : I → I → Set a} {i j} → Digit A i j → Star A i j
toStar (one   x) = x ◅ ε
toStar (two   x y) = x ◅ y ◅ ε
toStar (three x y z) = x ◅ y ◅ z ◅ ε
toStar (four  x y z w) = x ◅ y ◅ z ◅ w ◅ ε


measureDigit : ∀ {o m e} (C : Category o m e) → let open Category C in ∀ {e′} {A : Obj → Obj → Set e′} (f : ∀ {i j} → A i j → Hom i j) → ∀ {i j} → Digit A i j → Hom i j
measureDigit C f = elim
  where
  open Category C
  elim : ∀ {i j} → Digit _ i j → Hom i j
  elim (one   x)       = f x
  elim (two   x y)     = f y ∘ f x
  elim (three x y z)   = f z ∘ f y ∘ f x
  elim (four  x y z w) = f w ∘ f z ∘ f y ∘ f x


module Node {o m e} (C : Category o m e) {e′} (A : Category.Obj C → Category.Obj C → Set e′) (f : ∀ {i j} → A i j → Category.Hom C i j) where
  open Category C

  data Node : Obj → Obj → Set (o ⊔ m ⊔ e ⊔ e′) where
     two   : ∀ {i j k}   (m : Hom i k) (x : A i j) (y : A j k)             .(eq : m ≈ f y ∘ f x) → Node i k
     three : ∀ {i j k l} (m : Hom i l) (x : A i j) (y : A j k) (z : A k l) .(eq : m ≈ f z ∘ f y ∘ f x) → Node i l

  measure : ∀ {i j} → Node i j → Hom i j
  measure (two   m _ _ _) = m
  measure (three m _ _ _ _) = m

three′ : ∀ {o m e} {C : Category o m e} → let open Category C in ∀ {e′} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j} {i j k l} (x : A i j) (y : A j k) (z : A k l) → Node.Node C A f i l
three′ {C = C} {f = f} x y z = Node.three (f z ∘ f y ∘ f x) x y z {!!}
  where open Category C


module _ {o m e} (C : Category o m e) where
  open Category C

  open Digit
  open Node C renaming (measure to measureNode)

  mutual
    data FingerTree {e′} {A : Obj → Obj → Set e′} (f : ∀ {i j} → A i j → Hom i j) : Obj → Obj → Set (o ⊔ m ⊔ e ⊔ e′) where
      empty  : ∀ {i} → FingerTree f i i
      single : ∀ {i j} (x : A i j) → FingerTree f i j
      deep   : ∀ {i j k l} (m : Hom i l) (left : Digit A i j) (t : FingerTree (measureNode A f) j k) (right : Digit A k l)
                          .(eq : m ≈ measureDigit C f right ∘ measureTree t ∘ measureDigit C f left) → FingerTree f i l

    measureTree : ∀ {e′} {i j} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j} → FingerTree f i j → Hom i j
    measureTree empty = id
    measureTree {f = f} (single x) = f x
    measureTree (deep m l x r _) = m


  _◂_ : ∀ {e′} {i j k} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j} → A i j → FingerTree f j k → FingerTree f i k
  _◂_ a empty = single a
  _◂_ {f = f} a (single x) = deep (f x ∘ f a) (one a) empty (one x) {!!}
  _◂_ {f = f} a (deep m (one   x)       t r eq) = deep (m ∘ f a) (two   a x)     t r {!!}
  _◂_ {f = f} a (deep m (two   x y)     t r eq) = deep (m ∘ f a) (three a x y)   t r {!!}
  _◂_ {f = f} a (deep m (three x y z)   t r eq) = deep (m ∘ f a) (four  a x y z) t r {!!}
  _◂_ {f = f} a (deep m (four  x y z w) t r eq) = deep (m ∘ f a) (two a x) (three′ y z w ◂ t) r {!!}


  mutual
    appendTree : ∀ {e′} {i j k l} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j}
               → FingerTree f i j
               → Maybe (Digit A) j k
               → FingerTree f k l
               → FingerTree f i l
    appendTree empty ds r     = {!!}
    appendTree l     ds empty = {!!}
    appendTree (single l) ds r          = {!!}
    appendTree l          ds (single r) = {!!}
    appendTree (deep m l t r eq) ds (deep m′ l′ t′ r′ eq′) = deep {!!} l (addDigits t r ds l′ t′) r′ {!!}


    addDigits : ∀ {e′} {i j k l m n} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j}
              → FingerTree (measureNode A f) i j
              → Digit A j k → Maybe (Digit A) k l → Digit A l m
              → FingerTree (measureNode A f) m n
              → FingerTree (measureNode A f) i n
    addDigits t d ds d′ t′ with toStar d ◅◅ maybe ε toStar ds ◅◅ toStar d′
    addDigits t d ds d′ t′ | q = {!!}



  _⋈_ : ∀ {e′} {i j k} {A : Obj → Obj → Set e′} {f : ∀ {i j} → A i j → Hom i j}
      → FingerTree f i j → FingerTree f j k → FingerTree f i k
  t ⋈ s = appendTree t nothing s