{-# 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 List a = Nil | Cons a (List a)
    deriving (Eq, Show, Generic)

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

doubles :: List Nat -> List Nat
doubles xs = case xs of
  Nil -> Nil
  Cons x xss -> Cons ( double x ) ( doubles xss )

t1 = Cons (S Z) ( Cons (S (S Z )) Nil)
t2 = doubles t1

sum :: List Nat -> Nat
sum xs = case xs of
    Nil        -> Z
    Cons x xss -> plus x ( sum xss )

t3 = sum t1
t4 = sum t2
t5 = t4 == double t3

test1 :: Bool
test1 = and
         [ sum (Cons Z Nil) == Z
	 , sum ( doubles (Cons Z Nil) ) == double ( sum (Cons Z Nil) )
         , holds 1000 $ \ xs ->
                sum ( doubles (xs :: List Nat) )
	       	== double ( sum xs )
         ]

append :: List a -> List a -> List a
append xs ys = case xs of
  Nil        -> ys
  Cons x xss -> Cons x (append xss ys)

t6 = append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t7 = append ( Cons (S (S Z )) Nil) (Cons (S Z) (Cons Z Nil))
t8 = append ( Cons 1 ( Cons 2 Nil)) (Cons 3 Nil)

len :: List a -> Nat
len xs = case xs of
    Nil        -> Z
    Cons x xss -> S ( len xss )

t9 = append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t10 = doubles $ append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t11 = len t9
t12 = len t10
t13 = t11 == t12

test2 :: Bool
test2 = and
         [ len (Cons Z Nil) == S Z
	 , len (append t1 (Cons Z Nil)) == plus (len  t1) (len (Cons Z Nil))
         , holds 1000 $ \ xs ys ->
               len ( append (xs :: List Bool) (ys :: List Bool)) ==
	       plus ( len xs ) ( len ys )
         ]