, containers
hs-source-dirs: src
default-language: Haskell2010
+
+test-suite doctests
+ type: exitcode-stdio-1.0
+ hs-source-dirs: tests
+ ghc-options: -threaded
+ main-is: doctest.hs
+ build-depends: base
+ , doctest >= 0.8
+ , QuickCheck >= 2.7
+ , text >=1.2 && <1.3
+ , attoparsec >=0.12 && <0.13
+ , containers
+ default-language: Haskell2010
{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
+{-# LANGUAGE PatternSynonyms #-}
module Lambda where
import Control.Applicative
type VarName = String
-data Term = Var VarName | Lambda VarName Term | App Term Term
+data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
+
+pattern RedEx x t s = App (Lambda x t) s
+pattern AppApp a b c = App a (App b c)
+pattern EmLambda x y t = Lambda x (Lambda y t)
+
+-- $setup
+-- >>> import Test.QuickCheck
+-- >>> import Control.Applicative
+-- >>> let aTerm 0 = pure $ Var "x"
+-- >>> let aTerm n = oneof [pure (Var "x"), liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))]
+-- >>> instance Arbitrary Term where arbitrary = sized aTerm
+
+-- | Read and show λ-terms
+--
+-- >>> print $ Lambda "x" (Var "x")
+-- (λx.x)
+--
+-- prop> t == tRead (show (t :: Term))
instance Show Term where
show (Var x) = x
- show (Lambda x t) = "\\" ++ x ++ "." ++ show t
- show (App t r) = "(" ++ show t ++ " " ++ show r ++ ")"
+ show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
+ show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
+ show (AppApp a b c) = show a ++ " " ++ braced (App b c)
+ show (App t r) = show t ++ " " ++ show r
+
+braced :: Term -> String
+braced t = "(" ++ show t ++ ")"
--instance Read Term where
tRead :: String -> Term
parseLambda :: Parser Term
parseLambda = do
- char '\\'
+ char '\\' <|> char 'λ'
vars <- sepBy1 parseVar (char ' ')
char '.'
t <- parseTerm