Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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 CCategory.Obj CSet e′) (f : ∀ {i j} → A i jCategory.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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.