{-# language DeriveGeneric #-}
module Blueprint where

import Prelude hiding ( reverse, sum )
import Test.LeanCheck
import Test.LeanCheck.Generic
import GHC.Generics

data Nat = Z | S Nat
     deriving (Eq, Show, Generic)

instance Listable Nat where tiers = genericTiers

plus :: Nat -> Nat -> Nat
plus x y = case x of
     Z -> y
     S x'  -> S ( plus x' y )

double :: Nat -> Nat
double x = case x of
       Z -> Z
       S x' -> S ( S ( double x' ) )

--------------------------

data Bintree a = Leaf | Branch (Bintree a) a (Bintree a)  
     deriving (Eq, Show, Generic)

instance (Listable a) =>  Listable (Bintree a) where tiers = genericTiers

t :: Bintree Nat
t = Branch (Branch Leaf (S Z) Leaf)
     	    Z
     	    (Branch Leaf (S (S Z)) (Branch Leaf Z Leaf) )

size :: Bintree a -> Nat
size t = case t of
  Leaf         -> Z
  Branch l _ r -> S ( plus (size l) (size r) )

doubles :: Bintree Nat -> Bintree Nat
doubles t = case t of
  Leaf         -> Leaf
  Branch l k r -> Branch (doubles l) (double k) (doubles r) 

sum :: Bintree Nat -> Nat
sum t = case t of
  Leaf         -> Z
  Branch l k r -> plus k ( plus (sum l) (sum r) )

test :: Bool
test = and
          [ size t == S (S (S (S Z)))
	  , size (doubles t) == size t
	  , sum (doubles t) == double (sum t)
	  , holds 1000 $ \ t -> size (doubles t) == size t             
	  , holds 1000 $ \ t -> sum (doubles t) == double (sum t)             
	    ]