Skip to content

Instantly share code, notes, and snippets.

@twanvl twanvl/leonardo.agda
Created Apr 28, 2015

Embed
What would you like to do?
-- 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
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.