lambda-calculator (empty) → 0.5.0
raw patch · 19 files changed
+850/−0 lines, 19 filesdep +HUnitdep +Shellacdep +Shellac-readlinesetup-changed
Dependencies added: HUnit, Shellac, Shellac-readline, base, hspec, lambda-calculator, parsec
Files
- LICENSE +20/−0
- Setup.hs +2/−0
- app/Main.hs +42/−0
- lambda-calculator.cabal +60/−0
- src/Language/Lambda.hs +27/−0
- src/Language/Lambda/Eval.hs +43/−0
- src/Language/Lambda/Expression.hs +51/−0
- src/Language/Lambda/Parser.hs +46/−0
- src/Language/Lambda/PrettyPrint.hs +50/−0
- test/Language/Lambda/EvalSpec.hs +88/−0
- test/Language/Lambda/Examples/BoolSpec.hs +109/−0
- test/Language/Lambda/Examples/NatSpec.hs +103/−0
- test/Language/Lambda/Examples/PairSpec.hs +39/−0
- test/Language/Lambda/ExpressionSpec.hs +40/−0
- test/Language/Lambda/HspecUtils.hs +8/−0
- test/Language/Lambda/ParserSpec.hs +54/−0
- test/Language/Lambda/PrettyPrintSpec.hs +37/−0
- test/Language/LambdaSpec.hs +30/−0
- test/Spec.hs +1/−0
+ LICENSE view
@@ -0,0 +1,20 @@+The MIT License (MIT)++Copyright (c) 2016 Sean D Gillespie++Permission is hereby granted, free of charge, to any person obtaining a copy of+this software and associated documentation files (the "Software"), to deal in+the Software without restriction, including without limitation the rights to+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies+of the Software, and to permit persons to whom the Software is furnished to do+so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,42 @@+module Main where++import Data.Version++import System.Console.Shell+import System.Console.Shell.ShellMonad+import System.Console.Shell.Backend.Readline (readlineBackend)++import Language.Lambda+import Paths_lambda_calculator++main :: IO ()+main = runShell mkShellDesc readlineBackend ()++mkShellDesc :: ShellDescription ()+mkShellDesc = shellDesc' $ mkShellDescription commands eval+ where shellDesc' d = d {+ greetingText = Just shellGreeting,+ prompt = shellPrompt+ }++shellGreeting :: String+shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"+ +shellPrompt :: s -> IO String+shellPrompt _ = return "λ > "++commands :: [ShellCommand s]+commands = [exitCommand "q",+ helpCommand "h"]++eval :: String -> Sh s ()+eval = either shellPutErrLn' shellPutStrLn' . evalString+ where shellPutErrLn' :: Show s => s -> Sh s' ()+ shellPutErrLn' = shellPutErrLn . show++ shellPutStrLn' :: PrettyPrint s => s -> Sh s' ()+ shellPutStrLn' = shellPutStrLn . prettyPrint++version' :: String+version' = showVersion version+
+ lambda-calculator.cabal view
@@ -0,0 +1,60 @@+name: lambda-calculator+version: 0.5.0+synopsis: A lambda calculus interpreter+description: Please see README.md+homepage: https://github.com/sgillespie/lambda-calculus#readme+license: MIT+license-file: LICENSE+author: Sean D Gillespie+maintainer: sean@mistersg.net+copyright: 2016 Sean Gillespie+category: LambdaCalculus,Language,Teaching+build-type: Simple+-- extra-source-files:+cabal-version: >=1.10++library+ hs-source-dirs: src+ exposed-modules: Language.Lambda,+ Language.Lambda.Expression,+ Language.Lambda.Eval,+ Language.Lambda.Parser,+ Language.Lambda.PrettyPrint+ build-depends: base <= 5,+ parsec+ default-language: Haskell2010++executable lambda-calculator+ hs-source-dirs: app+ main-is: Main.hs+ other-modules: Paths_lambda_calculator+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends: base,+ lambda-calculator,+ Shellac,+ Shellac-readline+ default-language: Haskell2010++test-suite lambda-calculus-test+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ other-modules: Language.LambdaSpec,+ Language.Lambda.Examples.BoolSpec,+ Language.Lambda.Examples.NatSpec,+ Language.Lambda.Examples.PairSpec,+ Language.Lambda.ExpressionSpec,+ Language.Lambda.EvalSpec,+ Language.Lambda.HspecUtils,+ Language.Lambda.ParserSpec,+ Language.Lambda.PrettyPrintSpec+ build-depends: base <= 5,+ lambda-calculator,+ hspec,+ HUnit+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/sgillespie/lambda-calculus
+ src/Language/Lambda.hs view
@@ -0,0 +1,27 @@+module Language.Lambda (+ LambdaExpr(..),+ PrettyPrint(..),+ evalExpr,+ evalString,+ parseExpr,+ uniques,+ ) where++import Control.Monad+import Text.Parsec++import Language.Lambda.Eval+import Language.Lambda.Expression+import Language.Lambda.Parser+import Language.Lambda.PrettyPrint++evalString :: String -> Either ParseError (LambdaExpr String)+evalString = liftM (evalExpr uniques) . parseExpr++-- TODO[sgillespie]: Uniques should be [a..z, a0..z0, a1..z1] etc+-- concatMap (\x -> map (\y -> y:x) ['a'..'z']) ([""] ++ map show [0..])+ +uniques :: [String]+uniques = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix+ where suffix = [""] ++ map show [(0::Int)..]+
+ src/Language/Lambda/Eval.hs view
@@ -0,0 +1,43 @@+module Language.Lambda.Eval where++import Data.List+import Data.Maybe++import Language.Lambda.Expression++evalExpr :: Eq n => [n] -> LambdaExpr n -> LambdaExpr n+evalExpr uniqs (Abs name expr) = Abs name . evalExpr uniqs $ expr+evalExpr _ expr@(Var _) = expr+evalExpr uniqs (App e1 e2) = betaReduce uniqs (evalExpr uniqs e1)+ (evalExpr uniqs e2)++betaReduce :: Eq n => [n] -> LambdaExpr n -> LambdaExpr n -> LambdaExpr n+betaReduce uniqs (App e1 e1') e2 = App (betaReduce uniqs e1 e1') e2+betaReduce _ expr@(Var _) e2 = App expr e2+betaReduce uniqs (Abs n e1) e2 = evalExpr uniqs . sub n e1' $ e2+ where fvs = freeVarsOf e2+ e1' = alphaConvert uniqs fvs e1++alphaConvert :: Eq n => [n] -> [n] -> LambdaExpr n -> LambdaExpr n+alphaConvert uniqs freeVars (Abs name body)+ | name `elem` freeVars = Abs uniq . sub name body . Var $ uniq+ | otherwise = Abs name . alphaConvert uniqs freeVars $ body+ where uniq = fromMaybe name (find (`notElem` freeVars) uniqs)+alphaConvert _ _ e = e++sub :: Eq n => n -> LambdaExpr n -> LambdaExpr n -> LambdaExpr n+sub name b@(Var name') expr+ | name == name' = expr+ | otherwise = b++sub name b@(Abs name' expr') expr+ | name == name' = b+ | otherwise = Abs name' (sub name expr' expr)++sub name (App e1 e2) expr = App (sub name e1 expr)+ (sub name e2 expr)++freeVarsOf :: Eq n => LambdaExpr n -> [n]+freeVarsOf (Abs n expr) = filter (/=n) . freeVarsOf $ expr+freeVarsOf (App e1 e2) = freeVarsOf e1 ++ freeVarsOf e2+freeVarsOf (Var n) = [n]
+ src/Language/Lambda/Expression.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.Lambda.Expression where++import Prelude hiding (abs, uncurry)++import Language.Lambda.PrettyPrint++data LambdaExpr name+ = Var name+ | App (LambdaExpr name) (LambdaExpr name)+ | Abs name (LambdaExpr name)+ deriving (Eq, Show)++-- Pretty printing+instance PrettyPrint a => PrettyPrint (LambdaExpr a) where+ prettyPrint = prettyPrint . pprExpr empty++-- Pretty print a lambda expression+pprExpr :: PrettyPrint n => PDoc String -> LambdaExpr n -> PDoc String+pprExpr pdoc (Var n) = prettyPrint n `add` pdoc+pprExpr pdoc (Abs n body) = pprAbs pdoc n body+pprExpr pdoc (App e1 e2) = pprApp pdoc e1 e2++-- Pretty print an abstraction +pprAbs :: PrettyPrint n => PDoc String -> n -> LambdaExpr n -> PDoc String+pprAbs pdoc n body+ = between vars' [lambda] ". " (pprExpr pdoc body')+ where (vars, body') = uncurry n body+ vars' = intercalate (map prettyPrint vars) " " empty++-- Pretty print an application+pprApp :: PrettyPrint n+ => PDoc String+ -> LambdaExpr n+ -> LambdaExpr n+ -> PDoc String+pprApp pdoc e1@(Abs _ _) e2@(Abs _ _) = betweenParens (pprExpr pdoc e1) pdoc+ `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)+pprApp pdoc e1 e2@(App _ _) = pprExpr pdoc e1+ `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)+pprApp pdoc e1 e2@(Abs _ _) = pprExpr pdoc e1+ `mappend` addSpace (betweenParens (pprExpr pdoc e2) pdoc)+pprApp pdoc e1@(Abs _ _) e2 = betweenParens (pprExpr pdoc e1) pdoc+ `mappend` addSpace (pprExpr pdoc e2)+pprApp pdoc e1 e2+ = pprExpr pdoc e1 `mappend` addSpace (pprExpr pdoc e2)++uncurry :: n -> LambdaExpr n -> ([n], LambdaExpr n)+uncurry n body = uncurry' [n] body+ where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'+ uncurry' ns body' = (reverse ns, body')
+ src/Language/Lambda/Parser.hs view
@@ -0,0 +1,46 @@+module Language.Lambda.Parser (parseExpr) where++import Control.Monad+import Prelude hiding (abs, curry, id)++import Text.Parsec+import Text.Parsec.String++import Language.Lambda.Expression++parseExpr :: String -> Either ParseError (LambdaExpr String)+parseExpr = parse (whitespace *> expr <* eof) ""++expr :: Parser (LambdaExpr String)+expr = try app <|> term++term :: Parser (LambdaExpr String)+term = abs <|> var <|> parens++var :: Parser (LambdaExpr String)+var = Var <$> identifier++abs :: Parser (LambdaExpr String)+abs = curry <$> idents <*> expr+ where idents = (symbol '\\') *> many1 identifier <* (symbol '.')+ curry = flip (foldr Abs)++app :: Parser (LambdaExpr String)+app = chainl1 term (return App)++parens :: Parser (LambdaExpr String)+parens = symbol '(' *> expr <* symbol ')'++lexeme :: Parser a -> Parser a+lexeme p = p <* whitespace++whitespace :: Parser ()+whitespace = void . many . oneOf $ " \t"++identifier :: Parser String+identifier = lexeme ((:) <$> first <*> many rest)+ where first = letter <|> char '_'+ rest = first <|> digit++symbol :: Char -> Parser ()+symbol = void . lexeme . char
+ src/Language/Lambda/PrettyPrint.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.Lambda.PrettyPrint where++import qualified Data.List as L++class PrettyPrint a where+ prettyPrint :: a -> String++instance PrettyPrint String where+ prettyPrint = id+ +newtype PDoc s = PDoc [s]+ deriving (Eq, Show)++instance PrettyPrint s => PrettyPrint (PDoc s) where+ prettyPrint (PDoc ls) = concat . map prettyPrint $ ls++instance Monoid (PDoc s) where+ mempty = empty+ (PDoc p1) `mappend` (PDoc p2) = PDoc $ p1 ++ p2++instance Functor PDoc where+ fmap f (PDoc ls) = PDoc (fmap f ls)++empty :: PDoc s+empty = PDoc []++add :: s -> PDoc s -> PDoc s+add s (PDoc ps) = PDoc (s:ps)++append :: [s] -> PDoc s -> PDoc s+append = mappend . PDoc++between :: PDoc s -> s -> s -> PDoc s -> PDoc s+between (PDoc str) start end pdoc = PDoc ((start:str) ++ [end]) `mappend` pdoc++betweenParens :: PDoc String -> PDoc String -> PDoc String+betweenParens doc = between doc "(" ")"++intercalate :: [[s]] -> [s] -> PDoc [s] -> PDoc [s]+intercalate ss sep = add $ L.intercalate sep ss++addSpace :: PDoc String -> PDoc String+addSpace = add [space]+ +space :: Char+space = ' '++lambda :: Char+lambda = 'λ'
+ test/Language/Lambda/EvalSpec.hs view
@@ -0,0 +1,88 @@+module Language.Lambda.EvalSpec where++import Test.Hspec++import Language.Lambda+import Language.Lambda.Eval+import Language.Lambda.Expression++spec :: Spec+spec = do+ describe "evalExpr" $ do+ let evalExpr' = evalExpr uniques+ + it "beta reduces" $ do+ let expr = App (Abs "x" (Var "x")) (Var "z")+ evalExpr' expr `shouldBe` Var "z"++ it "reduces multiple applications" $ do+ let expr = App (App (Abs "f" (Abs "x" (App (Var "f") (Var "x")))) (Var "g")) (Var "y")+ evalExpr' expr `shouldBe` App (Var "g") (Var "y")++ it "reduces inner redexes" $ do+ let expr = Abs "x" (App (Abs "y" (Var "y")) (Var "x"))+ evalExpr' expr `shouldBe` Abs "x" (Var "x")++ it "reduces with name captures" $ do+ let expr = App (Abs "f" (Abs "x" (App (Var "f") (Var "x"))))+ (Abs "f" (Var "x"))+ evalExpr' expr `shouldBe` Abs "z" (Var "x")++ describe "betaReduce" $ do+ let betaReduce' = betaReduce []+ + it "reduces simple applications" $ do+ let e1 = Abs "x" (Var "x")+ e2 = (Var "y")+ betaReduce' e1 e2 `shouldBe` Var "y"++ it "reduces nested abstractions" $ do+ let e1 = Abs "x" (Abs "y" (Var "x"))+ e2 = Var "z"+ betaReduce' e1 e2 `shouldBe` Abs "y" (Var "z")++ it "reduces inner applications" $ do+ let e1 = Abs "f" (App (Var "f") (Var "x"))+ e2 = Var "g"+ betaReduce' e1 e2 `shouldBe` App (Var "g") (Var "x")++ it "does not reduce unreducible expression" $ do+ let e1 = Var "x"+ e2 = Var "y"+ betaReduce' e1 e2 `shouldBe` App (Var "x") (Var "y")++ it "does not reduce irreducible chained applications" $ do+ let e1 = App (Var "x") (Var "y")+ e2 = Var "z"+ betaReduce' e1 e2 `shouldBe` App (App (Var "x") (Var "y")) (Var "z")++ it "does not sub shadowed bindings" $ do+ let e1 = Abs "x" (Abs "x" (Var "x"))+ e2 = Var "z"+ betaReduce' e1 e2 `shouldBe` Abs "x" (Var "x")++ describe "alphaConvert" $ do+ it "alpha converts simple expressions" $ do+ let freeVars = ["x"]+ expr = Abs "x" (Var "x")+ uniques = ["y"]+ alphaConvert uniques freeVars expr `shouldBe` Abs "y" (Var "y")+ + it "avoids captures" $ do+ let freeVars = ["x"]+ expr = Abs "x" (Var "x")+ uniques = ["x", "y"]+ alphaConvert uniques freeVars expr `shouldBe` Abs "y" (Var "y")++ describe "freeVarsOf" $ do+ it "Returns simple vars" $ do+ freeVarsOf (Var "x") `shouldBe` ["x"]+ + it "Does not return bound vars" $ do+ freeVarsOf (Abs "x" (Var "x")) `shouldBe` []++ it "Returns nested simple vars" $ do+ freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"]++ it "Returns applied simple vars" $ do+ freeVarsOf (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]
+ test/Language/Lambda/Examples/BoolSpec.hs view
@@ -0,0 +1,109 @@+module Language.Lambda.Examples.BoolSpec where++import Test.Hspec++import Language.Lambda.HspecUtils++spec :: Spec+spec = do+ describe "Bool" $ do+ -- Bool is the definition of Booleans. We represent bools+ -- using Church Encodings:+ --+ -- true: \t f. t+ -- false: \t f. f+ describe "and" $ do+ -- The function and takes two Bools and returns true+ -- iff both arguments are true+ -- + -- and(true, true) = true+ -- and(false, true) = false+ -- and(true, false) = false+ -- and(false, false) = false+ --+ -- and is defined by+ -- and = \x y. x y x+ it "true and true = true" $ do+ "(\\x y. x y x) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"++ it "true and false = false" $ do+ "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"+ + it "false and true = false" $ do+ "(\\x y. x y x) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. f"++ it "false and false = false" $ do+ "(\\x y. x y x) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"++ it "false and p = false" $ do+ "(\\x y. x y x) (\\t f. f) p" `shouldEvalTo` "\\t f. f"++ it "true and p = false" $ do+ "(\\x y. x y x) (\\t f. t) p" `shouldEvalTo` "p"++ describe "or" $ do+ -- or takes two Bools and returns true iff either argument is true+ -- + -- or(true, true) = true+ -- or(true, false) = true+ -- or(false, true) = true+ -- or(false, false) = false+ --+ -- or is defined by+ -- or = \x y. x x y+ it "true or true = true" $ do+ "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"+ + it "true or false = true" $ do+ "(\\x y. x x y) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. t"+ + it "false or true = true" $ do+ "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"++ it "false or false = false" $ do+ "(\\x y. x x y) (\\t f. f) (\\t f. f)" `shouldEvalTo` "\\t f. f"++ it "true or p = true" $ do+ "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"++ it "false or p = p" $ do+ "(\\x y. x x y) (\\t f. f) p" `shouldEvalTo` "p"+ ++ describe "not" $ do+ -- not takes a Bool and returns its opposite value+ --+ -- not(true) = false+ -- not(false) = true+ --+ -- not is defined by+ -- not = \x. x (\t f. f) (\t f. t)+ it "not true = false" $ do+ "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"++ it "not false = true"$ do+ "(\\x. x (\\t f. f) (\\t f. t)) \\t f. f" `shouldEvalTo` "\\t f. t"+ + describe "if" $ do+ -- if takes a Bool and two values. If returns the first value+ -- if the Bool is true, and the second otherwise. In other words,+ -- if p x y = if p then x else y+ --+ -- if(true, x, y) = x+ -- if(false, x, y) = y+ -- + -- if is defined by+ -- if = \p x y. p x y+ it "if true 0 1 = 0" $ do+ "(\\p x y. p x y) (\\t f. t) (\\f x. x) (\\f x. f x)"+ `shouldEvalTo` "\\f x. x"++ it "if false 0 1 = 1" $ do+ "(\\p x y. p x y) (\\t f. f) (\\f x. x) (\\f x. f x)"+ `shouldEvalTo` "\\f x. f x"++ it "it true p q = p" $ do+ "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"++ it "it false p q = q" $ do+ "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
+ test/Language/Lambda/Examples/NatSpec.hs view
@@ -0,0 +1,103 @@+module Language.Lambda.Examples.NatSpec where++import Test.Hspec++import Language.Lambda.HspecUtils++spec :: Spec+spec = do+ describe "Nat" $ do+ -- Nat is the definition of natural numbers. More precisely, Nat+ -- is the set of nonnegative integers. We represent nats using+ -- Church Encodings:+ --+ -- 0: \f x. x+ -- 1: \f x. f x+ -- 2: \f x. f (f x)+ -- ...and so on++ describe "successor" $ do+ -- successor is a function that adds 1+ -- succ(0) = 1+ -- succ(1) = 2+ -- ... and so forth+ --+ -- successor is defined by+ -- succ = \n f x. f (n f x)+ it "succ 0 = 1" $ do+ "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. f x"++ it "succ 1 = 2" $ do+ "(\\n f x. f (n f x)) (\\f x. f x)" `shouldEvalTo` "\\f x. f (f x)"++ describe "add" $ do+ -- add(m, n) = m + n+ --+ -- It is defined by applying successor m times on n:+ -- add = \m n f x. m f (n f x)+ it "add 0 2 = 2" $ do+ "(\\m n f x. m f (n f x)) (\\f x. x) (\\f x. f (f x))"+ `shouldEvalTo` "\\f x. f (f x)"++ it "add 3 2 = 5" $ do+ "(\\m n f x. m f (n f x)) (\\f x. f (f (f x))) (\\f x. f (f x))"+ `shouldEvalTo` "\\f x. f (f (f (f (f x))))"++ -- Here, we use `\f x. n f x` instead of `n`. This is because+ -- I haven't implemented eta conversion+ it "add 0 n = n" $ do+ "(\\m n f x. m f (n f x)) (\\f x. x) n"+ `shouldEvalTo` "\\f x. n f x"++ describe "multiply" $ do+ -- multiply(m, n) = m * n+ --+ -- multiply is defined by applying add m times+ -- multiply = \m n f x. m (n f x) x)+ --+ -- Using eta conversion, we can omit the parameter x+ -- multiply = \m n f. m (n f)+ it "multiply 0 2 = 0" $ do+ "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"+ `shouldEvalTo` "\\f x. x"++ it "multiply 2 3 = 6" $ do+ "(\\m n f. m (n f)) (\\f x. f (f x)) (\\f x. f (f (f x)))"+ `shouldEvalTo` "\\f x. f (f (f (f (f (f x)))))"++ it "multiply 0 n = 0" $ do+ "(\\m n f. m (n f)) (\\f x. x) n"+ `shouldEvalTo` "\\f x. x"++ it "multiply 1 n = n" $ do+ "(\\m n f. m (n f)) (\\f x. f x) n"+ `shouldEvalTo` "\\f x. n f x"++ describe "power" $ do+ -- The function power raises m to the power of n.+ -- power(m, n) = m^n+ --+ -- power is defined by applying multiply n times+ -- power = \m n f x. (n m) f x+ --+ -- Using eta conversion again, we can omit the parameter f+ -- power = \m n = n m++ -- NOTE: Here we use the first form to get more predictable+ -- variable names. Otherwise, alpha conversion will choose a random+ -- unique variable.+ it "power 0 1 = 0" $ do+ "(\\m n f x. (n m) f x) (\\f x. x) (\\f x. f x)"+ `shouldEvalTo` "\\f x. x"++ it "power 2 3 = 8" $ do+ "(\\m n f x. (n m) f x) (\\f x. f (f x)) (\\f x. f (f (f x)))"+ `shouldEvalTo` "\\f x. f (f (f (f (f (f (f (f x)))))))"++ it "power n 0 = 1" $ do+ "(\\m n f x. (n m) f x) n (\\f x. x)"+ `shouldEvalTo` "\\f x. f x"++ it "power n 1 = n" $ do+ "(\\m n f x. (n m) f x) n (\\f x. f x)"+ `shouldEvalTo` "\\f x. n f x"
+ test/Language/Lambda/Examples/PairSpec.hs view
@@ -0,0 +1,39 @@+module Language.Lambda.Examples.PairSpec where++import Language.Lambda.HspecUtils++import Test.Hspec++spec :: Spec+spec = do+ describe "Pair" $ do+ -- Pair is the definition of tuples with two items. Pairs,+ -- again are represented using Church Encodings:+ --+ -- pair = \x y f. f x y+ describe "first" $ do+ -- The function first returns the first item in a pair+ -- first(x, y) = x+ --+ -- first is defined by+ -- first = \p. p (\t f. t)+ it "first 0 1 = 0" $ do+ "(\\p. p (\\t f. t)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"+ `shouldEvalTo` "\\f x. x"++ it "first x y = x" $ do+ "(\\p. p (\\t f. t)) ((\\x y f. f x y) x y)" `shouldEvalTo` "x"++ describe "second" $ do+ -- The function second returns the second item in a pair+ -- second(x, y) = y+ --+ -- second is defined by+ -- second = \p. p (\t f. f)+ it "second 0 1 = 1" $ do+ "(\\p. p (\\t f. f)) ((\\x y f. f x y) (\\f x. x) (\\f x. f x))"+ `shouldEvalTo` "\\f x. f x"++ it "second x y = y" $ do+ "(\\p. p (\\t f. f)) ((\\x y f. f x y) x y)" `shouldEvalTo` "y"+ "(\\p. p (\\x y z. x)) ((\\x y z f. f x y z) x y z)" `shouldEvalTo` "x"
+ test/Language/Lambda/ExpressionSpec.hs view
@@ -0,0 +1,40 @@+module Language.Lambda.ExpressionSpec where++import Test.Hspec++import Language.Lambda.Expression+import Language.Lambda.PrettyPrint++spec :: Spec+spec = do+ describe "prettyPrint" $ do+ it "prints simple variables" $ do+ prettyPrint (Var "x") `shouldBe` "x"++ it "prints simple abstractions" $ do+ prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x"++ it "prints simple applications" $ do+ prettyPrint (App (Var "a") (Var "b"))+ `shouldBe` "a b"++ it "prints nested applications" $ do+ prettyPrint (Abs "f" (Abs "x" (Var"x")))+ `shouldBe` "λf x. x"++ it "prints nested applications" $ do+ prettyPrint (App (App (Var "f") (Var "x")) (Var "y"))+ `shouldBe` "f x y"++ it "prints parenthesized applications" $ do+ prettyPrint (App (Var "f") (App (Var "x") (Var "y")))+ `shouldBe` "f (x y)"++ prettyPrint (App (Abs "x" (Var "x")) (Var "y"))+ `shouldBe` "(λx. x) y"++ prettyPrint (App (Var "x") (Abs "f" (Var "f")))+ `shouldBe` "x (λf. f)"+ + prettyPrint (App (Abs "f" (Var "f")) (Abs "g" (Var "g")))+ `shouldBe` "(λf. f) (λg. g)"
+ test/Language/Lambda/HspecUtils.hs view
@@ -0,0 +1,8 @@+module Language.Lambda.HspecUtils where++import Test.Hspec++import Language.Lambda++shouldEvalTo :: String -> String -> Expectation+shouldEvalTo s1 = shouldBe (evalString s1) . evalString
+ test/Language/Lambda/ParserSpec.hs view
@@ -0,0 +1,54 @@+module Language.Lambda.ParserSpec (spec) where++import Data.Either++import Test.Hspec++import Language.Lambda.Expression+import Language.Lambda.Parser++spec :: Spec+spec = do+ describe "parseExpr" $ do+ it "parses simple variables" $ do+ parseExpr "x" `shouldBe` Right (Var "x")++ it "parses parenthesized variables" $ do+ parseExpr "(x)" `shouldBe` Right (Var "x")++ it "parses simple abstractions" $ do+ parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))++ it "parses nested abstractions" $ do+ parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))++ it "parses simple applications" $ do+ parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))++ it "parses chained applications" $ do+ parseExpr "f x y" `shouldBe` Right (App (App (Var "f") (Var "x")) (Var "y"))++ it "parses complex expressions" $ do+ let exprs = [+ "\\f x. f x",+ "(\\p x y. y) (\\p x y. x)",+ "f (\\x. x)",+ "(\\x . f x) g y",+ "(\\f . (\\ x y. f x y) f x y) w x y"+ ]+ + mapM_ ((flip shouldSatisfy) isRight . parseExpr) exprs++ it "does not parse trailing errors" $ do+ parseExpr "x +" `shouldSatisfy` isLeft+ + it "ignores whitespace" $ do+ let exprs = [+ " x ",+ " \\ x . x ",+ " ( x ) "+ ]+ + mapM_ ((flip shouldSatisfy) isRight . parseExpr) exprs+ +
+ test/Language/Lambda/PrettyPrintSpec.hs view
@@ -0,0 +1,37 @@+module Language.Lambda.PrettyPrintSpec where++import Test.Hspec++import Language.Lambda.PrettyPrint+ +spec :: Spec+spec = do+ describe "PDoc" $ do+ it "pretty prints empty" $ do+ prettyPrint' empty `shouldBe` ""++ it "pretty prints added components" $ do+ let pdoc = add "f" (add "x" empty)+ prettyPrint' pdoc `shouldBe` "fx"++ it "pretty prints appended components" $ do+ let pdoc = append ["f", "x", "y"] empty+ prettyPrint' pdoc `shouldBe` "fxy"++ it "pretty prints between parens" $ do+ let pdoc = between (PDoc ["f"]) "(" ")" empty+ prettyPrint' pdoc `shouldBe` "(f)"++ let pdoc' = betweenParens (PDoc ["f"]) empty+ prettyPrint' pdoc' `shouldBe` "(f)"++ it "pretty prints intercalated spaces" $ do+ let pdoc = intercalate ["f", "x", "y"] [space] empty+ prettyPrint' pdoc `shouldBe` "f x y"++ it "pretty prints lambda" $ do+ let pdoc = between (PDoc ["x"]) "\\" ". " (add "x" empty)+ prettyPrint' pdoc `shouldBe` "\\x. x"++prettyPrint' :: PDoc String -> String+prettyPrint' = prettyPrint
+ test/Language/LambdaSpec.hs view
@@ -0,0 +1,30 @@+module Language.LambdaSpec where++import Test.Hspec++import Language.Lambda++spec :: Spec+spec = do+ describe "evalString" $ do+ it "evaluates simple strings" $ do+ evalString "x" `shouldBe` Right (Var "x")+ evalString "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))+ evalString "f y" `shouldBe` Right (App (Var "f") (Var "y"))++ it "reduces simple applications" $ do+ evalString "(\\x .x) y" `shouldBe` Right (Var "y")++ it "reduces applications with nested redexes" $ do+ evalString "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))++ describe "uniques" $ do+ let alphabet = reverse ['a'..'z']+ len = length alphabet+ + it "starts with plain alphabet" $ do+ take len uniques `shouldBe` map (:[]) alphabet++ it "adds index afterwards" $ do+ take len (drop len uniques) `shouldBe` map (:['0']) alphabet+
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}