{-# LANGUAGE NoMonomorphismRestriction, ExtendedDefaultRules #-} {-# LANGUAGE DeriveDataTypeable #-} import Data.Typeable import qualified DeBruijn import qualified HOAS import Convert i = HOAS.Lam \$ \x -> x zero = HOAS.Lam \$ \f -> HOAS.Lam \$ \x -> x one = HOAS.Lam \$ \f -> HOAS.Lam \$ \x -> f `HOAS.App` x two = HOAS.Lam \$ \f -> HOAS.Lam \$ \x -> f `HOAS.App` (f `HOAS.App` x) three = HOAS.Lam \$ \f -> HOAS.Lam \$ \x -> f `HOAS.App` (f `HOAS.App` (f `HOAS.App` x)) plus = HOAS.Lam \$ \m -> HOAS.Lam \$ \n -> HOAS.Lam \$ \f -> HOAS.Lam \$ \x -> m `HOAS.App` f `HOAS.App` (n `HOAS.App` f `HOAS.App` x) plusTwoThree = plus `HOAS.App` two `HOAS.App` three data Nat = Z | S Nat deriving (Show, Typeable) pair = HOAS.Lam \$ \x -> HOAS.Lam \$ \y -> HOAS.Lam \$ \z -> z `HOAS.App` x `HOAS.App` y pairfst = HOAS.Lam \$ \p -> p `HOAS.App` (HOAS.Lam \$ \x -> HOAS.Lam \$ \y -> x) pairsnd = HOAS.Lam \$ \p -> p `HOAS.App` (HOAS.Lam \$ \x -> HOAS.Lam \$ \y -> y) pairfstPair = pairfst `HOAS.App` (pair `HOAS.App` (HOAS.Con 'a') `HOAS.App` (HOAS.Con 'b')) main = do printLine "Identity :" (convert i) printLine "zero :" (convert zero) printLine "one :" (convert one) printLine "two :" (convert two) printLine "three :" (convert three) printLine "plus :" (convert plus) printLine "plus two three :\n " (convert plusTwoThree) printLine "EVAL plus two three:" ((DeBruijn.intp (convert plusTwoThree)) DeBruijn.Empty S Z) printLine "pairfst (pair 'a' 'b'):\n " (convert pairfstPair) printLine "EVAL pairfst (pair 'a' 'b'):" (DeBruijn.intp (convert pairfstPair) DeBruijn.Empty) where printLine desc e = putStrLn \$ desc ++ " " ++ show e