Fun with theoretical primitive data structures

data-fun.agda

makeRecord :
  (ks : Set) (o : Relation.Binary ks) →
  {¬refl : ¬ Relation.Reflexive o} {asym : Relation.Asymmetric o} {trans : Relation.Transitive o} →
  {τs : Record ks o $ makeRecord ks o $ λ k τs → Record o τs → Type} →
  ((k : ks) → Record (filter (o k) ks) o (fst $ _≅_.l⇒r joinSplitRecord τs) → get τs k) →
  Record ks o τs
Record :
  (ks : Set) → (o : Relation.Binary ks) →
  {¬refl : ¬ Relation.Reflexive o} {asym : Relation.Asymmetric o} {trans : Relation.Transitive o} →
  Record ks o (makeRecord ks o $ λ k τs → Record o τs → Type) → Type
get : (k : ks) → (r : Record ks o τs) → get τs k (fst $ _≅_.l⇒r joinSplitRecord r)
joinSplitRecord :
  {ks : Set} →
  {rs : Map ks (record : {
    ks' : Set
    o : Relation.Binary ks'
    ¬refl : ¬ Relation.Reflexive o
    asym : Relation.Asymmetric o
    trans : Relation.Transitive o
    τs : Record ks' o $ makeRecord ks' o $ λ k τs → Record o τs → Type
  })} →
  {disj : Disjoint $ map (.ks') rs} →
  Iso
    (let
      ks' = union $ map (.ks') rs
      o = λ c v → let
        kc , pc = Disjoint.reverse c disj
        kv , pv = Disjoint.reverse v disj
        w = get kc rs
      in ∃ c≡v : kc ≡ kv. w.o c (replace ? (sym c≡v) v)
    in Record ks' o $ makeRecord ks' o $ λ k' τs → let
      k , p = Disjoint.reverse k' disj
      w = get k rs
    in get k' w.τs $ fst $ _≅_.l⇒r joinSplitRecord τs)
    (
      Record ks (λ _ _ → False) $
      makeRecord ks (λ _ _ → False) $ λ k _ →
      let w = get k rs in
      Record w.ks' w.o w.τs
    )

map :
  (ks : Set) (oi : Relation.Binary ks) →
  {¬refl-i : ¬ Relation.Reflexive oi} {asym-i : Relation.Asymmetric oi} {trans-i : Relation.Transitive oi} →
  (oo : Relation.Binary ks) →
  {¬refl-o : ¬ Relation.Reflexive oo} {asym-o : Relation.Asymmetric oo} {trans-o : Relation.Transitive oo} →
  {τsi : Record ks oi $ makeRecord ks oi $ λ k τs → Record oi τs → Type} →
  {τo :
    {k : ks} →
    (ro : Record
      (filter (oo k) ks) oo
      (makeRecord (filter (oo k) ks) oo $ λ k ro →
        τo ro $ get k ri)
    ) →
    (v : get k τsi (fst $ _≅_.l⇒r joinSplitRecord ri)) →
    Type
  } →
  (f :
    {k : ks} →
    (ro : Record
      (filter (oo k) ks) oo
      (makeRecord (filter (oo k) ks) oo $ λ k ro →
        τo ro $ get k ri)
    ) →
    (v : get k τsi (fst $ _≅_.l⇒r joinSplitRecord ri)) →
    τo ro v
  ) →
  (ri : Record ks oi τsi) →
  Record ks oo (makeRecord ks oo $ λ k ro → τo ro $ get k ri)