{-# OPTIONS --cubical --safe #-}

open import Prelude
open import Algebra

module Data.FingerTree {ā„“} {š‘† : Type ā„“} (mon : Monoid š‘†) where

open Monoid mon

record Measured {a} (A : Type a) : Type (a ā„“āŠ” ā„“) where
  constructor measured
  field Ī¼ : A ā†’ š‘†

open Measured ā¦ƒ ... ā¦„ public

data Digit {a} (A : Type a) : Type a where
  Dā‚ : A ā†’ Digit A
  Dā‚‚ : A ā†’ A ā†’ Digit A
  Dā‚ƒ : A ā†’ A ā†’ A ā†’ Digit A

data Node {a} (A : Type a) : Type a where
  Nā‚‚ : A ā†’ A ā†’ Node A
  Nā‚ƒ : A ā†’ A ā†’ A ā†’ Node A

instance
  measuredDigit : ā¦ƒ _ : Measured A ā¦„ ā†’ Measured (Digit A)
  measuredDigit =
    measured Ī» { (Dā‚ x) ā†’ Ī¼ x
               ; (Dā‚‚ x xā‚) ā†’ Ī¼ x āˆ™ Ī¼ xā‚
               ; (Dā‚ƒ x xā‚ xā‚‚) ā†’ Ī¼ x āˆ™ Ī¼ xā‚ āˆ™ Ī¼ xā‚‚
               }

instance
  measuredNode : ā¦ƒ _ : Measured A ā¦„ ā†’ Measured (Node A)
  measuredNode =
    measured Ī» { (Nā‚‚ x xā‚) ā†’ Ī¼ x āˆ™ Ī¼ xā‚
               ; (Nā‚ƒ x xā‚ xā‚‚) ā†’ Ī¼ x āˆ™ Ī¼ xā‚ āˆ™ Ī¼ xā‚‚
               }

record āŸŖ_āŸ« (A : Type a) ā¦ƒ _ : Measured A ā¦„ : Type (a ā„“āŠ” ā„“) where
  constructor recd
  field
    val : A
    mem : š‘†
    prf : Ī¼ val ā‰” mem
open āŸŖ_āŸ« public

memo : ā¦ƒ _ : Measured A ā¦„ ā†’ A ā†’ āŸŖ A āŸ«
memo x = recd x (Ī¼ x) refl

instance
  measuredMemo : ā¦ƒ _ : Measured A ā¦„ ā†’ Measured āŸŖ A āŸ«
  measuredMemo = measured mem

mutual
  record Deep {a} (A : Type a) ā¦ƒ _ : Measured A ā¦„ : Type (a ā„“āŠ” ā„“) where
    pattern
    constructor more
    inductive
    field
      lbuff : Digit A
      tree  : Tree āŸŖ Node A āŸ«
      rbuff : Digit A

  data Tree {a} (A : Type a) ā¦ƒ _ : Measured A ā¦„ : Type (a ā„“āŠ” ā„“) where
    empty : Tree A
    single : A ā†’ Tree A
    deep : āŸŖ Deep A āŸ«  ā†’ Tree A

  Ī¼-deep : āˆ€ {a} {A : Type a} ā¦ƒ _ : Measured A ā¦„ ā†’ Deep A ā†’ š‘†
  Ī¼-deep (more l x r) = Ī¼ l āˆ™ (Ī¼-tree x āˆ™ Ī¼ r)

  Ī¼-tree : āˆ€ {a} {A : Type a} ā¦ƒ _ : Measured A ā¦„ ā†’ Tree A ā†’ š‘†
  Ī¼-tree empty = Īµ
  Ī¼-tree (single x) = Ī¼ x
  Ī¼-tree (deep xs) = xs .mem

  instance
    Measured-Deep : āˆ€ {a} {A : Type a} ā†’ ā¦ƒ _ : Measured A ā¦„ ā†’ Measured (Deep A)
    Measured-Deep = measured Ī¼-deep

  instance
    Measured-Tree : āˆ€ {a} {A : Type a} ā†’ ā¦ƒ _ : Measured A ā¦„ ā†’ Measured (Tree A)
    Measured-Tree = measured Ī¼-tree
open Deep