packages feed

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 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 #-}