lambda-calculator 2.0.0 → 3.0.0

raw patch · 55 files changed

+2254/−1564 lines, 55 filesdep +bytestringdep +mtldep +prettyprinterdep −Shellacdep −Shellac-readlinedep ~basedep ~optparse-applicativePVP ok

version bump matches the API change (PVP)

Dependencies added: bytestring, mtl, prettyprinter, repline, rio, text

Dependencies removed: Shellac, Shellac-readline

Dependency ranges changed: base, optparse-applicative

API changes (from Hackage documentation)

Files

• app/CliOptions.hs +41/−0
• app/Main.hs +15/−100
• app/Repl.hs +11/−0
• app/Repl/Shared.hs +59/−0
• app/Repl/SystemF.hs +40/−0
• app/Repl/Untyped.hs +50/−0
• lambda-calculator.cabal +261/−76
• scripts/HLint.hs +16/−0
• src/Language/Lambda.hs +3/−24
• src/Language/Lambda/Eval.hs +0/−56
• src/Language/Lambda/Expression.hs +0/−51
• src/Language/Lambda/Parser.hs +0/−46
• src/Language/Lambda/Shared/Errors.hs +61/−0
• src/Language/Lambda/Shared/UniqueSupply.hs +9/−0
• src/Language/Lambda/SystemF.hs +26/−0
• src/Language/Lambda/SystemF/Expression.hs +124/−0
• src/Language/Lambda/SystemF/Parser.hs +88/−0
• src/Language/Lambda/SystemF/State.hs +89/−0
• src/Language/Lambda/SystemF/TypeCheck.hs +122/−0
• src/Language/Lambda/Untyped.hs +52/−0
• src/Language/Lambda/Untyped/Eval.hs +121/−0
• src/Language/Lambda/Untyped/Expression.hs +57/−0
• src/Language/Lambda/Untyped/Parser.hs +57/−0
• src/Language/Lambda/Untyped/State.hs +88/−0
• src/Language/Lambda/Util/PrettyPrint.hs +0/−53
• src/Language/SystemF.hs +0/−16
• src/Language/SystemF/Expression.hs +0/−145
• src/Language/SystemF/Parser.hs +0/−86
• src/Language/SystemF/TypeCheck.hs +0/−119
• test/HLint.hs +0/−16
• test/Language/Lambda/EvalSpec.hs +0/−110
• test/Language/Lambda/Examples/BoolSpec.hs +0/−108
• test/Language/Lambda/Examples/NatSpec.hs +0/−102
• test/Language/Lambda/Examples/PairSpec.hs +0/−38
• test/Language/Lambda/ExpressionSpec.hs +0/−39
• test/Language/Lambda/HspecUtils.hs +0/−11
• test/Language/Lambda/ParserSpec.hs +0/−53
• test/Language/Lambda/SystemF/ExpressionSpec.hs +87/−0
• test/Language/Lambda/SystemF/ParserSpec.hs +86/−0
• test/Language/Lambda/SystemF/TypeCheckSpec.hs +71/−0
• test/Language/Lambda/SystemFSpec.hs +9/−0
• test/Language/Lambda/Untyped/EvalSpec.hs +160/−0
• test/Language/Lambda/Untyped/Examples/BoolSpec.hs +110/−0
• test/Language/Lambda/Untyped/Examples/NatSpec.hs +104/−0
• test/Language/Lambda/Untyped/Examples/PairSpec.hs +40/−0
• test/Language/Lambda/Untyped/ExpressionSpec.hs +50/−0
• test/Language/Lambda/Untyped/HspecUtils.hs +14/−0
• test/Language/Lambda/Untyped/ParserSpec.hs +56/−0
• test/Language/Lambda/UntypedSpec.hs +77/−0
• test/Language/Lambda/Util/PrettyPrintSpec.hs +0/−36
• test/Language/LambdaSpec.hs +0/−30
• test/Language/SystemF/ExpressionSpec.hs +0/−81
• test/Language/SystemF/ParserSpec.hs +0/−84
• test/Language/SystemF/TypeCheckSpec.hs +0/−75
• test/Language/SystemFSpec.hs +0/−9

@@ -0,0 +1,41 @@+module CliOptions+  ( CliOptions(..),+    Language(..),+    parseCliOptions+  ) where++import RIO++import Options.Applicative hiding (command, ParseError())++data CliOptions = CliOptions {+  language :: Language,+  version :: Bool+}++-- | Supported Languages:+-- +--    * Untyped Lambda Calculus+--    * System F+data Language +  = Untyped+  | SystemF++parseCliOptions :: IO CliOptions+parseCliOptions = execParser opts+  where opts = info+          (helper <*> cliParser)+          (briefDesc <> progDesc "A Lambda Calculus Interpreter")++cliParser :: Parser CliOptions+cliParser = CliOptions +  <$> flag Untyped SystemF language+  <*> switch version+  where language = long "system-f"+          <> short 'f'+          <> internal -- this is a secret feature+          <> help "Use the System F interpreter"++        version = long "version"+          <> short 'v'+          <> help "Print the version"

@@ -1,107 +1,22 @@ module Main where -import Data.Version--import Data.Semigroup-import Options.Applicative hiding (ParseError)-import System.Console.Shell-import System.Console.Shell.ShellMonad-import System.Console.Shell.Backend.Readline (readlineBackend)-+import CliOptions (CliOptions(..), parseCliOptions)+import Repl (runRepl) import qualified Paths_lambda_calculator as P -import Language.Lambda-import Language.Lambda.Util.PrettyPrint-import Language.SystemF+import Data.Version+import RIO  main :: IO ()-main = execParser opts >>= runShell'-  where opts = info (helper <*> cliParser)-                    (briefDesc <> progDesc "A Lambda Calculus Interpreter")---- 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 language-          }--shellGreeting :: String-shellGreeting = "Lambda Calculator (" ++ version' ++ ")\nType :h for help\n"-  -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 -> Result String) -> String -> Sh s' ()-eval f = either shellPutErrLn shellPutStrLn . f+main = runSimpleApp $ do+  CliOptions{..} <- liftIO parseCliOptions --- Get the current version-version' :: String-version' = showVersion P.version- +  if version+    then+      logInfo $ "Lambda Calculator (" <> version' <> ")"+    else+      liftIO $ runRepl language+    +-- | Get the current version+version' :: Utf8Builder+version' = fromString $ showVersion P.version

@@ -0,0 +1,11 @@+module Repl (runRepl) where++import CliOptions (Language(..))+import Repl.SystemF (runSystemFRepl)+import Repl.Untyped (runUntypedRepl)++import RIO++runRepl :: Language -> IO ()+runRepl SystemF = runSystemFRepl+runRepl Untyped = runUntypedRepl

@@ -0,0 +1,59 @@+module Repl.Shared where++import CliOptions (Language(..))+import Paths_lambda_calculator (version)+import Language.Lambda.Shared.Errors (LambdaException())+import Language.Lambda.Shared.UniqueSupply (defaultUniques)+import Language.Lambda.SystemF++import Data.Text (singleton)+import Data.Text.IO (putStrLn)+import Data.Version (showVersion)+import RIO+import RIO.State+import RIO.Text (pack, unpack)+import System.Console.Repline+import Control.Monad.Except+import qualified Data.Map as M++mkReplOpts banner command = ReplOpts+  { banner = banner,+    command = command,+    options = commands,+    prefix = Just ':',+    multilineCommand = Nothing,+    tabComplete = Custom completer,+    initialiser = initializer,+    finaliser = return Exit+  }++prompt :: Applicative ap => Text -> HaskelineT ap Text+prompt prefix = pure $ prefix <> " > "++commands :: (MonadIO m, MonadThrow m) => [(String, String -> HaskelineT m ())]+commands+  = [ ("h", help'),+      ("help", help'),+      ("q", quit'),+      ("quit", quit')+    ]+  where help' = const helpCommand+        quit' = const abort++completer :: Monad m => CompletionFunc m+completer (left, _) = pure (left, []) -- No tab completion++initializer :: MonadIO io => HaskelineT io ()+initializer = liftIO $ putStrLn greeting+  where greeting = "Lambda Calculator ("+          <> version'+          <> ")\nType :h for help\n"++helpCommand :: MonadIO io => HaskelineT io ()+helpCommand = liftIO $ putStrLn banner+  where banner = " Commands available: \n\n"+          <> "    :help, :h\tShow this help\n"+          <> "    :quit, :q\tQuit\n"++version' :: Text+version' = fromString $ showVersion version

@@ -0,0 +1,40 @@+module Repl.SystemF (runSystemFRepl) where++import Language.Lambda.Shared.Errors (LambdaException())+import Language.Lambda.Shared.UniqueSupply (defaultUniques)+import Language.Lambda.SystemF+import Repl.Shared++import Data.Text (singleton)+import Data.Text.IO (putStrLn)+import RIO+import RIO.State+import RIO.Text (pack, unpack)+import System.Console.Repline+import Control.Monad.Except (ExceptT(..), runExceptT)++type EvalT name m+  = StateT (TypecheckState name)+      (ExceptT LambdaException m)++type Repl a = HaskelineT (EvalT Text IO) a++runSystemFRepl :: IO ()+runSystemFRepl+  = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState+  where replOpts = mkReplOpts banner' $ evalSystemF . pack+        initialState = mkTypecheckState defaultUniques++banner' :: MultiLine -> Repl String+banner' _ = unpack <$> prompt (singleton upperLambda)++evalSystemF :: Text -> Repl ()+evalSystemF input = do+  state' <- get++  let res = runTypecheck (evalText input) state'+  case res of+    Left err -> liftIO . putStrLn . pack . show $ err+    Right (res', newState) -> do+      put newState+      liftIO . putStrLn . prettyPrint $ res'

