{-# LANGUAGE GADTs, KindSignatures, DataKinds, StandaloneDeriving #-}
module Main where
import Test.HUnit
import Data.List
data Nat = Zero | Succ Nat
data Mountains :: Nat -> * where
End :: Mountains Zero
Up :: Mountains (Succ k) -> Mountains k
Equal :: Mountains k -> Mountains k
Down :: Mountains k -> Mountains (Succ k)
deriving instance Show (Mountains k)
type Alpen = Mountains Zero
mountains :: Mountains k -> [Int]
mountains End = [0]
mountains (Up ms) = 0:map (+1) (mountains ms)
mountains (Equal ms) = 0:mountains ms
mountains (Down ms) = 0:map (\x->x-1) (mountains ms)
class Generate (k :: Nat) where
generate :: Int -> [Mountains k]
instance Generate Zero where
generate 0 = [End]
generate n = map Up (generate (n-1))
++ map Equal (generate (n-1))
instance Generate k => Generate (Succ k) where
generate 0 = []
generate n = map Up (generate (n-1))
++ map Equal (generate (n-1))
++ map Down (generate (n-1))
main = runTestTT $ test [ "example" ~: sort (map mountains ((generate 4) :: [Alpen]))
~?=
[ [0,0,0,0,0]
, [0,0,0,1,0]
, [0,0,1,0,0]
, [0,0,1,1,0]
, [0,1,0,0,0]
, [0,1,0,1,0]
, [0,1,1,0,0]
, [0,1,1,1,0]
, [0,1,2,1,0] ]
]