Linear time? conversion of braun trees to lists

braunTree.agda

module braunTree where

open import Data.Nat renaming (_⊔_ to _⊔ℕ_)
open import Data.Empty
open import Data.List
open import Level
open import Function

data Tree {a} (A : Set a) : Set a where
  _⟦_⟧_ : Tree A → A → Tree A → Tree A
  Leaf : Tree A

record Q2 {a b} (B : Set b) (A : Set a) : Set (a ⊔ b) where
  inductive
  constructor code
  field
    unQ2 : (B → B) → (B → B) → A
open Q2

leveln : ℕ → Level
leveln ℕ.zero = Level.zero
leveln (ℕ.suc x) = Level.suc (leveln x)

Q2n : ∀ {b} → (B : Set b) → (n : ℕ) → Set (leveln n ⊔ b)
Q2n B ℕ.zero = Q2 ⊥ B
Q2n B (ℕ.suc n) = Lift (Level.suc (leveln n)) (Q2 (Q2n B n) B)
constQ2 : ∀ {n b} {B : Set b} → B → Q2n B n
constQ2 {ℕ.zero} b = code (λ _ _ → b)
constQ2 {ℕ.suc n} b = lift (code (λ _ _ → b))
unQ2n : ∀ {n b} {B : Set b} → Q2n B n → B
unQ2n {ℕ.zero} x = x .unQ2 id id
unQ2n {ℕ.suc n} x = x .lower .unQ2 id id

untree : ∀ {a}{A : Set a} → Tree A → List A
untree Leaf = []
untree {A = A} (l ⟦ v ⟧ r) = unQ2n (encode (l ⟦ v ⟧ r) (emptyCode _)) where
  height : Tree A → ℕ
  height (l ⟦ v ⟧ r) = ℕ.suc (height l ⊔ℕ height r)
  height Leaf = ℕ.zero
  upQ2nL : ∀ {n m b} {B : Set b} → Q2n B n → Q2n B (n ⊔ℕ m)
  downQ2nL : ∀ {n m b} {B : Set b} → Q2n B (n ⊔ℕ m) → Q2n B n
  upQ2nL {ℕ.zero} {ℕ.zero} b = constQ2 (unQ2n b)
  upQ2nL {ℕ.zero} {ℕ.suc m} b = lift (code (λ ls rs → unQ2n (ls (rs (constQ2 (unQ2n b))))))
  upQ2nL {ℕ.suc n} {ℕ.zero} = id
  upQ2nL {ℕ.suc n} {ℕ.suc m} b = lift (code λ ls rs → b .lower .unQ2 (downQ2nL ∘ ls ∘ upQ2nL) (downQ2nL ∘ rs ∘ upQ2nL))
  downQ2nL {ℕ.zero} {ℕ.zero} = id
  downQ2nL {ℕ.zero} {ℕ.suc m} b = constQ2 (unQ2n b)
  downQ2nL {ℕ.suc n} {ℕ.zero} = id
  downQ2nL {ℕ.suc n} {ℕ.suc m} b = lift (code (λ ls rs → b .lower .unQ2 (upQ2nL ∘ ls ∘ downQ2nL) (upQ2nL ∘ rs ∘ downQ2nL)))
  swapQ2n : ∀ {n m b} {B : Set b} → Q2n B (n ⊔ℕ m) → Q2n B (m ⊔ℕ n)
  swapQ2n {ℕ.zero} {ℕ.zero} = id
  swapQ2n {ℕ.zero} {ℕ.suc m} = id
  swapQ2n {ℕ.suc n} {ℕ.zero} = id
  swapQ2n {ℕ.suc n} {ℕ.suc m} xs = lift (code (λ ls rs → xs .lower .unQ2 (swapQ2n {m} {n} ∘ ls ∘ swapQ2n {n} {m}) (swapQ2n {m} {n} ∘ rs ∘ swapQ2n {n} {m})))
  liftCodingL : ∀ {n m b} {B : Set b} → (Q2n B n → Q2n B n) → Q2n B (n ⊔ℕ m) → Q2n B (n ⊔ℕ m)
  liftCodingL f = upQ2nL ∘ f ∘ downQ2nL
  liftCodingR : ∀ {n m b} {B : Set b} → (Q2n B m → Q2n B m) → (Q2n B (n ⊔ℕ m) → Q2n B (n ⊔ℕ m))
  liftCodingR {n} {m} f = swapQ2n {m} {n} ∘ liftCodingL f ∘ swapQ2n {n} {m}

  encode : (t : Tree A) → Q2n (List A) (height t) → Q2n (List A) (height t)
  encode (l ⟦ v ⟧ r) xs = lift (code λ ls rs → v ∷ xs .lower .unQ2 (ls ∘ liftCodingL (encode l)) (rs ∘ liftCodingR (encode r)))
  encode Leaf xs = code λ _ _ → []
  emptyCode : ∀ n → Q2n (List A) (ℕ.suc n)
  emptyCode ℕ.zero = lift (code λ _ _ → [])
  emptyCode (ℕ.suc n) = lift (code λ ls rs → unQ2n (ls (rs (emptyCode n))))

private
  open import Relation.Binary.PropositionalEquality
  test : untree (((Leaf ⟦ 4 ⟧ Leaf) ⟦ 2 ⟧ (Leaf ⟦ 6 ⟧ Leaf)) ⟦ 1 ⟧ ((Leaf ⟦ 5 ⟧ Leaf) ⟦ 3 ⟧ (Leaf ⟦ 7 ⟧ Leaf))) ≡ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []
  test = refl

  test2 : untree (((Leaf ⟦ 4 ⟧ Leaf) ⟦ 2 ⟧ (Leaf ⟦ 6 ⟧ Leaf)) ⟦ 1 ⟧ Leaf) ≡ 1 ∷ 2 ∷ 4 ∷ 6 ∷ []
  test2 = refl