@@ -0,0 +1,50 @@+module Repl.Untyped (runUntypedRepl) where++import Language.Lambda.Shared.Errors (LambdaException())+import Language.Lambda.Shared.UniqueSupply (defaultUniques)+import Language.Lambda.Untyped+import Repl.Shared++import Data.Text (singleton)+import Data.Text.IO (putStrLn)+import RIO+import RIO.State+import RIO.Text (pack, unpack)+import System.Console.Repline+import Control.Monad.Except++type EvalT name m+  = StateT (EvalState name)+      (ExceptT LambdaException m)++type Repl a = HaskelineT (EvalT Text IO) a++runUntypedRepl :: IO ()+runUntypedRepl+  = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState+  where replOpts = ReplOpts+          { banner = const $ unpack <$> prompt',+            command = evalLambda . pack,+            options = commands,+            prefix = Just ':',+            multilineCommand = Nothing,+            tabComplete = Custom completer,+            initialiser = initializer,+            finaliser = return Exit+          }++        initialState = mkEvalState defaultUniques++prompt' :: Repl Text+prompt' = prompt $ singleton lambda++evalLambda :: Text -> Repl ()+evalLambda input = do+  state' <- get+  +  let res = runEval (evalText input) state'+  case res of+    Left err -> liftIO . putStrLn . textDisplay $ err+    Right (res', newState) -> do+      put newState+      liftIO . putStrLn . prettyPrint $ res'

@@ -1,84 +1,269 @@-name:                lambda-calculator-version:             2.0.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.Util.PrettyPrint,+cabal-version: 1.12 -                       Language.SystemF,-                       Language.SystemF.Expression,-                       Language.SystemF.Parser,-                       Language.SystemF.TypeCheck-  build-depends:       base >= 4.9 && < 5,-                       containers,-                       parsec-  default-language:    Haskell2010+-- This file has been generated from package.yaml by hpack version 0.34.7.+--+-- see: https://github.com/sol/hpack+--+-- hash: 089fe9b55bbab6cbfceb1623b5f1eb4f8c706b39fa51ad2d87957cefea80301c -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 >= 4.9,-                       lambda-calculator,-                       optparse-applicative >= 0.13,-                       Shellac,-                       Shellac-readline-  default-language:    Haskell2010+name:           lambda-calculator+version:        3.0.0+synopsis:       A lambda calculus interpreter+description:    Please see README.md+category:       LambdaCalculus,Language,Teaching+homepage:       https://github.com/sgillespie/lambda-calculus#readme+bug-reports:    https://github.com/sgillespie/lambda-calculus/issues+author:         Sean D Gillespie+maintainer:     sean@mistersg.net+copyright:      2016 Sean Gillespie+license:        MIT+license-file:   LICENSE+build-type:     Simple -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,+source-repository head+  type: git+  location: https://github.com/sgillespie/lambda-calculus -                       Language.Lambda.Util.PrettyPrintSpec,+library+  exposed-modules:+      Language.Lambda.Shared.Errors+      Language.Lambda.Shared.UniqueSupply+      Language.Lambda.Untyped+      Language.Lambda.Untyped.Expression+      Language.Lambda.Untyped.Eval+      Language.Lambda.Untyped.Parser+      Language.Lambda.Untyped.State+      Language.Lambda.SystemF+      Language.Lambda.SystemF.Expression+      Language.Lambda.SystemF.Parser+      Language.Lambda.SystemF.State+      Language.Lambda.SystemF.TypeCheck+  other-modules:+      Language.Lambda+      Paths_lambda_calculator+  hs-source-dirs:+      src+  default-extensions:+      BangPatterns+      ConstraintKinds+      DataKinds+      DefaultSignatures+      DeriveDataTypeable+      DeriveFoldable+      DeriveFunctor+      DeriveGeneric+      DeriveTraversable+      DoAndIfThenElse+      EmptyDataDecls+      ExistentialQuantification+      FlexibleContexts+      FlexibleInstances+      FunctionalDependencies+      GADTs+      GeneralizedNewtypeDeriving+      InstanceSigs+      KindSignatures+      LambdaCase+      MultiParamTypeClasses+      MultiWayIf+      NamedFieldPuns+      PartialTypeSignatures+      PatternGuards+      PolyKinds+      RankNTypes+      RecordWildCards+      ScopedTypeVariables+      StandaloneDeriving+      TupleSections+      TypeFamilies+      TypeSynonymInstances+      ViewPatterns+      NoImplicitPrelude+      OverloadedStrings+  ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints+  build-depends:+      base >=4.9 && <5+    , containers+    , mtl+    , parsec+    , prettyprinter+    , rio+  default-language: Haskell2010 -                       Language.SystemFSpec,-                       Language.SystemF.ExpressionSpec,-                       Language.SystemF.ParserSpec,-                       Language.SystemF.TypeCheckSpec-  build-depends:       base < 5,-                       lambda-calculator,-                       containers,-                       hspec,-                       HUnit-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N-  default-language:    Haskell2010+executable lambda-calculator+  main-is: Main.hs+  other-modules:+      CliOptions+      Repl+      Repl.Shared+      Repl.SystemF+      Repl.Untyped+      Paths_lambda_calculator+  hs-source-dirs:+      app+  default-extensions:+      BangPatterns+      ConstraintKinds+      DataKinds+      DefaultSignatures+      DeriveDataTypeable+      DeriveFoldable+      DeriveFunctor+      DeriveGeneric+      DeriveTraversable+      DoAndIfThenElse+      EmptyDataDecls+      ExistentialQuantification+      FlexibleContexts+      FlexibleInstances+      FunctionalDependencies+      GADTs+      GeneralizedNewtypeDeriving+      InstanceSigs+      KindSignatures+      LambdaCase+      MultiParamTypeClasses+      MultiWayIf+      NamedFieldPuns+      PartialTypeSignatures+      PatternGuards+      PolyKinds+      RankNTypes+      RecordWildCards+      ScopedTypeVariables+      StandaloneDeriving+      TupleSections+      TypeFamilies+      TypeSynonymInstances+      ViewPatterns+      NoImplicitPrelude+      OverloadedStrings+  ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.9 && <5+    , bytestring+    , containers+    , lambda-calculator+    , mtl+    , optparse-applicative+    , prettyprinter+    , repline+    , rio+    , text+  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+  type: exitcode-stdio-1.0+  main-is: HLint.hs+  hs-source-dirs:+      scripts+  default-extensions:+      BangPatterns+      ConstraintKinds+      DataKinds+      DefaultSignatures+      DeriveDataTypeable+      DeriveFoldable+      DeriveFunctor+      DeriveGeneric+      DeriveTraversable+      DoAndIfThenElse+      EmptyDataDecls+      ExistentialQuantification+      FlexibleContexts+      FlexibleInstances+      FunctionalDependencies+      GADTs+      GeneralizedNewtypeDeriving+      InstanceSigs+      KindSignatures+      LambdaCase+      MultiParamTypeClasses+      MultiWayIf+      NamedFieldPuns+      PartialTypeSignatures+      PatternGuards+      PolyKinds+      RankNTypes+      RecordWildCards+      ScopedTypeVariables+      StandaloneDeriving+      TupleSections+      TypeFamilies+      TypeSynonymInstances+      ViewPatterns+      ImplicitPrelude+  ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.9 && <5+    , hlint+    , mtl+    , prettyprinter+    , rio+  default-language: Haskell2010 -source-repository head-  type:     git-  location: https://github.com/sgillespie/lambda-calculus+test-suite lambda-calculus-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Language.Lambda.SystemF.ExpressionSpec+      Language.Lambda.SystemF.ParserSpec+      Language.Lambda.SystemF.TypeCheckSpec+      Language.Lambda.SystemFSpec+      Language.Lambda.Untyped.EvalSpec+      Language.Lambda.Untyped.Examples.BoolSpec+      Language.Lambda.Untyped.Examples.NatSpec+      Language.Lambda.Untyped.Examples.PairSpec+      Language.Lambda.Untyped.ExpressionSpec+      Language.Lambda.Untyped.HspecUtils+      Language.Lambda.Untyped.ParserSpec+      Language.Lambda.UntypedSpec+      Paths_lambda_calculator+  hs-source-dirs:+      test+  default-extensions:+      BangPatterns+      ConstraintKinds+      DataKinds+      DefaultSignatures+      DeriveDataTypeable+      DeriveFoldable+      DeriveFunctor+      DeriveGeneric+      DeriveTraversable+      DoAndIfThenElse+      EmptyDataDecls+      ExistentialQuantification+      FlexibleContexts+      FlexibleInstances+      FunctionalDependencies+      GADTs+      GeneralizedNewtypeDeriving+      InstanceSigs+      KindSignatures+      LambdaCase+      MultiParamTypeClasses+      MultiWayIf+      NamedFieldPuns+      PartialTypeSignatures+      PatternGuards+      PolyKinds+      RankNTypes+      RecordWildCards+      ScopedTypeVariables+      StandaloneDeriving+      TupleSections+      TypeFamilies+      TypeSynonymInstances+      ViewPatterns+  ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      HUnit+    , base >=4.9 && <5+    , containers+    , hspec+    , lambda-calculator+    , mtl+    , prettyprinter+    , rio+  default-language: Haskell2010

@@ -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

