twanvl

data Spine a
  = NS (NS a a (a,a,a))
  | AS (AS a a a)
  deriving (Show)

-- non-adjacent spine: list of increasing size trees, with no two trees of adjacent index
data NS a b c
  = Nil
  | NMore (NS a c (a,b,c))
  | NCons b (NS a (a,b,c) (a,c,(a,b,c)))

twanvl

{-# LANGUAGE ImplicitParams #-}
import Control.Monad
import Control.Monad.Fix
import Control.Applicative
import Control.Concurrent
import Control.Concurrent.MVar
import Control.Exception
import Prelude hiding (catch)
import Data.IORef
import Data.Traversable

twanvl

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds, GADTs #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.Exts

-- see http://www.reddit.com/r/haskell/comments/117r1p/whats_wrong_with_ghc_haskells_current_constraint/

data Dict :: Constraint -> * where
    Dict :: c => Dict c

twanvl

{-
http://noamlewis.wordpress.com/2013/02/12/penalty-search-problem-revisited-dynamic-programming-control-parallel-to-the-rescue/

-}

import Data.MemoCombinators

--f k = fromIntegral k

data CostTree

twanvl

{-# OPTIONS --without-K #-}
module 2013-06-26-midpoints where

{-

This is a proof that the HIT

data S A where
    [_] : A -> S A;
    mid : {x y : A} -> Id x y -> Id [ x ] [ y ]

twanvl

module 2013-11-13-confluence-problem where

open import 2013-11-13-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP

twanvl

module 2013-12-20-confluence-problem-v2 where

open import 2013-12-20-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP

twanvl

module 2013-11-13-relations where

open import Level hiding (zero;suc)
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
open import Data.Product using (∃)
open import Induction.WellFounded

twanvl

{-#LANGUAGE NoMonomorphismRestriction #-}
module Main (main) where

import Control.Monad (void)
import Control.Monad.Identity
import Criterion.Main
import qualified Data.Conduit      as C
import qualified Data.Conduit.Combinators as CC
import qualified Data.Conduit.List as C
import qualified Data.Machine      as M

twanvl

-- 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