packages feed

lambda-calculator 1.0.0 → 1.1.0

raw patch · 24 files changed

+864/−367 lines, 24 filesdep +hlintdep +optparse-applicativedep ~base

Dependencies added: hlint, optparse-applicative

Dependency ranges changed: base

Files

app/Main.hs view
@@ -2,41 +2,105 @@  import Data.Version +import Options.Applicative hiding (ParseError) import System.Console.Shell import System.Console.Shell.ShellMonad import System.Console.Shell.Backend.Readline (readlineBackend) +import qualified Paths_lambda_calculator as P+ import Language.Lambda-import Paths_lambda_calculator+import Language.Lambda.Util.PrettyPrint+import Language.SystemF  main :: IO ()-main = runShell mkShellDesc readlineBackend ()+main = execParser opts >>= runShell'+  where opts = info (helper <*> cliParser)+                    (briefDesc <> progDesc "A Lambda Calculus Interpreter") -mkShellDesc :: ShellDescription ()-mkShellDesc = shellDesc' $ mkShellDescription commands eval+-- Option Parsing+data CliOptions = CliOptions {+  language :: Eval Language,+  version :: Bool+  }++-- Supported Languages:+-- +--  * Untyped Lambda Calculus+--  * System F+data Language +  = Untyped+  | SystemF++-- The result of an evaluation+type Result a = Either a -- An error+                       a -- The result++-- Represent a language together with its evaluation function+data Eval a = Eval a (String -> Result String)++untyped :: Eval Language+untyped = Eval Untyped eval+  where eval = fromEvalString Language.Lambda.evalString++systemf :: Eval Language+systemf = Eval SystemF eval+  where eval = fromEvalString Language.SystemF.evalString++-- Take a typed evaluation function and return a function that returns a result+-- +-- For example:+--   (String -> Either ParseError (LambdaExpr String)) -> (String -> Result String)+--   (String -> Either ParseError (SystemFExpr String String)) -> (String -> Result String)+fromEvalString :: (Show s, PrettyPrint p)+               => (String -> Either s p)+               -> (String -> Result String)+fromEvalString f = either (Left . show) (Right . prettyPrint) . f++cliParser :: Parser CliOptions+cliParser = CliOptions +  <$> flag untyped systemf (long "system-f" <> +                            short 'f' <> +                            internal <>    -- this is a secret feature+                            help "Use the System F interpreter")++  <*> switch (long "version" <> +              short 'v' <> +              help "Print the version")++-- Interactive Shell+runShell' :: CliOptions -> IO ()+runShell' CliOptions{version=True} = putStrLn version'+runShell' CliOptions{language=Eval lang eval} +  = runShell (mkShellDesc lang eval) readlineBackend ()++mkShellDesc :: Language +            -> (String -> Result String)+            -> ShellDescription ()+mkShellDesc language f = shellDesc' $ mkShellDescription commands (eval f)   where shellDesc' d = d {           greetingText = Just shellGreeting,-          prompt = shellPrompt+          prompt = shellPrompt language           }  shellGreeting :: String shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"   -shellPrompt :: s -> IO String-shellPrompt _ = return "λ > "+shellPrompt :: Language -> s -> IO String+shellPrompt language _ = return $ prefix language : " > "+  where prefix Untyped = lambda+        prefix SystemF = upperLambda  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+commands = [+  exitCommand "q",+  helpCommand "h"+  ] -        shellPutStrLn' :: PrettyPrint s => s -> Sh s' ()-        shellPutStrLn' = shellPutStrLn . prettyPrint+eval :: (String -> Result String) -> String -> Sh s' ()+eval f = either shellPutErrLn shellPutStrLn . f +-- Get the current version version' :: String-version' = showVersion version+version' = showVersion P.version
lambda-calculator.cabal view
@@ -1,5 +1,5 @@ name:                lambda-calculator-version:             1.0.0+version:             1.1.0 synopsis:            A lambda calculus interpreter description:         Please see README.md homepage:            https://github.com/sgillespie/lambda-calculus#readme@@ -19,7 +19,12 @@                        Language.Lambda.Expression,                        Language.Lambda.Eval,                        Language.Lambda.Parser,-                       Language.Lambda.PrettyPrint++                       Language.Lambda.Util.PrettyPrint,++                       Language.SystemF,+                       Language.SystemF.Expression,+                       Language.SystemF.Parser   build-depends:       base <= 5,                        parsec   default-language:    Haskell2010@@ -31,6 +36,7 @@   ghc-options:         -threaded -rtsopts -with-rtsopts=-N   build-depends:       base,                        lambda-calculator,+                       optparse-applicative,                        Shellac,                        Shellac-readline   default-language:    Haskell2010@@ -47,11 +53,25 @@                        Language.Lambda.EvalSpec,                        Language.Lambda.HspecUtils,                        Language.Lambda.ParserSpec,-                       Language.Lambda.PrettyPrintSpec++                       Language.Lambda.Util.PrettyPrintSpec,++                       Language.SystemFSpec,+                       Language.SystemF.ExpressionSpec,+                       Language.SystemF.ParserSpec   build-depends:       base <= 5,                        lambda-calculator,                        hspec,                        HUnit+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  default-language:    Haskell2010++test-suite lambda-calculus-lint+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             HLint.hs+  build-depends:       base <= 5,+                       hlint   ghc-options:         -threaded -rtsopts -with-rtsopts=-N   default-language:    Haskell2010
src/Language/Lambda.hs view
@@ -1,5 +1,7 @@+{-# LANGUAGE FlexibleInstances #-} module Language.Lambda (   LambdaExpr(..),+  ParseError(..),   PrettyPrint(..),   evalExpr,   evalString,@@ -13,15 +15,12 @@ import Language.Lambda.Eval import Language.Lambda.Expression import Language.Lambda.Parser-import Language.Lambda.PrettyPrint+import Language.Lambda.Util.PrettyPrint  evalString :: String -> Either ParseError (LambdaExpr String)-evalString = liftM (evalExpr uniques) . parseExpr+evalString = fmap (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)..]+  where suffix = "" : map show [(0::Int)..]
src/Language/Lambda/Expression.hs view
@@ -3,7 +3,7 @@  import Prelude hiding (abs, uncurry) -import Language.Lambda.PrettyPrint+import Language.Lambda.Util.PrettyPrint  data LambdaExpr name   = Var name@@ -46,6 +46,6 @@   = pprExpr pdoc e1 `mappend` addSpace (pprExpr pdoc e2)  uncurry :: n -> LambdaExpr n -> ([n], LambdaExpr n)-uncurry n body = uncurry' [n] body+uncurry n = uncurry' [n]   where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'         uncurry' ns body'          = (reverse ns, body')
src/Language/Lambda/Parser.hs view
@@ -22,7 +22,7 @@  abs :: Parser (LambdaExpr String) abs = curry <$> idents <*> expr-  where idents = (symbol '\\') *> many1 identifier <* (symbol '.')+  where idents = symbol '\\' *> many1 identifier <* symbol '.'         curry = flip (foldr Abs)  app :: Parser (LambdaExpr String)
− src/Language/Lambda/PrettyPrint.hs 
@@ -1,50 +0,0 @@-{-# 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 = 'λ'
+ src/Language/Lambda/Util/PrettyPrint.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.Lambda.Util.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) = concatMap 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 = 'λ'++upperLambda :: Char+upperLambda = 'Λ'
+ src/Language/SystemF.hs view
@@ -0,0 +1,16 @@+module Language.SystemF (+  PrettyPrint(..),+  SystemFExpr(..),+  evalString,+  parseExpr+  ) where++import Text.Parsec++import Language.Lambda.Util.PrettyPrint+import Language.SystemF.Expression+import Language.SystemF.Parser++evalString :: String -> Either ParseError (SystemFExpr String String)+evalString = parseExpr+
+ src/Language/SystemF/Expression.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.SystemF.Expression where++import Data.Monoid++import Language.Lambda.Util.PrettyPrint++data SystemFExpr name ty+  = Var name                                        -- Variable+  | App (SystemFExpr name ty) (SystemFExpr name ty) -- Application+  | Abs name (Ty ty) (SystemFExpr name ty)          -- Abstraction+  | TyAbs ty (SystemFExpr name ty)                  -- Type Abstraction+                                                    -- \X. body++  | TyApp (SystemFExpr name ty) (Ty ty)             -- Type Application+                                                    -- x [X]+  deriving (Eq, Show)++data Ty name+  = TyVar name                  -- Type variable (T)+  | TyArrow (Ty name) (Ty name) -- Type arrow    (T -> U)+  deriving (Eq, Show)++-- Pretty printing+instance (PrettyPrint n, PrettyPrint t) => PrettyPrint (SystemFExpr n t) where+  prettyPrint = prettyPrint . pprExpr empty++instance PrettyPrint n => PrettyPrint (Ty n) where+  prettyPrint = prettyPrint . pprTy empty True++-- Same as prettyPrint, but we assume the same type for names and types. Useful+-- for testing.+prettyPrint' :: PrettyPrint n => SystemFExpr n n -> String+prettyPrint' = prettyPrint++-- Pretty print a system f expression+pprExpr :: (PrettyPrint n, PrettyPrint t) +        => PDoc String +        -> SystemFExpr n t+        -> PDoc String+pprExpr pdoc (Var n)        = prettyPrint n `add` pdoc+pprExpr pdoc (App e1 e2)    = pprApp pdoc e1 e2+pprExpr pdoc (Abs n t body) = pprAbs pdoc n t body+pprExpr pdoc (TyAbs t body) = pprTAbs pdoc t body+pprExpr pdoc (TyApp e ty)   = pprTApp pdoc e ty++-- Pretty print an application+pprApp :: (PrettyPrint n, PrettyPrint t)+       => PDoc String+       -> SystemFExpr n t+       -> SystemFExpr n t+       -> 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)++pprTApp :: (PrettyPrint n, PrettyPrint t)+        => PDoc String+        -> SystemFExpr n t+        -> Ty t+        -> PDoc String+pprTApp pdoc expr ty = expr' `mappend` addSpace (between ty' "[" "]" empty)+  where expr' = pprExpr pdoc expr+        ty' = add (prettyPrint ty) empty++-- Pretty print an abstraction+pprAbs :: (PrettyPrint n, PrettyPrint t)+       => PDoc String+       -> n+       -> Ty t+       -> SystemFExpr n t+       -> PDoc String+pprAbs pdoc name ty body = between vars' lambda' ". " (pprExpr pdoc body')+  where (vars, body') = uncurryAbs name ty body+        vars' = intercalate (map (uncurry pprArg) vars) " " empty+        lambda' = [lambda, space]++        pprArg n t = prettyPrint n ++ (':':pprArg' t)+        pprArg' t@(TyVar _)     = prettyPrint t+        pprArg' t@(TyArrow _ _) = prettyPrint $ betweenParens (pprTy empty False t) empty++-- Pretty print types+pprTy :: PrettyPrint n+      => PDoc String+      -> Bool -- Add a space between arrows?+      -> Ty n+      -> PDoc String+pprTy pdoc space (TyVar n) = prettyPrint n `add` pdoc+pprTy pdoc space (TyArrow a b) = pprTyArrow pdoc space a b++pprTyArrow :: PrettyPrint n+           => PDoc String+           -> Bool -- Add a space between arrows?+           -> Ty n+           -> Ty n+           -> PDoc String+pprTyArrow pdoc space a@(TyVar _) b = pprTyArrow' space (pprTy pdoc space a) +                                                        (pprTy pdoc space b)+pprTyArrow pdoc space (TyArrow a1 a2) b = pprTyArrow' space a' (pprTy pdoc space b)+  where a' = betweenParens (pprTyArrow pdoc space a1 a2) empty++pprTyArrow' :: Bool -- Add a space between arrows?+            -> PDoc String+            -> PDoc String+            -> PDoc String+pprTyArrow' space a b = a <> arrow <> b+  where arrow | space     = " -> " `add` empty+              | otherwise = "->" `add` empty++-- Pretty print a type abstraction+pprTAbs :: (PrettyPrint n, PrettyPrint t)+        => PDoc String+        -> t+        -> SystemFExpr n t+        -> PDoc String+pprTAbs pdoc ty body = between vars' lambda' ". " (pprExpr pdoc body')+  where (vars, body') = uncurryTAbs ty body+        vars' = intercalate (map prettyPrint vars) " " empty+        lambda' = [upperLambda, space]++uncurryAbs :: n -> Ty t -> SystemFExpr n t -> ([(n, Ty t)], SystemFExpr n t)+uncurryAbs name ty = uncurry' [(name, ty)] +  where uncurry' ns (Abs n' t' body') = uncurry' ((n', t'):ns) body'+        uncurry' ns body'             = (reverse ns, body')++uncurryTAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)+uncurryTAbs ty = uncurry' [ty]+  where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'+        uncurry' ts body'            = (reverse ts, body')
+ src/Language/SystemF/Parser.hs view
@@ -0,0 +1,86 @@+module Language.SystemF.Parser (+  parseExpr,+  parseType+  ) where++import Control.Monad+import Prelude hiding (abs)++import Text.Parsec+import Text.Parsec.String++import Language.SystemF.Expression++parseExpr :: String -> Either ParseError (SystemFExpr String String)+parseExpr = parse (whitespace *> expr <* eof) ""++parseType :: String -> Either ParseError (Ty String)+parseType = parse (whitespace *> ty <* eof) ""++-- Parse expressions+expr :: Parser (SystemFExpr String String)+expr = try tyapp <|> try app <|> term++app :: Parser (SystemFExpr String String)+app = chainl1 term (return App)++tyapp :: Parser (SystemFExpr String String)+tyapp = TyApp+      <$> term+      <*> ty'+  where ty' = symbol '[' *> ty <* symbol ']'++term :: Parser (SystemFExpr String String)+term = try abs <|> tyabs <|> var <|> parens expr++var :: Parser (SystemFExpr String String)+var = Var <$> exprId++abs :: Parser (SystemFExpr String String)+abs = curry +    <$> (symbol '\\' *> many1 args <* symbol '.') +    <*> expr+  where args = (,) <$> (exprId <* symbol ':') <*> ty+        curry = flip . foldr . uncurry $ Abs++tyabs :: Parser (SystemFExpr String String)+tyabs = curry <$> args <*> expr+  where args = symbol '\\' *> many1 typeId <* symbol '.'+        curry = flip (foldr TyAbs)++-- Parse type expressions+ty :: Parser (Ty String)+ty = try arrow++arrow :: Parser (Ty String)+arrow = chainr1 tyterm (symbol' "->" *> return TyArrow)++tyterm :: Parser (Ty String)+tyterm = tyvar <|> parens ty++tyvar :: Parser (Ty String)+tyvar = TyVar <$> typeId++parens :: Parser a -> Parser a+parens p = symbol '(' *> p <* symbol ')'++identifier :: Parser Char -> Parser String+identifier firstChar = lexeme ((:) <$> first <*> many rest)+  where first = firstChar <|> char '_'+        rest = first <|> digit++typeId, exprId :: Parser String+typeId = identifier upper+exprId = identifier lower++whitespace :: Parser ()+whitespace = void . many . oneOf $ " \t"++symbol :: Char -> Parser ()+symbol = void . lexeme . char++symbol' :: String -> Parser ()+symbol' = void . lexeme . string++lexeme :: Parser a -> Parser a+lexeme p = p <* whitespace
+ test/HLint.hs view
@@ -0,0 +1,16 @@+module Main (main) where++import Language.Haskell.HLint (hlint)+import System.Exit (exitFailure, exitSuccess)++arguments :: [String]+arguments = [ +  "app",+  "src",+  "test"+  ]++main :: IO ()+main = hlint arguments >>= main'+  where main' [] = exitSuccess+        main' _  = exitFailure
test/Language/Lambda/EvalSpec.hs view
@@ -33,7 +33,7 @@          it "reduces simple applications" $ do       let e1 = Abs "x" (Var "x")-          e2 = (Var "y")+          e2 = Var "y"       betaReduce' e1 e2 `shouldBe` Var "y"      it "reduces nested abstractions" $ do@@ -97,14 +97,14 @@       etaConvert expr `shouldBe` expr    describe "freeVarsOf" $ do-    it "Returns simple vars" $ do+    it "Returns simple vars" $       freeVarsOf (Var "x") `shouldBe` ["x"]   -    it "Does not return bound vars" $ do+    it "Does not return bound vars" $       freeVarsOf (Abs "x" (Var "x")) `shouldBe` [] -    it "Returns nested simple vars" $ do+    it "Returns nested simple vars" $       freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"] -    it "Returns applied simple vars" $ do+    it "Returns applied simple vars" $       freeVarsOf (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]
test/Language/Lambda/Examples/BoolSpec.hs view
@@ -5,105 +5,104 @@ import Language.Lambda.HspecUtils  spec :: Spec-spec = do-  describe "Bool" $ do-    -- Bool is the definition of Booleans. We represent bools-    -- using Church Encodings:+spec = 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     ---    -- 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"+    -- and is defined by+    -- and = \x y. x y x+    it "true and true = true" $+      "(\\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 "true and false = false" $+      "(\\x y. x y x) (\\t f. t) (\\t f. f)" `shouldEvalTo` "\\t f. f"+      +    it "false and true = false" $+      "(\\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 false = false" $+      "(\\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 "false and p = false" $+      "(\\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"+    it "true and p = false" $+      "(\\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"+  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" $+      "(\\x y. x x y) (\\t f. t) (\\t f. t)" `shouldEvalTo` "\\t f. t"+    +    it "true or false = true" $+      "(\\x y. x x y) (\\t f. t) (\\t f. f)" `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 true = true" $+      "(\\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 "false or false = false" $+      "(\\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 "true or p = true" $+      "(\\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"-        +    it "false or p = p" $+      "(\\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"+  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" $+      "(\\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 "not false = true" $+      "(\\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" $+      "(\\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 "if false 0 1 = 1" $+      "(\\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 true p q = p" $+      "(\\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"+    it "it false p q = q" $+      "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"
test/Language/Lambda/Examples/NatSpec.hs view
@@ -5,99 +5,98 @@ 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+spec = 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"+  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" $+      "(\\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)"+    it "succ 1 = 2" $+      "(\\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)"+  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" $+      "(\\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))))"+    it "add 3 2 = 5" $+      "(\\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"+    -- 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" $+      "(\\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"+  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" $+      "(\\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 2 3 = 6" $+      "(\\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 0 n = 0" $+      "(\\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"+    it "multiply 1 n = n" $+      "(\\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+  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"+    -- 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" $+      "(\\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 2 3 = 8" $+      "(\\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 0 = 1" $+      "(\\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"+    it "power n 1 = n" $+      "(\\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
@@ -5,35 +5,34 @@ 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:+spec = 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     ---    -- 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"+    -- first is defined by+    -- first = \p. p (\t f. t)+    it "first 0 1 = 0" $+      "(\\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"+    it "first x y = x" $+      "(\\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"+  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" $+      "(\\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"+    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
@@ -3,26 +3,25 @@ import Test.Hspec  import Language.Lambda.Expression-import Language.Lambda.PrettyPrint+import Language.Lambda.Util.PrettyPrint  spec :: Spec-spec = do-  describe "prettyPrint" $ do-    it "prints simple variables" $ do+spec = describe "prettyPrint" $ do+    it "prints simple variables" $        prettyPrint (Var "x") `shouldBe` "x" -    it "prints simple abstractions" $ do+    it "prints simple abstractions" $       prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x" -    it "prints simple applications" $ do+    it "prints simple applications" $       prettyPrint (App (Var "a") (Var "b"))         `shouldBe` "a b" -    it "prints nested applications" $ do-      prettyPrint (Abs "f" (Abs "x" (Var"x")))+    it "prints nested abstractions" $+      prettyPrint (Abs "f" (Abs "x" (Var "x")))         `shouldBe` "λf x. x" -    it "prints nested applications" $ do+    it "prints nested applications" $       prettyPrint (App (App (Var "f") (Var "x")) (Var "y"))         `shouldBe` "f x y"
test/Language/Lambda/HspecUtils.hs view
@@ -5,4 +5,7 @@ import Language.Lambda  shouldEvalTo :: String -> String -> Expectation-shouldEvalTo s1 = shouldBe (evalString s1) . evalString+shouldEvalTo s1 = shouldBe (eval s1) . eval++eval :: String -> Either ParseError (LambdaExpr String)+eval = evalString
test/Language/Lambda/ParserSpec.hs view
@@ -8,47 +8,46 @@ import Language.Lambda.Parser  spec :: Spec-spec = do-  describe "parseExpr" $ do-    it "parses simple variables" $ do-      parseExpr "x" `shouldBe` Right (Var "x")+spec = describe "parseExpr" $ do+  it "parses simple variables" $+    parseExpr "x" `shouldBe` Right (Var "x") -    it "parses parenthesized variables" $ do-      parseExpr "(x)" `shouldBe` Right (Var "x")+  it "parses parenthesized variables" $+    parseExpr "(x)" `shouldBe` Right (Var "x") -    it "parses simple abstractions" $ do-      parseExpr "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))+  it "parses simple abstractions" $+    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 nested abstractions" $+    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 simple applications" $+    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 chained applications" $+    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 "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+  it "does not parse trailing errors" $+    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 
@@ -1,37 +0,0 @@-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/Lambda/Util/PrettyPrintSpec.hs view
@@ -0,0 +1,36 @@+module Language.Lambda.Util.PrettyPrintSpec where++import Test.Hspec++import Language.Lambda.Util.PrettyPrint+  +spec :: Spec+spec = describe "PDoc" $ do+  it "pretty prints empty" $+    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
@@ -12,19 +12,19 @@       evalString "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))       evalString "f y" `shouldBe` Right (App (Var "f") (Var "y")) -    it "reduces simple applications" $ do+    it "reduces simple applications" $       evalString "(\\x .x) y" `shouldBe` Right (Var "y") -    it "reduces applications with nested redexes" $ do+    it "reduces applications with nested redexes" $       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+    it "starts with plain alphabet" $       take len uniques `shouldBe` map (:[]) alphabet -    it "adds index afterwards" $ do+    it "adds index afterwards" $       take len (drop len uniques) `shouldBe` map (:['0']) alphabet
+ test/Language/SystemF/ExpressionSpec.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.SystemF.ExpressionSpec where++import Test.Hspec++import Language.Lambda.Util.PrettyPrint+import Language.SystemF.Expression++spec :: Spec+spec = describe "prettyPrint" $ do+  it "prints simple variables" $+    prettyPrint' (Var "x") `shouldBe` "x"++  it "prints simple applications" $+    prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"++  it "prints simple abstractions" $ +    prettyPrint (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"++  it "prints simple type abstractions" $+    prettyPrint (TyAbs (TyVar "X") (Var "x")) `shouldBe` "Λ X. x"++  it "prints simple type applications" $ +    prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"++  it "prints nested abstractions" $+    prettyPrint (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))+      `shouldBe` "λ f:F x:X. x"++  it "prints abstractions with composite types" $ do+    prettyPrint (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))+      `shouldBe ` "λ f:(X->Y). f"++    prettyPrint (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))+      `shouldBe ` "λ f:(X->Y->Z). f"++  it "prints nested type abstractions" $+    prettyPrint (TyAbs (TyVar "A") (TyAbs (TyVar "B") (Var "x")))+      `shouldBe` "Λ A B. x"++  it "prints nested applications" $+    prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))+      `shouldBe` "f x y"++  it "prints parenthesized applications" $ do+    prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))+      `shouldBe` "w (x y)"++    prettyPrint (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))+      `shouldBe` "(λ t:T. t) x"++    prettyPrint (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))+      `shouldBe` "(λ f:F. f) (λ g:G. g)"++  it "prints simple types" $+    prettyPrint (TyVar "X") `shouldBe` "X"++  it "print simple arrow types" $+    prettyPrint (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"++  it "prints chained arrow types" $+    prettyPrint (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))+      `shouldBe` "X -> Y -> Z"++  it "prints nested arrow types" $+    prettyPrint (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))+      `shouldBe` "(T -> U) -> V"
+ test/Language/SystemF/ParserSpec.hs view
@@ -0,0 +1,84 @@+module Language.SystemF.ParserSpec (spec) where++import Data.Either++import Test.Hspec++import Language.SystemF.Expression+import Language.SystemF.Parser++spec :: Spec+spec = do+  describe "parseExpr" $ do+    it "parses simple variables" $+      parseExpr "x" `shouldBe` Right (Var "x")++    it "parses parenthesized variables" $+      parseExpr "(x)" `shouldBe` Right (Var "x")++    it "parses simple abstractions" $+      parseExpr "\\x:T. x" `shouldBe` Right (Abs "x" (TyVar "T") (Var "x"))++    it "parses simple type abstractions" $+      parseExpr "\\X. x" `shouldBe` Right (TyAbs "X" (Var "x"))++    it "parses simple type applications" $ +      parseExpr "x [T]" `shouldBe` Right (TyApp (Var "x") (TyVar "T"))++    it "parses nested abstractions" $+      parseExpr "\\a:A b:B. b" +        `shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))++    it "parses abstractions with arrow types" $+      parseExpr "\\f:(T->U). f"+        `shouldBe` Right (Abs "f" (TyArrow (TyVar "T") (TyVar "U")) (Var "f"))++    it "parses simple applications" $+      parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))++    it "parses chained applications" $+      parseExpr "a b c" `shouldBe` Right (App (App (Var "a") (Var "b")) (Var "c"))++    it "parses complex expressions"  $ do+      let exprs = [+            "\\f:(A->B) x:B. f x",+            "(\\p:(X->Y->Z) x:X y:Y. y) (\\p:(A->B->C) x:B y:C. x)",+            "f (\\x:T. x)",+            "(\\ x:X . f x) g y",+            "(\\f:(X->Y) . (\\ x:X y:Y. f x y) f x y) w x y",+            "(\\x:T. x) [U]"+            ]++      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs++    it "does not parse trailing errors" $+      parseExpr "x +" `shouldSatisfy` isLeft++    it "ignores whitespace" $ do+      let exprs = [+            " x ",+            " \\ x : X. x ",+            " ( x ) "+            ]++      mapM_ (flip shouldSatisfy isRight . parseExpr) exprs+  +  describe "parseType" $ do+    it "parses simple variables" $+      parseType "X" `shouldBe` Right (TyVar "X")++    it "parses parenthesized variables" $+      parseType "(T)" `shouldBe` Right (TyVar "T")++    it "parses simple arrow types" $+      parseType "A -> B" `shouldBe` Right (TyArrow (TyVar "A") (TyVar "B")) ++    it "parses parenthesized arrow types" $+      parseType "((X)->(Y))" `shouldBe` Right (TyArrow (TyVar "X") (TyVar "Y"))++    it "parses nested arrow types" $ do+      parseType "T -> U -> V" +        `shouldBe` Right (TyArrow (TyVar "T") (TyArrow (TyVar "U") (TyVar "V")))++      parseType "(W -> V) -> U"+        `shouldBe` Right (TyArrow (TyArrow (TyVar "W") (TyVar "V")) (TyVar "U"))
+ test/Language/SystemFSpec.hs view
@@ -0,0 +1,9 @@+module Language.SystemFSpec where++import Test.Hspec++import Language.SystemF++spec :: Spec+spec = describe "evalString" $ +  return ()