leonardo.agda

-- Inspired by https://www.fpcomplete.com/user/edwardk/fibonacci/leonardo

open import Data.Nat

module Leonardo (A : Set) where

  -- Tree n is a tree of size the nth Leonardo number
  data Tree : ℕ → Set where
    tip  : A → Tree 0
    tip' : A → Tree 1
    bin  : ∀ {i} → A → Tree i → Tree (1 + i) → Tree (2 + i)
  
  -- Spine' i is a spine starting at index i, with no adjacent indices
  data Spine' : ℕ → Set where
    nil  : ∀ {i} → Spine' i
    skip : ∀ {i} → Spine' (1 + i) → Spine' i
    cons : ∀ {i} → Tree i → Spine' (2 + i) → Spine' i

  data Spine : Set where
    skip : Spine' 1 → Spine
    cons : ∀ {i} → Tree i → Tree (1 + i) → Spine' (3 + i) → Spine

  skips : ∀ {n} → Spine' (suc n) → Spine
  skips {n = zero} x = skip x
  skips {n = suc n} x = skips (skip x)

  cons' : ∀ {n} → Tree n → Spine' (suc n) → Spine
  cons' {n = zero}  (tip x) nil          = skip (cons (tip' x) nil) -- = cons' (tip' x) nil
  cons' {n = zero}  (tip x) (skip xs)    = cons' (tip' x) xs
  cons' {n = suc _} x       nil          = skips (cons x nil)
  cons' {n = suc _} x       (skip xs)    = skips (cons x xs)
  cons' {n = _}     x       (cons xs ys) = cons x xs ys

  _∷_ : A → Spine → Spine
  x ∷ skip xs       = cons' (tip x) xs
  x ∷ cons xs ys zs = cons' (bin x xs ys) zs