@@ -1,26 +1,5 @@-{-# LANGUAGE FlexibleInstances #-}-module Language.Lambda (-  LambdaExpr(..),-  ParseError(..),-  PrettyPrint(..),-  evalExpr,-  evalString,-  parseExpr,-  uniques,+module Language.Lambda+  ( module Language.Lambda.Shared.Errors   ) where -import Control.Monad-import Text.Parsec--import Language.Lambda.Eval-import Language.Lambda.Expression-import Language.Lambda.Parser-import Language.Lambda.Util.PrettyPrint--evalString :: String -> Either ParseError (LambdaExpr String)-evalString = fmap (evalExpr uniques) . parseExpr--uniques :: [String]-uniques = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix-  where suffix = "" : map show [(0::Int)..]-+import Language.Lambda.Shared.Errors

@@ -1,56 +0,0 @@-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--etaConvert :: Eq n => LambdaExpr n -> LambdaExpr n-etaConvert (Abs n (App e1 (Var n')))-  | n == n'   = etaConvert e1-  | otherwise = Abs n (App (etaConvert e1) (Var n'))-etaConvert (Abs n e@(Abs _ _)) -  -- If `etaConvert e == e` then etaConverting it will create an infinite loop-  | e == e'   = Abs n e'-  | otherwise = etaConvert (Abs n e')-  where e' = etaConvert e-etaConvert (Abs n expr) = Abs n (etaConvert expr)-etaConvert (App e1 e2)  = App (etaConvert e1) (etaConvert e2)-etaConvert expr@(Var _) = expr--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]

@@ -1,51 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-module Language.Lambda.Expression where--import Prelude hiding (abs, uncurry)--import Language.Lambda.Util.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 = uncurry' [n]-  where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'-        uncurry' ns body'          = (reverse ns, body')

@@ -1,46 +0,0 @@-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

@@ -0,0 +1,61 @@+module Language.Lambda.Shared.Errors+  ( LambdaException(..),+    isLambdaException,+    isLetError,+    isParseError,+    isImpossibleError+  ) where++import RIO++data LambdaException+  -- | An expression that cannot be parsed+  -- Examples:+  --+  --     \x y+  --     = y+  = ParseError Text++  -- | A let binding nested in another expression+  -- Examples:+  --+  --     \x. let y = z+  --     x (let y = z)+  | InvalidLet Text -- ^ A let binding nested in another expression++  -- | The expected type does not match the actual type+  -- Examples:+  --+  --     (\x: X. x) (y:Y)+  | TyMismatchError Text++  -- | A catch-all error that indicates a bug in this project+  | ImpossibleError+  deriving (Eq, Typeable)++instance Exception LambdaException++instance Display LambdaException where+  textDisplay (ParseError txt) = "Parse error " <> txt+  textDisplay (InvalidLet txt) = "Illegal nested let: " <> txt+  textDisplay ImpossibleError = "An impossible error occurred! Please file a bug."++instance Show LambdaException where+  show = show . textDisplay++-- | Returns true if the passed in value is a LamdbaExpression. Can be used, for example,+-- as a `shouldThrow` matcher+isLambdaException :: LambdaException -> Bool+isLambdaException _ = True++isLetError :: LambdaException -> Bool+isLetError (InvalidLet _) = True+isLetError _ = False++isParseError :: LambdaException -> Bool+isParseError (ParseError _) = True+isParseError _ = False++isImpossibleError :: LambdaException -> Bool+isImpossibleError ImpossibleError = True+isImpossibleError _ = False

@@ -0,0 +1,9 @@+module Language.Lambda.Shared.UniqueSupply where++import RIO+import RIO.Text (pack)++defaultUniques :: [Text]+defaultUniques = map pack strings+  where strings = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix+        suffix = "" : map show [(0::Int)..]

@@ -0,0 +1,26 @@+module Language.Lambda.SystemF (+  Globals(),+  evalText,++  module Language.Lambda.SystemF.Expression,+  module Language.Lambda.SystemF.Parser,+  module Language.Lambda.SystemF.State+  ) where++import Control.Monad.Except+import RIO+import qualified RIO.Text as Text+import qualified Data.Map as Map++import Language.Lambda.Shared.Errors+import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.Parser+import Language.Lambda.SystemF.State++type Globals = Map.Map String (SystemFExpr String String)++evalText :: Text -> Typecheck Text (SystemFExpr Text Text)+evalText text = case parseExpr text of+  Left err -> throwError $ ParseError $ Text.pack $ show err+  Right res -> return res+

@@ -0,0 +1,124 @@+module Language.Lambda.SystemF.Expression+  ( SystemFExpr(..),+    Ty(..),+    prettyPrint,+    upperLambda+  ) where++import Data.Monoid+import Prettyprinter+import Prettyprinter.Render.Text (renderStrict)+import RIO++data SystemFExpr name ty+  -- | Variable: `x`+  = Var name+  -- | Function application: `x y`+  | App (SystemFExpr name ty) (SystemFExpr name ty)+  -- | Lambda abstraction: `\x: X. x`+  | Abs name (Ty ty) (SystemFExpr name ty)+  -- | Type Abstraction: `\X. body`+  | TyAbs ty (SystemFExpr name ty)                  +  -- | Type Application: `x [X]`+  | TyApp (SystemFExpr name ty) (Ty ty)+  deriving (Eq, Show)++data Ty name+  = TyVar name                  -- ^ Type variable (T)+  | TyArrow (Ty name) (Ty name) -- ^ Type arrow    (T -> U)+  | TyForAll name (Ty name)     -- ^ Universal type (forall T. X)+  deriving (Eq, Show)++instance (Pretty name, Pretty ty) => Pretty (SystemFExpr name ty) where+  pretty (Var name) = pretty name+  pretty (App e1 e2) = prettyApp e1 e2+  pretty (Abs name ty body) = prettyAbs name ty body+  pretty (TyAbs ty body) = prettyTyAbs ty body+  pretty (TyApp expr ty) = prettyTyApp expr ty++instance Pretty name => Pretty (Ty name) where+  pretty = prettyTy False++prettyPrint :: Pretty pretty => pretty -> Text+prettyPrint expr = renderStrict docStream+  where docStream = layoutPretty defaultLayoutOptions (pretty expr)++upperLambda :: Char+upperLambda = 'Λ'++prettyApp+  :: (Pretty name, Pretty ty)+  => SystemFExpr name ty+  -> SystemFExpr name ty+  -> Doc a+prettyApp e1@Abs{} e2@Abs{} = parens (pretty e1) <+> parens (pretty e2)+prettyApp e1@Abs{} e2 = parens (pretty e1) <+> pretty e2+prettyApp e1 e2@Abs{} = pretty e1 <+> parens (pretty e2)+prettyApp e1 e2@App{} = pretty e1 <+> parens (pretty e2)+prettyApp e1 e2 = pretty e1 <+> pretty e2++prettyAbs+  :: (Pretty name, Pretty ty)+  => name+  -> Ty ty+  -> SystemFExpr name ty+  -> Doc ann+prettyAbs name ty body+  = lambda+    <+> hsep (map (uncurry prettyArg) names)+    <> dot+    <+> pretty body'+  where (names, body') = uncurryAbs name ty body++prettyTyAbs :: (Pretty name, Pretty ty) => ty -> SystemFExpr name ty -> Doc ann+prettyTyAbs name body = upperLambda' <+> hsep (map pretty names) <> dot+    <+> pretty body'+  where (names, body') = uncurryTyAbs name body+prettyTyApp :: (Pretty name, Pretty ty) => SystemFExpr name ty -> Ty ty -> Doc ann+prettyTyApp expr ty = pretty expr <+> brackets (pretty ty)++prettyTy :: Pretty name => Bool -> Ty name -> Doc ann+prettyTy _ (TyVar name) = pretty name+prettyTy compact (TyArrow t1 t2) = prettyTyArrow compact t1 t2+prettyTy compact (TyForAll name ty) = prettyTyForAll compact name ty++prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann+prettyTyArrow compact (TyArrow t1 t2) t3+  = prettyTyArrow' compact compositeTy $ prettyTy compact t3+  where compositeTy = parens $ prettyTyArrow compact t1 t2++prettyTyArrow compact t1 t2+  = prettyTyArrow' compact (prettyTy compact t1) (prettyTy compact t2)++prettyTyForAll :: Pretty name => Bool -> name -> Ty name -> Doc ann+prettyTyForAll compact name ty+  = "forall"+  <+> pretty name <> dot+  <+> prettyTy compact ty++lambda :: Doc ann+lambda = pretty 'λ'++prettyArg :: (Pretty name, Pretty ty) => name -> Ty ty -> Doc ann+prettyArg name (TyArrow t1 t2)+  = pretty name <> colon <> parens (prettyTyArrow True t1 t2)+prettyArg name ty = pretty name <> colon <> pretty ty++upperLambda' :: Doc ann+upperLambda' = pretty upperLambda++prettyTyArrow' :: Bool -> Doc ann -> Doc ann -> Doc ann+prettyTyArrow' compact doc1 doc2 = doc1 `add'` "->" `add'` doc2+  where add'+          | compact = (<>) +          | otherwise = (<+>)++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')++uncurryTyAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)+uncurryTyAbs ty = uncurry' [ty]+  where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'+        uncurry' ts body'            = (reverse ts, body')

@@ -0,0 +1,88 @@+module Language.Lambda.SystemF.Parser (+  parseExpr,+  parseType+  ) where++import Control.Monad+import Data.Functor+import RIO hiding ((<|>), abs, many, try)+import qualified RIO.Text as Text++import Text.Parsec+import Text.Parsec.Text++import Language.Lambda.SystemF.Expression++parseExpr :: Text -> Either ParseError (SystemFExpr Text Text)+parseExpr = parse (whitespace *> expr <* eof) ""++parseType :: Text -> Either ParseError (Ty Text)+parseType = parse (whitespace *> ty <* eof) ""++-- Parse expressions+expr :: Parser (SystemFExpr Text Text)+expr = try tyapp <|> try app <|> term++app :: Parser (SystemFExpr Text Text)+app = chainl1 term (return App)++tyapp :: Parser (SystemFExpr Text Text)+tyapp = TyApp+      <$> term+      <*> ty'+  where ty' = symbol '[' *> ty <* symbol ']'++term :: Parser (SystemFExpr Text Text)+term = try abs <|> tyabs <|> var <|> parens expr++var :: Parser (SystemFExpr Text Text)+var = Var <$> exprId++abs :: Parser (SystemFExpr Text Text)+abs = curry'+    <$> (symbol '\\' *> many1 args <* symbol '.') +    <*> expr+  where args = (,) <$> (exprId <* symbol ':') <*> ty+        curry' = flip . foldr . uncurry $ Abs++tyabs :: Parser (SystemFExpr Text Text)+tyabs = curry' <$> args <*> expr+  where args = symbol '\\' *> many1 typeId <* symbol '.'+        curry' = flip (foldr TyAbs)++-- Parse type expressions+ty :: Parser (Ty Text)+ty = try arrow++arrow :: Parser (Ty Text)+arrow = chainr1 tyterm (symbol' "->" $> TyArrow)++tyterm :: Parser (Ty Text)+tyterm = tyvar <|> parens ty++tyvar :: Parser (Ty Text)+tyvar = TyVar <$> typeId++parens :: Parser a -> Parser a+parens p = symbol '(' *> p <* symbol ')'++identifier :: Parser Char -> Parser Text+identifier firstChar = lexeme $ Text.cons <$> first' <*> (Text.pack <$> many rest)+  where first' = firstChar <|> char '_'+        rest = first' <|> digit++typeId, exprId :: Parser Text+typeId = identifier upper+exprId = identifier lower++whitespace :: Parser ()+whitespace = void . many . oneOf $ " \t"++symbol :: Char -> Parser ()+symbol = void . lexeme . char++symbol' :: Text -> Parser ()+symbol' = void . lexeme . string . Text.unpack++lexeme :: Parser a -> Parser a+lexeme p = p <* whitespace

@@ -0,0 +1,89 @@+module Language.Lambda.SystemF.State+  ( TypecheckState(..),+    Typecheck(),+    Context(),+    runTypecheck,+    execTypecheck,+    unsafeRunTypecheck,+    unsafeExecTypecheck,+    mkTypecheckState,+    context,+    uniques,+    getContext,+    getUniques,+    modifyContext,+    modifyUniques,+    setContext,+    setUniques+  ) where++import Language.Lambda.Shared.Errors (LambdaException(..))+import Language.Lambda.SystemF.Expression (Ty(..))++import Control.Monad.Except (Except(), runExcept)+import RIO+import RIO.State+import qualified RIO.Map as Map++data TypecheckState name = TypecheckState+  { tsContext :: Context name,+    tsUniques :: [name]+  }++type Typecheck name+  = StateT (TypecheckState name)+      (Except LambdaException)++type Context name = Map name (Ty name)++runTypecheck+  :: Typecheck name result+  -> TypecheckState name+  -> Either LambdaException (result, TypecheckState name)+runTypecheck computation = runExcept . runStateT computation++execTypecheck+  :: Typecheck name result+  -> TypecheckState name+  -> Either LambdaException result+execTypecheck computation = runExcept . evalStateT computation++unsafeRunTypecheck+  :: Typecheck name result+  -> TypecheckState name+  -> (result, TypecheckState name)+unsafeRunTypecheck computation state' = either impureThrow id tcResult+  where tcResult = runTypecheck computation state'++unsafeExecTypecheck :: Typecheck name result -> TypecheckState name -> result+unsafeExecTypecheck computation state' = either impureThrow id tcResult+  where tcResult = execTypecheck computation state'++mkTypecheckState :: [name] -> TypecheckState name+mkTypecheckState = TypecheckState Map.empty++uniques :: Lens' (TypecheckState name) [name]+uniques f state' = (\uniques' -> state' { tsUniques = uniques' })+  <$> f (tsUniques state')++context :: Lens' (TypecheckState name) (Context name)+context f state' = (\context' -> state' { tsContext = context' })+  <$> f (tsContext state')++getUniques :: Typecheck name [name]+getUniques = gets (^. uniques)++getContext :: Typecheck name (Context name)+getContext = gets (^. context)++modifyContext :: (Context name -> Context name) -> Typecheck name ()+modifyContext f = modify $ context %~ f++modifyUniques :: ([name] -> [name]) -> Typecheck name ()+modifyUniques f = modify $ uniques %~ f++setUniques :: [name] -> Typecheck name ()+setUniques uniques' = modify (& uniques .~ uniques')++setContext :: Context name -> Typecheck name ()+setContext context' = modify (& context .~ context')

@@ -0,0 +1,122 @@+module Language.Lambda.SystemF.TypeCheck where++import Language.Lambda.Shared.Errors (LambdaException(..))+import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.State++import Control.Monad.Except (MonadError(..))+import Prettyprinter+import RIO+import qualified RIO.List as List+import qualified RIO.Map as Map++type UniqueSupply n = [n]+type Context' n t = Map n t++-- TODO: name/ty different types+typecheck+  :: (Ord name, Pretty name)+  => SystemFExpr name name+  -> Typecheck name (Ty name)+typecheck (Var v) = typecheckVar v+typecheck (Abs n t body) = typecheckAbs n t body+typecheck (App e1 e2) = typecheckApp e1 e2+typecheck (TyAbs t body) = typecheckTyAbs t body+typecheck (TyApp e ty) = typecheckTyApp e ty++typecheckVar :: Ord name => name -> Typecheck name (Ty name)+typecheckVar var = getContext >>= defaultToFreshTyVar . Map.lookup var+  where defaultToFreshTyVar (Just v) = return v+        defaultToFreshTyVar Nothing = TyVar <$> unique++typecheckAbs+  :: (Ord name, Pretty name)+  => name+  -> Ty name+  -> SystemFExpr name name+  -> Typecheck name (Ty name)+typecheckAbs name ty body+  = modifyContext (Map.insert name ty)+    >> TyArrow ty <$> typecheck body++typecheckApp+  :: (Ord name, Pretty name)+  => SystemFExpr name name+  -> SystemFExpr name name+  -> Typecheck name (Ty name)+typecheckApp e1 e2 = do+  -- Typecheck expressions+  t1 <- typecheck e1+  t2 <- typecheck e2++  -- Verify the type of t1 is an Arrow+  (t1AppInput, t1AppOutput) <- case t1 of+    (TyArrow appInput appOutput) -> return (appInput, appOutput)+    t1' -> throwError $ tyMismatchError t1' t1++  -- Verify the output of e1 matches the type of e2+  if t1AppInput == t2+    then return t1AppOutput+    else throwError $ tyMismatchError (TyArrow t2 t1AppOutput) (TyArrow t1 t1AppOutput)++typecheckTyAbs+  :: (Ord name, Pretty name)+  => name+  -> SystemFExpr name name+  -> Typecheck name (Ty name)+typecheckTyAbs ty body+  = modifyContext (Map.insert ty (TyVar ty))+    >> TyForAll ty <$> typecheck body++typecheckTyApp+  :: (Ord name, Pretty name)+  => SystemFExpr name name+  -> Ty name+  -> Typecheck name (Ty name)+typecheckTyApp (TyAbs t expr) ty = typecheck $ substitute ty t expr+typecheckTyApp expr _ = typecheck expr++unique :: Typecheck name name+unique = getUniques >>= fromJust' . List.headMaybe+  where fromJust' (Just u) = return u+        fromJust' Nothing = throwError ImpossibleError++substitute+  :: Eq n+  => Ty n+  -> n+  -> SystemFExpr n n+  -> SystemFExpr n n+substitute ty name (App e1 e2) = App (substitute ty name e1) (substitute ty name e2)+substitute ty name (Abs n ty' e) = Abs n (substituteTy ty name ty') (substitute ty name e)+substitute ty name (TyAbs ty' e) = TyAbs ty' (substitute ty name e) +substitute ty name (TyApp e ty') = TyApp (substitute ty name e) (substituteTy ty name ty')+substitute _ _ expr = expr++substituteTy+  :: Eq name+  => Ty name+  -> name+  -> Ty name+  -> Ty name+substituteTy ty name (TyArrow t1 t2) +  = TyArrow (substituteTy ty name t1) (substituteTy ty name t2)+substituteTy ty name ty'@(TyVar name') +  | name == name' = ty+  | otherwise     = ty'+substituteTy _ name t2@(TyForAll name' t2') +  | name == name' = t2+  | otherwise     = TyForAll name' (substituteTy t2 name t2')+++tyMismatchError+  :: (Pretty t1, Pretty t2)+  => t1+  -> t2+  -> LambdaException+tyMismatchError expected actual+  = TyMismatchError+  $ "Couldn't match expected type "+  <> prettyPrint expected+  <> " with actual type "+  <> prettyPrint actual

@@ -0,0 +1,52 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.Lambda.Untyped (+  evalText,+  runEvalText,+  execEvalText,+  unsafeExecEvalText,+  defaultUniques,++  module Language.Lambda.Untyped.Expression,+  module Language.Lambda.Untyped.Eval,+  module Language.Lambda.Untyped.Parser,+  module Language.Lambda.Untyped.State+  ) where++import Control.Monad.Except+import Data.Either+import RIO+import qualified RIO.Text as Text++import Language.Lambda.Shared.Errors+import Language.Lambda.Shared.UniqueSupply (defaultUniques)+import Language.Lambda.Untyped.Eval+import Language.Lambda.Untyped.Expression+import Language.Lambda.Untyped.Parser+import Language.Lambda.Untyped.State++evalText :: Text -> Eval Text (LambdaExpr Text)+evalText = either throwParseError evalExpr' . parseExpr+  where throwParseError = throwError . ParseError . Text.pack . show+        evalExpr' = evalExpr++runEvalText+  :: Text+  -> Globals Text+  -> Either LambdaException (LambdaExpr Text, EvalState Text)+runEvalText input globals' = runEval (evalText input) (mkState globals')++execEvalText+  :: Text+  -> Globals Text+  -> Either LambdaException (LambdaExpr Text)+execEvalText input globals' = execEval (evalText input) (mkState globals')++unsafeExecEvalText+  :: Text+  -> Globals Text+  -> LambdaExpr Text+unsafeExecEvalText input globals'+  = unsafeExecEval (evalText input) (mkState globals')++mkState :: Globals Text -> EvalState Text+mkState = flip EvalState defaultUniques

@@ -0,0 +1,121 @@+module Language.Lambda.Untyped.Eval+  ( EvalState(..),+    evalExpr,+    subGlobals,+    betaReduce,+    alphaConvert,+    etaConvert,+    freeVarsOf+  ) where++import Control.Monad.Except+import Prettyprinter+import RIO+import RIO.List (find)+import qualified RIO.Map as Map++import Language.Lambda.Shared.Errors+import Language.Lambda.Untyped.Expression+import Language.Lambda.Untyped.State++-- | Evaluate an expression+evalExpr :: (Pretty name, Ord name) => LambdaExpr name -> Eval name (LambdaExpr name)+evalExpr (Let name expr) = do+  globals' <- getGlobals+  result <- evalExpr' $ subGlobals globals' expr++  setGlobals $ Map.insert name result globals'++  return $ Let name result++evalExpr expr = do+  globals' <- getGlobals+  evalExpr' $ subGlobals globals' expr++-- | Evaluate an expression; does not support `let`+evalExpr' :: (Eq name, Pretty name) => LambdaExpr name -> Eval name (LambdaExpr name)+evalExpr' expr@(Var _) = return expr+evalExpr' (Abs name expr) = Abs name <$> evalExpr' expr+evalExpr' (App e1 e2) = do+  e1' <- evalExpr' e1+  e2' <- evalExpr' e2+  betaReduce e1' e2'+evalExpr' expr@(Let _ _) = throwError . InvalidLet . prettyPrint $ expr++-- | Look up free vars that have global bindings and substitute them+subGlobals+  :: Ord name+  => Map name (LambdaExpr name)+  -> LambdaExpr name+  -> LambdaExpr name+subGlobals globals' expr@(Var x) = Map.findWithDefault expr x globals'+subGlobals globals' (App e1 e2) = App (subGlobals globals' e1) (subGlobals globals' e2)+subGlobals globals' (Abs name expr) = Abs name expr'+  where expr'+          | Map.member name globals' = expr+          | otherwise = subGlobals globals' expr+subGlobals _ expr = expr++-- | Function application+betaReduce+  :: (Eq name, Pretty name)+  => LambdaExpr name+  -> LambdaExpr name+  -> Eval name (LambdaExpr name)+betaReduce expr@(Var _) e2 = return $ App expr e2+betaReduce (App e1 e1') e2 = do+  reduced <- betaReduce e1 e1'+  return $ App reduced e2+betaReduce (Abs n e1) e2 = do+  e1' <- alphaConvert (freeVarsOf e2) e1+  evalExpr' $ substitute e1' n e2+betaReduce _ _ = throwError ImpossibleError++-- | Rename abstraction parameters to avoid name captures+alphaConvert :: Eq name => [name] -> LambdaExpr name -> Eval name (LambdaExpr name)+alphaConvert freeVars (Abs name body) = do+  uniques' <- getUniques+  let nextVar = fromMaybe name $ find (`notElem` freeVars) uniques'++  if name `elem` freeVars+    then return $ Abs nextVar (substitute body name (Var nextVar))+    else Abs name <$> alphaConvert freeVars body++alphaConvert _ expr = return expr++-- | Eliminite superfluous abstractions+etaConvert :: Eq n => LambdaExpr n -> LambdaExpr n+etaConvert (Abs n (App e1 (Var n')))+  | n == n'   = etaConvert e1+  | otherwise = Abs n (App (etaConvert e1) (Var n'))+etaConvert (Abs n e@(Abs _ _)) +  -- If `etaConvert e == e` then etaConverting it will create an infinite loop+  | e == e'   = Abs n e'+  | otherwise = etaConvert (Abs n e')+  where e' = etaConvert e+etaConvert (Abs n expr) = Abs n (etaConvert expr)+etaConvert (App e1 e2)  = App (etaConvert e1) (etaConvert e2)+etaConvert expr = expr++-- | Substitute an expression for a variable name in another expression+substitute :: Eq name => LambdaExpr name -> name -> LambdaExpr name -> LambdaExpr name+substitute subExpr@(Var name) subName inExpr+  | name == subName = inExpr+  | otherwise = subExpr++substitute subExpr@(Abs name expr) subName inExpr+  | name == subName = subExpr+  | otherwise = Abs name (substitute expr subName inExpr)++substitute (App e1 e2) subName inExpr+  = App (sub e1) (sub e2)+  where sub expr = substitute expr subName inExpr++substitute _ _ expr = expr++-- | Find the free variables in an expression+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]+freeVarsOf _ = []

@@ -0,0 +1,57 @@+module Language.Lambda.Untyped.Expression+  ( LambdaExpr(..),+    lambda,+    prettyPrint+  ) where++import RIO+import Prettyprinter+import Prettyprinter.Render.Text (renderStrict)++data LambdaExpr name+  = Var name                                -- ^ Variables+  | App (LambdaExpr name) (LambdaExpr name) -- ^ Application+  | Abs name (LambdaExpr name)              -- ^ Abstractions+  | Let name (LambdaExpr name)              -- ^ Let bindings+  deriving (Eq, Show)++instance Pretty name => Pretty (LambdaExpr name) where+  pretty (Var name) = pretty name+  pretty (Abs name body) = prettyAbs name body+  pretty (App e1 e2) = prettyApp e1 e2+  pretty (Let name body) = prettyLet name body++prettyPrint :: Pretty name => LambdaExpr name -> Text+prettyPrint expr = renderStrict docStream+  where docStream = layoutPretty defaultLayoutOptions (pretty expr)++lambda :: Char+lambda = 'λ'++prettyAbs :: Pretty name => name -> LambdaExpr name -> Doc a+prettyAbs name body+  = lambda' <> hsep (map pretty names) <> dot+    <+> pretty body'+  where (names, body') = uncurryAbs name body++prettyApp :: Pretty name => LambdaExpr name -> LambdaExpr name -> Doc a+prettyApp e1@(Abs _ _) e2@(Abs _ _) = parens (pretty e1) <+> parens (pretty e2)+prettyApp e1@(Abs _ _) e2 = parens (pretty e1) <+> pretty e2+prettyApp e1 e2@(Abs _ _) = pretty e1 <+> parens (pretty e2)+prettyApp e1 e2@(App _ _) = pretty e1 <+> parens (pretty e2)+prettyApp e1 e2 = pretty e1 <+> pretty e2++prettyLet :: Pretty name => name -> LambdaExpr name -> Doc a+prettyLet name body+  = pretty ("let"::Text)+    <+> pretty name+    <+> "="+    <+> pretty body++lambda' :: Doc ann+lambda' = pretty lambda++uncurryAbs :: n -> LambdaExpr n -> ([n], LambdaExpr n)+uncurryAbs n = uncurry' [n]+  where uncurry' ns (Abs n' body') = uncurry' (n':ns) body'+        uncurry' ns body'          = (reverse ns, body')

@@ -0,0 +1,57 @@+module Language.Lambda.Untyped.Parser+  ( parseExpr,+    module Text.Parsec+  ) where++import Control.Monad+import RIO hiding ((<|>), abs, curry, many, try)+import qualified RIO.Text as Text++import Text.Parsec+import Text.Parsec.Text++import Language.Lambda.Untyped.Expression++parseExpr :: Text -> Either ParseError (LambdaExpr Text)+parseExpr = parse (whitespace *> expr <* eof) ""++expr :: Parser (LambdaExpr Text)+expr = try app <|> term++term :: Parser (LambdaExpr Text)+term = let' <|> abs <|> var <|> parens++var :: Parser (LambdaExpr Text)+var = Var <$> identifier++abs :: Parser (LambdaExpr Text)+abs = curry <$> idents <*> expr+  where idents = symbol '\\' *> many1 identifier <* symbol '.'+        curry = flip (foldr Abs)++app :: Parser (LambdaExpr Text)+app = chainl1 term (return App)++let' :: Parser (LambdaExpr Text)+let' = Let <$> ident <*> expr+  where ident = keyword "let" *> identifier <* symbol '='++parens :: Parser (LambdaExpr Text)+parens = symbol '(' *> expr <* symbol ')'++lexeme :: Parser a -> Parser a+lexeme p =  p <* whitespace++whitespace :: Parser ()+whitespace = void . many . oneOf $ " \t"++identifier :: Parser Text+identifier = lexeme $ Text.cons <$> first' <*> (Text.pack <$> many rest)+  where first' = letter <|> char '_'+        rest  = first' <|> digit++symbol :: Char -> Parser ()+symbol = void . lexeme . char++keyword :: Text -> Parser ()+keyword = void . lexeme . string . Text.unpack

@@ -0,0 +1,88 @@+module Language.Lambda.Untyped.State+  ( EvalState(..),+    Eval(),+    Globals(),+    runEval,+    execEval,+    unsafeExecEval,+    unsafeRunEval,+    globals,+    uniques,+    mkEvalState,+    getGlobals,+    getUniques,+    setGlobals,+    setUniques+  ) where++import Language.Lambda.Shared.Errors+import Language.Lambda.Untyped.Expression ++import Control.Monad.Except+import RIO+import RIO.State+import qualified RIO.Map as Map++-- | The evaluation state+data EvalState name = EvalState+  { esGlobals :: Globals name,+    esUniques :: [name] -- ^ Unused unique names+  }++-- | A stateful computation+type Eval name+  = StateT (EvalState name)+      (Except LambdaException)++-- | A mapping of global variables to expressions+type Globals name = Map name (LambdaExpr name)++-- | Run an evalualation+runEval :: Eval name result -> EvalState name -> Either LambdaException (result, EvalState name)+runEval computation = runExcept . runStateT computation++-- | Run an evalualation, throwing away the final state+execEval :: Eval name result -> EvalState name -> Either LambdaException result+execEval computation = runExcept . evalStateT computation++-- | Run an evaluation. If the result is an error, throws it+unsafeRunEval :: Eval name result -> EvalState name -> (result, EvalState name)+unsafeRunEval computation state'+  = case runEval computation state' of+      Left err -> error $ show err+      Right res -> res+  +-- | Run an evaluation, throwing away the final state. If the result is an error, throws it+unsafeExecEval:: Eval name result -> EvalState name -> result+unsafeExecEval computation state'+  = case execEval computation state' of+      Left err -> impureThrow err+      Right res -> res++-- | Create an EvalState+mkEvalState :: [name] -> EvalState name+mkEvalState = EvalState Map.empty++globals :: Lens' (EvalState name) (Globals name)+globals f state'+  = (\globals' -> state' { esGlobals = globals' })+  <$> f (esGlobals state')++uniques :: Lens' (EvalState name) [name]+uniques f state'+  = (\uniques' -> state' { esUniques = uniques' })+  <$> f (esUniques state')++-- | Access globals from the state monad+getGlobals :: Eval name (Globals name)+getGlobals = gets (^. globals)++-- | Access unique supply from state monad+getUniques :: Eval name [name]+getUniques = gets (^. uniques)++setGlobals :: Globals name -> Eval name ()+setGlobals globals' = modify (& globals .~ globals')++setUniques :: [name] -> Eval name ()+setUniques uniques' = modify (& uniques .~ uniques')

@@ -1,53 +0,0 @@-{-# 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 = 'Λ'

@@ -1,16 +0,0 @@-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-

@@ -1,145 +0,0 @@-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)-  | TyForAll name (Ty name)     -- Universal type (forall T. X)-  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-pprTy pdoc _     (TyForAll n t) =  pprTyForAll pdoc n t--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--pprTyForAll :: PrettyPrint n-            => PDoc String-            -> n-            -> Ty n-            -> PDoc String-pprTyForAll pdoc n t = prefix <> prettyPrint t `add` pdoc-  where prefix = between (prettyPrint n `add` empty) "forall " ". " 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')

@@ -1,86 +0,0 @@-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

@@ -1,119 +0,0 @@-module Language.SystemF.TypeCheck where--import Data.Map-import Prelude hiding (lookup)--import Language.Lambda.Util.PrettyPrint-import Language.SystemF.Expression--type UniqueSupply n = [n]-type Context n t = Map n t--typecheck :: (Ord n, Eq n, PrettyPrint n)-          => UniqueSupply n -          -> Context n (Ty n)-          -> SystemFExpr n n -          -> Either String (Ty n)-typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v-typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body-typecheck uniqs ctx (App e1 e2)    = tcApp uniqs ctx e1 e2-typecheck uniqs ctx (TyAbs t body) = tcTyAbs uniqs ctx t body-typecheck uniqs ctx (TyApp e ty)   = tcTyApp uniqs ctx e ty--tcVar :: (Ord n, Eq n, PrettyPrint n)-      => UniqueSupply n-      -> Context n (Ty n)-      -> n-      -> Either String (Ty n)-tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)--tcAbs :: (Ord n, Eq n, PrettyPrint n)-      => UniqueSupply n-      -> Context n (Ty n)-      -> n-      -> Ty n-      -> SystemFExpr n n-      -> Either String (Ty n)-tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body-  where ctx' = insert name ty ctx--tcApp :: (Ord n, Eq n, PrettyPrint n)-      => UniqueSupply n-      -> Context n (Ty n)-      -> SystemFExpr n n-      -> SystemFExpr n n-      -> Either String (Ty n)-tcApp uniqs ctx e1 e2 = do-    t1 <- typecheck uniqs ctx e1-    t2 <- typecheck uniqs ctx e2--    -- Unwrap t1; Should be (t2 -> *)-    (t2', t3) <- either genMismatchVar return (arrow t1)--    if t2' == t2-      then return t3-      else Left $ tyMismatchMsg (TyArrow t2 t3) (TyArrow t1 t3)--  where genMismatchVar expected = tyMismatchMsg expected <$> unique uniqs >>= Left-        arrow (TyArrow t1 t2) = return (t1, t2)-        arrow t               = Left t--tcTyAbs :: (Ord n, Eq n, PrettyPrint n)-        => UniqueSupply n-        -> Context n (Ty n)-        -> n-        -> SystemFExpr n n-        -> Either String (Ty n)-tcTyAbs uniqs ctx ty body = TyForAll ty <$> typecheck uniqs ctx' body-  where ctx' = insert ty (TyVar ty) ctx--tcTyApp :: (Ord n, Eq n, PrettyPrint n)-        => UniqueSupply n-        -> Context n (Ty n)-        -> SystemFExpr n n-        -> Ty n-        -> Either String (Ty n)-tcTyApp uniqs ctx (TyAbs t expr) ty = typecheck uniqs ctx expr'-  where expr' = sub t ty expr-tcTyApp uniqs ctx expr ty = typecheck uniqs ctx expr---- Utilities-unique :: UniqueSupply t-       -> Either String t-unique (u:_) = return u-unique _     = fail "Unique supply ran out"--sub :: Eq n-    => n-    -> Ty n-    -> SystemFExpr n n-    -> SystemFExpr n n-sub name ty (App e1 e2)   = App (sub name ty e1) (sub name ty e2)-sub name ty (Abs n ty' e) = Abs n (subTy name ty ty') (sub name ty e)-sub name ty (TyAbs ty' e) = TyAbs ty' (sub name ty e) -sub name ty (TyApp e ty') = TyApp (sub name ty e) (subTy name ty ty')-sub name ty expr = expr--subTy :: Eq n-      => n-      -> Ty n-      -> Ty n-      -> Ty n-subTy name ty (TyArrow t1 t2) -  = TyArrow (subTy name ty t1) (subTy name ty t2)-subTy name ty ty'@(TyVar name') -  | name == name' = ty-  | otherwise     = ty'-subTy name t1 t2@(TyForAll name' t2') -  | name == name' = t2-  | otherwise     = TyForAll name' (subTy name t2 t2')---tyMismatchMsg :: (PrettyPrint t, PrettyPrint t')-              => t-              -> t'-              -> String-tyMismatchMsg expected actual = "Couldn't match expected type " ++-                                prettyPrint expected ++-                                " with actual type " ++-                                prettyPrint actual

@@ -1,16 +0,0 @@-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

@@ -1,110 +0,0 @@-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 "etaConvert" $ do-    it "eta converts simple expressions" $ do-      let expr = Abs "x" $ App (Var "f") (Var "x")-      etaConvert expr `shouldBe` Var "f" --    it "eta converts nested applications" $ do-      let expr = Abs "y" $ App (App (Var "f") (Var "x")) (Var "y")-      etaConvert expr `shouldBe` App (Var "f") (Var "x")--      let expr' = Abs "x" $ Abs "y" (App (App (Var "f") (Var "x")) (Var "y"))-      etaConvert expr' `shouldBe` Var "f" --      let expr'' = Abs "x" (Abs "y" (App (Var "y") (Var "x")))-      etaConvert expr'' `shouldBe` expr''--      let expr''' = Abs "f" (Abs "x" (Var "x"))-      etaConvert expr''' `shouldBe` expr'''--    it "ignores non-eta convertable expressions" $ do-      let expr = Abs "x" $ Var "x"-      etaConvert expr `shouldBe` expr--  describe "freeVarsOf" $ do-    it "Returns simple vars" $-      freeVarsOf (Var "x") `shouldBe` ["x"]-  -    it "Does not return bound vars" $-      freeVarsOf (Abs "x" (Var "x")) `shouldBe` []--    it "Returns nested simple vars" $-      freeVarsOf (Abs "x" (Var "y")) `shouldBe` ["y"]--    it "Returns applied simple vars" $-      freeVarsOf (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]

@@ -1,108 +0,0 @@-module Language.Lambda.Examples.BoolSpec where--import Test.Hspec--import Language.Lambda.HspecUtils--spec :: Spec-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-    ---    -- 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" $-      "(\\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" $-      "(\\x y. x y x) (\\t f. f) (\\t f. f)" `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" $-      "(\\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" $-      "(\\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 "false or true = true" $-      "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"--    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" $-      "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"--    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" $-      "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"--    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" $-      "(\\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" $-      "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"--    it "it false p q = q" $-      "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"

@@ -1,102 +0,0 @@-module Language.Lambda.Examples.NatSpec where--import Test.Hspec--import Language.Lambda.HspecUtils--spec :: Spec-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" $-      "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. 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" $-      "(\\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" $-      "(\\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" $-      "(\\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" $-      "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"-        `shouldEvalTo` "\\f x. 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" $-      "(\\m n f. m (n f)) (\\f x. x) n"-        `shouldEvalTo` "\\f x. 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--    -- 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" $-      "(\\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" $-      "(\\m n f x. (n m) f x) n (\\f x. x)"-        `shouldEvalTo` "\\f x. 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"

@@ -1,38 +0,0 @@-module Language.Lambda.Examples.PairSpec where--import Language.Lambda.HspecUtils--import Test.Hspec--spec :: Spec-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-    ---    -- 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" $-      "(\\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" $-      "(\\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"

@@ -1,39 +0,0 @@-module Language.Lambda.ExpressionSpec where--import Test.Hspec--import Language.Lambda.Expression-import Language.Lambda.Util.PrettyPrint--spec :: Spec-spec = describe "prettyPrint" $ do-    it "prints simple variables" $ -      prettyPrint (Var "x") `shouldBe` "x"--    it "prints simple abstractions" $-      prettyPrint (Abs "x" (Var "x")) `shouldBe` "λx. x"--    it "prints simple applications" $-      prettyPrint (App (Var "a") (Var "b"))-        `shouldBe` "a b"--    it "prints nested abstractions" $-      prettyPrint (Abs "f" (Abs "x" (Var "x")))-        `shouldBe` "λf x. 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 "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)"

@@ -1,11 +0,0 @@-module Language.Lambda.HspecUtils where--import Test.Hspec--import Language.Lambda--shouldEvalTo :: String -> String -> Expectation-shouldEvalTo s1 = shouldBe (eval s1) . eval--eval :: String -> Either ParseError (LambdaExpr String)-eval = evalString

@@ -1,53 +0,0 @@-module Language.Lambda.ParserSpec (spec) where--import Data.Either--import Test.Hspec--import Language.Lambda.Expression-import Language.Lambda.Parser--spec :: Spec-spec = 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. x" `shouldBe` Right (Abs "x" (Var "x"))--  it "parses nested abstractions" $-    parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))--  it "parses simple applications" $-    parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))--  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 "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-            -

@@ -0,0 +1,87 @@+{-# LANGUAGE OverloadedStrings, NoImplicitPrelude #-}+module Language.Lambda.SystemF.ExpressionSpec where++import RIO+import Test.Hspec++import Language.Lambda.SystemF.Expression++spec :: Spec+spec = describe "prettyPrint" $ do+  let prettyPrint' :: SystemFExpr Text Text -> Text+      prettyPrint' = prettyPrint++      prettyPrintTy :: Ty Text -> Text+      prettyPrintTy = prettyPrint+  +  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 "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 "A" (TyAbs "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" $+    prettyPrintTy (TyVar "X") `shouldBe` "X"++  it "print simple arrow types" $+    prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"++  it "prints simple forall types" $+    prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"++  it "prints chained arrow types" $+    prettyPrintTy (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))+      `shouldBe` "X -> Y -> Z"++  it "prints nested arrow types" $+    prettyPrintTy (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))+      `shouldBe` "(T -> U) -> V"++  it "prints complex forall types" $+    prettyPrintTy (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))+      `shouldBe` "forall A. A -> A"++  it "prints nested forall types" $+    prettyPrintTy (TyForAll "W" +                  (TyForAll "X" +                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))+      `shouldBe` "forall W. forall X. W -> X -> Y"+

@@ -0,0 +1,86 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.SystemF.ParserSpec (spec) where++import Data.Either++import RIO+import Test.Hspec++import Language.Lambda.SystemF.Expression+import Language.Lambda.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"))

@@ -0,0 +1,71 @@+module Language.Lambda.SystemF.TypeCheckSpec (spec) where++import Data.Either+import Data.Map+import Prettyprinter+import Test.Hspec++import Language.Lambda.Shared.Errors+import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.State+import Language.Lambda.SystemF.TypeCheck++tc uniqs ctx expr = execTypecheck (typecheck expr) (TypecheckState (fromList ctx) uniqs)++spec :: Spec+spec = describe "typecheck" $ do+  it "typechecks simple variables in context" $+    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")++  it "typechecks simple variables not in context" $ +    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")++  it "typechecks simple abstractions" $+    tc [] [] (Abs "x" (TyVar "A") (Var "x")) +      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))++  it "typechecks simple applications" $ do+    let ctx = [+          ("f", TyArrow (TyVar "T") (TyVar "U")),+          ("a", TyVar "T")+          ]++    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")++  it "apply variable to variable fails" $ do+    let ctx = [+          ("a", TyVar "A"),+          ("b", TyVar "B")+          ]++    tc ["C"] ctx (App (Var "a") (Var "b")) +      `shouldSatisfy` isLeft++  it "apply arrow to variable of wrong type fails" $ do+    let ctx = [+          ("f", TyArrow (TyVar "F") (TyVar "G")),+          ("b", TyVar "B")+          ]++    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft++  it "typechecks simple type abstractions" $+    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))++  it "typechecks type abstractions with simple abstraction" $+    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) +      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))++  it "typechecks type abstractions with application" $+    tc [] [("y", TyVar "Y")] +      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) +           (Var "y"))+      `shouldBe` Right (TyVar "Y")++  it "typechecks simple type applications" $+    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))+      `shouldBe` Right (TyVar "A")++  it "typechecks type applications with simple abstraction" $+    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))+      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))

@@ -0,0 +1,9 @@+module Language.Lambda.SystemFSpec where++import Test.Hspec++import Language.Lambda.SystemF++spec :: Spec+spec = describe "evalString" $ +  return ()

@@ -0,0 +1,160 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.EvalSpec where++import Data.Map (fromList)+import RIO+import Test.Hspec++import Language.Lambda.Shared.Errors+import Language.Lambda.Untyped+import Language.Lambda.Untyped.Eval+import Language.Lambda.Untyped.State++spec :: Spec+spec = do+  describe "evalExpr" $ do+    let evalExpr' expr = execEval (evalExpr expr) (mkEvalState defaultUniques)++    it "beta reduces" $ do+      let expr = App (Abs "x" (Var "x")) (Var "z")+      evalExpr' expr `shouldBe` Right (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` Right (App (Var "g") (Var "y"))++    it "reduces inner redexes" $ do+      let expr = Abs "x" (App (Abs "y" (Var "y")) (Var "x"))+      evalExpr' expr `shouldBe` Right (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` Right (Abs "z" (Var "x"))++    it "reduces let bodies" $ do+      let expr = Let "x" $ App (Abs "y" (Var "y")) (Var "z")+      evalExpr' expr `shouldBe` Right (Let "x" (Var "z"))++    it "let expressions update state" $ do+      let res = flip unsafeExecEval (mkEvalState defaultUniques) $ do+            _ <- evalExpr $ Let "w" (Var "x")+            evalExpr $ Var "w"++      res `shouldBe` Var "x"++    it "nested let expressions fail" $ do+      let res = flip unsafeExecEval (mkEvalState defaultUniques) $ do+            evalExpr $ Let "x" (Let "y" (Var "z"))+      evaluate res `shouldThrow` isLetError++  describe "subGlobals" $ do+    let globals' :: Map String (LambdaExpr String)+        globals' = fromList [("w", Var "x")] +        subGlobals' = subGlobals globals'+    +    it "subs simple variables" $+      subGlobals' (Var "w") `shouldBe` Var "x"++    it "does not sub shadowed bindings" $ do+      let expr = Abs "w" (Var "w")+      subGlobals' expr `shouldBe` expr++    xit "does not capture globals" $ do+      let expr = Abs "x" (Var "w")+      subGlobals' expr `shouldBe` Abs "a" (Var "x")++  describe "betaReduce" $ do+    let betaReduce' :: LambdaExpr Text -> LambdaExpr Text -> LambdaExpr Text+        betaReduce' e1 e2 = unsafeExecEval (betaReduce e1 e2) (mkEvalState [])+    +    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+    let alphaConvert' :: [Text] -> [Text] -> LambdaExpr Text -> LambdaExpr Text+        alphaConvert' uniques' fvs expr+          = unsafeExecEval (alphaConvert fvs expr) (mkEvalState uniques')+    +    it "alpha converts simple expressions" $ do+      let freeVars = ["x"] :: [Text]+          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 "etaConvert" $ do+    it "eta converts simple expressions" $ do+      let expr :: LambdaExpr Text+          expr = Abs "x" $ App (Var "f") (Var "x") :: LambdaExpr Text+      etaConvert expr `shouldBe` Var "f" ++    it "eta converts nested applications" $ do+      let expr :: LambdaExpr Text+          expr = Abs "y" $ App (App (Var "f") (Var "x")) (Var "y")+      etaConvert expr `shouldBe` App (Var "f") (Var "x")++      let expr' :: LambdaExpr Text+          expr' = Abs "x" $ Abs "y" (App (App (Var "f") (Var "x")) (Var "y"))+      etaConvert expr' `shouldBe` Var "f" ++      let expr'' :: LambdaExpr Text+          expr'' = Abs "x" (Abs "y" (App (Var "y") (Var "x")))+      etaConvert expr'' `shouldBe` expr''++      let expr''' :: LambdaExpr Text+          expr''' = Abs "f" (Abs "x" (Var "x"))+      etaConvert expr''' `shouldBe` expr'''++    it "ignores non-eta convertable expressions" $ do+      let expr :: LambdaExpr Text+          expr = Abs "x" $ Var "x"+      etaConvert expr `shouldBe` expr++  describe "freeVarsOf" $ do+    let freeVarsOf' :: LambdaExpr Text -> [Text]+        freeVarsOf' = freeVarsOf+    +    it "Returns simple vars" $+      freeVarsOf' (Var "x") `shouldBe` ["x"]+  +    it "Does not return bound vars" $+      freeVarsOf' (Abs "x" (Var "x")) `shouldBe` []++    it "Returns nested simple vars" $+      freeVarsOf' (Abs "x" (Var "y")) `shouldBe` ["y"]++    it "Returns applied simple vars" $+      freeVarsOf' (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]

@@ -0,0 +1,110 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.Examples.BoolSpec where++import RIO+import Test.Hspec++import Language.Lambda.Untyped.HspecUtils++spec :: Spec+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+    --+    -- 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" $+      "(\\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" $+      "(\\x y. x y x) (\\t f. f) (\\t f. f)" `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" $+      "(\\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" $+      "(\\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 "false or true = true" $+      "(\\x y. x x y) (\\t f. f) (\\t f. t)" `shouldEvalTo` "\\t f. t"++    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" $+      "(\\x y. x x y) (\\t f. t) p" `shouldEvalTo` "\\t f. t"++    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" $+      "(\\x. x (\\t f. f) (\\t f. t)) \\t f. t" `shouldEvalTo` "\\t f. f"++    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" $+      "(\\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" $+      "(\\p x y. p x y) (\\t f. t) p q" `shouldEvalTo` "p"++    it "it false p q = q" $+      "(\\p x y. p x y) (\\t f. f) p q" `shouldEvalTo` "q"

@@ -0,0 +1,104 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.Examples.NatSpec where++import RIO+import Test.Hspec++import Language.Lambda.Untyped.HspecUtils++spec :: Spec+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" $+      "(\\n f x. f (n f x)) (\\f x. x)" `shouldEvalTo` "\\f x. 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" $+      "(\\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" $+      "(\\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" $+      "(\\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" $+      "(\\m n f. m (n f)) (\\f x. x) (\\f x. f (f x))"+        `shouldEvalTo` "\\f x. 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" $+      "(\\m n f. m (n f)) (\\f x. x) n"+        `shouldEvalTo` "\\f x. 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++    -- 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" $+      "(\\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" $+      "(\\m n f x. (n m) f x) n (\\f x. x)"+        `shouldEvalTo` "\\f x. 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"

@@ -0,0 +1,40 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.Examples.PairSpec where++import Language.Lambda.Untyped.HspecUtils++import RIO+import Test.Hspec++spec :: Spec+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+    --+    -- 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" $+      "(\\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" $+      "(\\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"

@@ -0,0 +1,50 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.ExpressionSpec where++import Language.Lambda.Untyped.Expression++import RIO+import Test.Hspec++spec :: Spec+spec = describe "prettyPrint" $ do+    let prettyPrint' :: LambdaExpr Text -> Text+        prettyPrint' = prettyPrint+  +    it "prints simple variables" $+      prettyPrint' (Var "x") `shouldBe` "x"++    it "prints simple abstractions" $+      prettyPrint' (Abs "x" (Var "x")) `shouldBe` "λx. x"++    it "prints simple applications" $+      prettyPrint' (App (Var "a") (Var "b"))+        `shouldBe` "a b"++    it "prints simple let expressions" $+      prettyPrint' (Let "x" (Var "y")) `shouldBe` "let x = y"++    it "prints nested abstractions" $+      prettyPrint' (Abs "f" (Abs "x" (Abs "y" (Var "x"))))+        `shouldBe` "λf x y. 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 "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)"++    it "prints complex let expressions" $+      prettyPrint' (Let "x" (Abs "a" (Abs "b" (App (Var "a") (Var "b")))))+        `shouldBe` "let x = λa b. a b"

@@ -0,0 +1,14 @@+{-# LANGUAGE NoImplicitPrelude #-}+module Language.Lambda.Untyped.HspecUtils where++import RIO+import Test.Hspec++import Language.Lambda.Shared.Errors+import Language.Lambda.Untyped++shouldEvalTo :: Text -> Text -> Expectation+shouldEvalTo s1 = shouldBe (eval s1) . eval++eval :: Text -> Either LambdaException (LambdaExpr Text)+eval input = execEval (evalText input) (mkEvalState defaultUniques)

@@ -0,0 +1,56 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.Untyped.ParserSpec (spec) where++import Language.Lambda.Untyped.Expression+import Language.Lambda.Untyped.Parser++import Data.Either+import Test.Hspec+import RIO++spec :: Spec+spec = 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. x" `shouldBe` Right (Abs "x" (Var "x"))++  it "parses nested abstractions" $+    parseExpr "\\f a. a" `shouldBe` Right (Abs "f" (Abs "a" (Var "a")))++  it "parses simple applications" $+    parseExpr "f x" `shouldBe` Right (App (Var "f") (Var "x"))++  it "parses chained applications" $+    parseExpr "f x y" `shouldBe` Right (App (App (Var "f") (Var "x")) (Var "y"))++  it "parses simple let expressions" $+    parseExpr "let x = z" `shouldBe` Right (Let "x" (Var "z"))++  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",+          "let x = \\f x. f 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

@@ -0,0 +1,77 @@+{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-}+module Language.Lambda.UntypedSpec where++import RIO+import qualified RIO.Map as Map+import qualified RIO.Text as Text+import Test.Hspec++import Language.Lambda.Untyped+import Language.Lambda.Untyped.HspecUtils++spec :: Spec+spec = do+  describe "evalText" $ do+    it "evaluates simple text" $ do+      eval "x" `shouldBe` Right (Var "x")+      eval "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))+      eval "f y" `shouldBe` Right (App (Var "f") (Var "y"))++    it "reduces simple applications" $+      eval "(\\x .x) y" `shouldBe` Right (Var "y")++    it "reduces applications with nested redexes" $+      eval "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))++  describe "runEvalText" $ do+    let runEvalText' input = fst <$> runEvalText input Map.empty+    +    it "evaluates simple strings" $ do+      runEvalText' "x" `shouldBe` Right (Var "x")+      runEvalText' "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))+      runEvalText' "f y" `shouldBe` Right (App (Var "f") (Var "y"))++    it "reduces simple applications" $+      runEvalText' "(\\x .x) y" `shouldBe` Right (Var "y")++    it "reduces applications with nested redexes" $+      runEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))++  describe "execEvalText" $ do+    let execEvalText' input = execEvalText input Map.empty+    +    it "evaluates simple texts" $ do+      execEvalText' "x" `shouldBe` Right (Var "x")+      execEvalText' "\\x. x" `shouldBe` Right (Abs "x" (Var "x"))+      execEvalText' "f y" `shouldBe` Right (App (Var "f") (Var "y"))++    it "reduces simple applications" $+      execEvalText' "(\\x .x) y" `shouldBe` Right (Var "y")++    it "reduces applications with nested redexes" $+      execEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Right (Abs "x" (Var "x"))++  describe "unsafeExecEvalText" $ do+    let unsafeExecEvalText' input = unsafeExecEvalText input Map.empty+    +    it "evaluates simple texts" $ do+      unsafeExecEvalText' "x" `shouldBe` Var "x"+      unsafeExecEvalText' "\\x. x" `shouldBe` Abs "x" (Var "x")+      unsafeExecEvalText' "f y" `shouldBe` App (Var "f") (Var "y")++    it "reduces simple applications" $+      unsafeExecEvalText' "(\\x .x) y" `shouldBe` Var "y"++    it "reduces applications with nested redexes" $+      unsafeExecEvalText' "(\\f x. f x) (\\y. y)" `shouldBe` Abs "x" (Var "x")++  describe "defaultUniques" $ do+    let alphabet = reverse ['a'..'z']+        len = length alphabet+    +    it "starts with plain alphabet" $+      take len defaultUniques `shouldBe` map (`Text.cons` Text.empty) alphabet++    it "adds index afterwards" $+      take len (drop len defaultUniques)+        `shouldBe` map (`Text.cons` Text.singleton '0') alphabet

@@ -1,36 +0,0 @@-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

@@ -1,30 +0,0 @@-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" $-      evalString "(\\x .x) y" `shouldBe` Right (Var "y")--    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" $-      take len uniques `shouldBe` map (:[]) alphabet--    it "adds index afterwards" $-      take len (drop len uniques) `shouldBe` map (:['0']) alphabet-

@@ -1,81 +0,0 @@-{-# 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 simple forall types" $-    prettyPrint (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"--  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"--  it "prints complex forall types" $-    prettyPrint (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))-      `shouldBe` "forall A. A -> A"--  it "prints nested forall types" $-    prettyPrint (TyForAll "W" -                  (TyForAll "X" -                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))-      `shouldBe` "forall W. forall X. W -> X -> Y"-

@@ -1,84 +0,0 @@-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"))

@@ -1,75 +0,0 @@-module Language.SystemF.TypeCheckSpec (spec) where--import Data.Either-import Data.Map--import Test.Hspec--import Language.Lambda.Util.PrettyPrint-import Language.SystemF.Expression-import Language.SystemF.TypeCheck--tc :: (Ord n, Eq n, PrettyPrint n)-          => UniqueSupply n -          -> [(n, Ty n)]-          -> SystemFExpr n n -          -> Either String (Ty n)-tc uniqs ctx = typecheck uniqs (fromList ctx)--spec :: Spec-spec = describe "typecheck" $ do-  it "typechecks simple variables in context" $-    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")--  it "typechecks simple variables not in context" $ -    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")--  it "typechecks simple abstractions" $-    tc [] [] (Abs "x" (TyVar "A") (Var "x")) -      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))--  it "typechecks simple applications" $ do-    let ctx = [-          ("f", TyArrow (TyVar "T") (TyVar "U")),-          ("a", TyVar "T")-          ]--    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")--  it "apply variable to variable fails" $ do-    let ctx = [-          ("a", TyVar "A"),-          ("b", TyVar "B")-          ]--    tc ["C"] ctx (App (Var "a") (Var "b")) -      `shouldSatisfy` isLeft--  it "apply arrow to variable of wrong type fails" $ do-    let ctx = [-          ("f", TyArrow (TyVar "F") (TyVar "G")),-          ("b", TyVar "B")-          ]--    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft--  it "typechecks simple type abstractions" $-    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))--  it "typechecks type abstractions with simple abstraction" $-    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) -      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))--  it "typechecks type abstractions with application" $-    tc [] [("y", TyVar "Y")] -      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) -           (Var "y"))-      `shouldBe` Right (TyVar "Y")--  it "typechecks simple type applications" $-    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))-      `shouldBe` Right (TyVar "A")--  it "typechecks type applications with simple abstraction" $-    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))-      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))

@@ -1,9 +0,0 @@-module Language.SystemFSpec where--import Test.Hspec--import Language.SystemF--spec :: Spec-spec = describe "evalString" $ -  return ()