diff options
17 files changed, 712 insertions, 91 deletions
diff --git a/lambda-calcul/haskell/app/Main.hs b/lambda-calcul/haskell/app/Main.hs index 5b48c01..0b40f60 100644 --- a/lambda-calcul/haskell/app/Main.hs +++ b/lambda-calcul/haskell/app/Main.hs @@ -1,6 +1,12 @@ -import Minilang.IO +import Minilang.IO (runEval) import System.IO (stdin, stdout) +import System.Posix.Terminal (queryTerminal) +import System.Posix (stdInput) +import Minilang.REPL (withTerminal) main :: IO () -main = - runEval stdin stdout +main = do + hasTty <- queryTerminal stdInput + if hasTty + then withTerminal + else runEval stdin stdout diff --git a/lambda-calcul/haskell/minilang.cabal b/lambda-calcul/haskell/minilang.cabal index a2bb355..039e4f0 100644 --- a/lambda-calcul/haskell/minilang.cabal +++ b/lambda-calcul/haskell/minilang.cabal @@ -31,6 +31,13 @@ library Minilang.Lambda.Eval Minilang.Lambda.Infer Minilang.Lambda.Parser + Minilang.REPL + Minilang.REPL.Haskeline + Minilang.REPL.IO + Minilang.REPL.Pure + Minilang.REPL.Purer + Minilang.REPL.Run + Minilang.REPL.Types hs-source-dirs: src default-extensions: @@ -48,16 +55,21 @@ library , async , base , bytestring + , cereal , containers , data-default , directory , exceptions , filepath + , haskeline , megaparsec , mtl , stm , text , unordered-containers + , wai + , websockets + , wai-websockets default-language: Haskell2010 test-suite minilang-test @@ -69,6 +81,8 @@ test-suite minilang-test Minilang.Lambda.DeBruijnSpec Minilang.Lambda.EvalSpec Minilang.Lambda.ParserSpec + Minilang.REPLSpec + Minilang.REPL.HaskelineSpec hs-source-dirs: test default-extensions: @@ -93,6 +107,7 @@ test-suite minilang-test , directory , exceptions , filepath + , haskeline , hspec , hspec-discover , minilang @@ -122,4 +137,5 @@ executable lambda base , containers , minilang + , unix default-language: Haskell2010 diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs index cbbdc51..58f8ba6 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs @@ -9,36 +9,14 @@ data Term | App Term Term deriving (Show, Read, Eq) -type Env = [(Text, Value)] +type Env = [(Text, Term)] -data Value - = V Text - | Abs Text Term Env -- a closure, ie. lambda with its captured environment - | Ap Value Value - deriving (Show, Read, Eq) +newEnv :: Env +newEnv = [] -- call-by-value evaluator -eval :: Term -> Env -> Value -eval (Var x) env = case lookup x env of - Just v -> v -- we do not need to eval v again - Nothing -> V x -- x is not bound in env -eval (Lam x body) env = Abs x body env -eval (App f a) env = - -- we need to force evaluation of the argument - -- because haskell's default semantics is non-strict - -- so if a' is never used, it will not be evaluated! - let a' = eval a env - in seq a' $ case eval f env of - Abs x body env' -> eval body ((x, a') : env') - f' -> Ap f' a' +eval :: Term -> Env -> Term +eval = undefined -evalNeed :: Term -> Env -> Value -evalNeed (Var x) env = case lookup x env of - Just v -> v - Nothing -> V x -evalNeed (Lam x body) env = Abs x body env -evalNeed (App f a) env = - let a' = eval a env - in case evalNeed f env of - Abs x body env' -> evalNeed body ((x, a') : env') - f' -> Ap f' a' +evalNeed :: Term -> Env -> Term +evalNeed = undefined diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs index 415849a..94fecb3 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs @@ -48,14 +48,14 @@ typeOf (Var _ t) = t typeOf (Lam _ _ t) = t typeOf (App _ _ t) = t -data Env = Env {nextVar :: Int, typeEnv :: Map.Map Text Type} +data Context = Context {nextVar :: Int, typeContext :: Map.Map Text Type} deriving (Eq, Show) annotate :: Eval.Term -> Either TypeError (ATerm Type) annotate t = - evalStateT (go (fromTerm t) []) newEnv + evalStateT (go (fromTerm t) []) newContext where - go :: ATerm a -> [(Text, Type)] -> StateT Env (Either TypeError) (ATerm Type) + go :: ATerm a -> [(Text, Type)] -> StateT Context (Either TypeError) (ATerm Type) go t bounds = case t of Var x _ -> case List.lookup x bounds of Just ty -> pure $ Var x ty @@ -73,22 +73,22 @@ annotate t = App a b _ -> App <$> go a bounds <*> go b bounds <*> freshVar -newEnv :: Env -newEnv = Env 0 Map.empty +newContext :: Context +newContext = Context 0 Map.empty -bind :: Text -> Type -> StateT Env (Either TypeError) () +bind :: Text -> Type -> StateT Context (Either TypeError) () bind x ty = do - modify (\(Env n env) -> Env n (Map.insert x ty env)) + modify (\(Context n env) -> Context n (Map.insert x ty env)) -lookup :: Text -> StateT Env (Either TypeError) (Maybe Type) +lookup :: Text -> StateT Context (Either TypeError) (Maybe Type) lookup x = do - Env _ env <- get + Context _ env <- get pure $ Map.lookup x env -freshVar :: (Monad m) => StateT Env m Type +freshVar :: (Monad m) => StateT Context m Type freshVar = do - get >>= \(Env n _) -> - modify (\(Env n' env') -> Env (n' + 1) env') >> pure (TyVar $ nameOf n) + get >>= \(Context n _) -> + modify (\(Context n' env') -> Context (n' + 1) env') >> pure (TyVar $ nameOf n) where nameOf n | n < 26 = pack [chr (n + ord 'a')] diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs index ad06552..df66113 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs @@ -1,4 +1,5 @@ -- ported from https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm +{-# LANGUAGE LambdaCase #-} module Minilang.Lambda.Unify where import Data.Text (Text) @@ -12,6 +13,16 @@ data Type infixr 5 :-> +pretty :: Type -> Text +pretty = \case + TyVar x -> x + f :-> g -> + let left = case f of + TyVar _ -> pretty f + _ -> "(" <> pretty f <> ")" + right = pretty g + in left <> " -> " <> right + -- invariant: no identifier on the left hand-side can appear in -- an earlier term in the list, ie. the list is in "dependency order" -- and forms a DAG. diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs new file mode 100644 index 0000000..a5ffce1 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# OPTIONS_GHC "-fno-warn-orphans" #-} + +module Minilang.REPL where + +import Control.Monad.Catch.Pure (CatchT (..)) +import Control.Monad.State +import Data.Text hiding (replicate) +import Minilang.REPL.Haskeline +import Minilang.REPL.IO +import Minilang.REPL.Pure +import Minilang.REPL.Purer +import Minilang.REPL.Run +import Minilang.REPL.Types +import System.Console.Haskeline ( + defaultBehavior, + defaultSettings, + historyFile, + runInputTBehavior, + setComplete, + ) +import System.IO (Handle) + +-- * Haskeline REPL + +withTerminal :: IO () +withTerminal = + runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) initialREPL + where + settings = setComplete completion $ defaultSettings{historyFile = Just "~/.minilang.history"} + +-- * Other REPLs + +{- | Pure IO REPL + Used for testing purposes +-} + +-- | +withHandles :: + Handle -> Handle -> IO () +withHandles hin hout = + evalStateT (runConsole runREPL) (IOEnv hin hout initialREPL) + +-- * Pure REPL + +withInput :: + [Text] -> [Text] +withInput stream = + outputText $ execState (runCatchT (runPure runREPL)) (PureEnv stream [] initialREPL) +-- * Purer REPL + +-- This useful for rehydrating and environment from a sequence of inputs + +withInputs :: + REPLEnv -> [In] -> PurerEnv +withInputs initEnv stream = + execState (runCatchT (runPurer runREPL)) (PurerEnv stream [] initEnv) diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs new file mode 100644 index 0000000..a822116 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC "-fno-warn-orphans" #-} +{-# LANGUAGE LambdaCase #-} + +module Minilang.REPL.Haskeline where + +import Control.Exception (throw) +import Control.Monad.Catch +import Control.Monad.Reader +import Control.Monad.State +import Data.Bifunctor +import Data.List + ( isPrefixOf, + isSuffixOf, + ) +import Data.Text (pack, unpack) +import Data.Text.IO as Text +import Minilang.REPL.Run (handleCommand) +import Minilang.REPL.Types +import System.Console.Haskeline + ( Completion (Completion, replacement), + CompletionFunc, + InputT, + getInputLineWithInitial, + outputStrLn, + ) +import System.Directory (listDirectory) +import Minilang.Lambda.Parser (resugar, pretty) +import qualified Minilang.Lambda.Unify as Unify + +-- * Haskeline REPL + +newtype Haskeline a = Haskeline {runHaskeline :: StateT REPLEnv (InputT IO) a} + deriving (Functor, Applicative, Monad, MonadIO, MonadState REPLEnv) + +hoist :: InputT IO a -> Haskeline a +hoist m = Haskeline $ StateT $ \s -> m >>= \a -> pure (a, s) + +instance MonadREPL Haskeline where + input = do + i <- hoist (getInputLineWithInitial "λΠ> " ("", "")) + case i of + Nothing -> pure EOF + Just (pack -> t) -> pure $ interpret t + output = hoist . outputStrLn . render + prompt = pure () + load = fmap (first FileError) . hoist . lift . try . Text.readFile . unpack + + getEnv = get + setEnv = put + +render :: Out -> String +render = \case + Msg t -> unpack t + Evaluated term typ -> unpack $ pretty (resugar term) <> " : " <> Unify.pretty typ + other -> show other + +completion :: CompletionFunc IO +completion = completion' . first reverse + +data CompleteWith + = SetUnset String + | LoadFile + | AllCommands + +completion' :: CompletionFunc IO +completion' (inputString, _) = + case matchedCompletionRule inputString of + SetUnset com : _ -> setUnsetCompletion com + LoadFile : _ -> completeLoadWithFiles (drop 6 inputString) + _ -> allCommandCompletions + where + matchedCompletionRule prefix = + snd + <$> filter + (($ prefix) . fst) + [ ((":set" `isPrefixOf`), SetUnset ":set"), + ((":unset" `isPrefixOf`), SetUnset ":unset"), + ((":load" `isPrefixOf`), LoadFile), + (const True, AllCommands) + ] + + completeLoadWithFiles prefix = do + files <- filter (prefix `isPrefixOf`) . filter (".mtt" `isSuffixOf`) <$> listDirectory "." + pure ("", fmap (\fp -> Completion (":load " <> fp) fp True) files) + + setUnsetCompletion com = + pure + ( "", + filter + ((inputString `isPrefixOf`) . replacement) + [ Completion (com <> " step") "step - Step through evaluation process, displaying each rule application" True, + Completion (com <> " debug") "debug - Debug parsing of input" True + ] + ) + + allCommandCompletions = + pure + ( "", + filter + ((inputString `isPrefixOf`) . replacement) + [ Completion ":quit" ":quit - Quit minilang REPL" False, + Completion ":env" ":env - Dump current environment and context (types and values)" False, + Completion ":clear" ":clear - Clear environment" False, + Completion ":load" ":load - Load a file into the REPL" True, + Completion ":set" ":set - Set some properties of the REPL" True, + Completion ":unset" ":unset - Unset some properties of the REPL" True, + Completion ":help" ":help - Provide help on commands" True + ] + ) + +instance MonadCatch Haskeline where + Haskeline m `catch` f = Haskeline $ m `catch` \e -> runHaskeline (f e) + +instance MonadThrow Haskeline where + throwM = throw diff --git a/lambda-calcul/haskell/src/Minilang/REPL/IO.hs b/lambda-calcul/haskell/src/Minilang/REPL/IO.hs new file mode 100644 index 0000000..90b1e5d --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/IO.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ViewPatterns #-} + +module Minilang.REPL.IO where + +import Control.Monad.Catch +import Control.Monad.Reader +import Control.Monad.State +import Data.Text (unpack, pack) +import Data.Text.IO as Text +import Minilang.REPL.Types +import System.IO (Handle, hFlush) +import System.IO.Error (isEOFError) + +data IOEnv = IOEnv + { inputHandle :: Handle, + outputHandle :: Handle, + repl :: REPLEnv + } + +newtype CONSOLE m a = CONSOLE {runConsole :: StateT IOEnv m a} + deriving (Functor, Applicative, Monad, MonadTrans, MonadState IOEnv) + +instance MonadREPL (CONSOLE IO) where + input = get >>= lift . (\h -> (interpret <$> hGetLine h) `catch` \(isEOFError -> True) -> pure EOF) . inputHandle + output a = get >>= lift . flip hPutStrLn (pack $ show a) . outputHandle + prompt = get >>= lift . (\h -> hPutStr h "λΠ> " >> hFlush h) . outputHandle + getEnv = get >>= pure . repl + setEnv e' = modify $ \e -> e {repl = e'} + load = lift . try . Text.readFile . unpack + +instance (MonadThrow m) => MonadThrow (CONSOLE m) where + throwM = lift . throwM + +instance (MonadCatch m) => MonadCatch (CONSOLE m) where + CONSOLE m `catch` f = CONSOLE $ m `catch` \e -> runConsole (f e) diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs new file mode 100644 index 0000000..23c45e1 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} + +module Minilang.REPL.Pure where + +import Control.Exception (throw) +import Control.Monad.Catch +import Control.Monad.Catch.Pure (CatchT (..)) +import Control.Monad.State +import Data.Text hiding (replicate) +import Minilang.REPL.Types + +data PureEnv = PureEnv + { inputText :: [Text], + outputText :: [Text], + pureREPL :: REPLEnv + } + +newtype PureREPL a = PureREPL {runPure :: CatchT (State PureEnv) a} + deriving (Functor, Applicative, Monad, MonadState PureEnv, MonadCatch) + +instance MonadREPL PureREPL where + input = do + ins <- inputText <$> get + case ins of + [] -> pure EOF + (t : ts) -> modify (\e -> e {inputText = ts}) >> pure (interpret t) + + output t = modify $ \e -> e {outputText = render t : outputText e} + prompt = pure () + getEnv = get >>= pure . pureREPL + setEnv e' = modify $ \e -> e {pureREPL = e'} + load f = pure $ Left $ REPLError $ "cannot load file " <> f <> " in Pure interpreter" + +render :: Out -> Text +render = \case + Msg t -> t + Bye -> "Bye!" + other -> pack (show other) + +instance MonadThrow PureREPL where + throwM = throw diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Purer.hs b/lambda-calcul/haskell/src/Minilang/REPL/Purer.hs new file mode 100644 index 0000000..9e4bd22 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Purer.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +module Minilang.REPL.Purer where + + +import Control.Monad.Catch +import Control.Monad.Catch.Pure (CatchT (..)) +import Control.Monad.State +import Minilang.REPL.Types + + +data PurerEnv = PurerEnv + { inputs :: [In] + , outputs :: [Out] + , purerREPL :: REPLEnv + } + +newtype PurerREPL a = PurerREPL { runPurer :: CatchT (State PurerEnv) a } + deriving (Functor, Applicative, Monad, MonadState PurerEnv, MonadCatch, MonadThrow) + +instance MonadREPL PurerREPL where + input = do + ins <- inputs <$> get + case ins of + [] -> pure EOF + (t:ts) -> modify (\ e -> e { inputs = ts }) >> pure t + + output t = modify $ \ e -> e { outputs = t : outputs e } + prompt = pure () + getEnv = get >>= pure . purerREPL + setEnv e' = modify $ \ e -> e { purerREPL = e' } + load f = pure $ Left $ REPLError $ "cannot load file " <> f <> " in Pure interpreter" diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs new file mode 100644 index 0000000..a4b50f4 --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Minilang.REPL.Run where + +import Control.Monad.Catch +import Data.Text hiding (replicate) +import qualified Data.Text as Text +import Debug.Trace (trace) +import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn) +import Minilang.Lambda.Infer (infer, newContext) +import Minilang.Lambda.Parser (desugar, parse) +import Minilang.REPL.Types +import Minilang.Lambda.Eval (newEnv) + +-- | Run a REPL session +runREPL :: + (MonadCatch m, MonadREPL m) => m () +runREPL = go + where + go = do + prompt + raw <- input + case raw of + EOF -> output Bye + In txt -> handleUserInput txt >> go + Com cmd -> handleCommand cmd >> go + +handleUserInput :: + (MonadCatch m, MonadREPL m) => + Text -> + m () +handleUserInput txt = do + -- repl@REPLEnv {env, context, debugParser} <- getEnv + case parse txt of + Left err -> output (Msg $ pack $ show err) + Right expr -> do + let term = desugar expr + case infer term of + Left typeError -> output (Msg $ pack $ show typeError) + Right typ -> do + let v = fromDeBruijn $ eval (toDeBruijn term) + output (Evaluated v typ) + +handleCommand :: + (MonadCatch m, MonadREPL m) => + Command -> + m () +handleCommand ClearEnv = getEnv >>= \e -> setEnv (e{env = newEnv, context = newContext}) +handleCommand DumpEnv = + getEnv >>= \REPLEnv{..} -> + output (CurrentEnv env context) +handleCommand (Load (File file)) = do + t <- load file + case t of + Left err -> output (Msg $ pack $ show err) + Right prog -> loadProgramInEnv prog +handleCommand (Load (Data prog)) = loadProgramInEnv prog +handleCommand (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e{stepTypeCheck = st}) +handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e{debugParser = st}) +handleCommand Help = + output (Msg helpText) + +loadProgramInEnv :: + (MonadCatch m, MonadREPL m) => + Text -> + m () +loadProgramInEnv prog = undefined -- do +-- repl@REPLEnv{rho = ρ, gamma = γ, debugParser} <- getEnv +-- case runParser program (ParserState debugParser) "" (unpack prog) of +-- Left err -> output (Msg $ pack $ show err) +-- Right e -> +-- ( do +-- (ρ', γ') <- loadProgram e ρ γ +-- setEnv (repl{rho = ρ', gamma = γ'}) +-- output (Msg makeMessage) +-- ) +-- `catch` \(TypingError err) -> output (Msg err) +-- where +-- makeMessage = +-- "Loaded \"" +-- <> ( if Text.length prog > 15 +-- then Text.take 15 prog <> "..." +-- else prog +-- ) +-- <> "\"" diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs new file mode 100644 index 0000000..383987b --- /dev/null +++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs @@ -0,0 +1,125 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE ViewPatterns #-} + +module Minilang.REPL.Types where + +import Control.Exception (Exception) +import Data.Aeson (FromJSON, ToJSON) +import Data.Text as Text hiding (replicate) +import GHC.Generics +import Minilang.Lambda.Eval (Env, Term, newEnv) +import Minilang.Lambda.Infer (Context, newContext) +import Minilang.Lambda.Unify (Type) + +class (Monad m) => MonadREPL m where + -- | Returns the current environment for this session + -- Environment is made of an `Env`ironment binding names to `Decl`arations + -- and typing `Context` binding names to `Value`s denoting evaluated types. + getEnv :: m REPLEnv + + -- | Updates the current environment for this session. + setEnv :: REPLEnv -> m () + + -- | Handle some input, parsing, typechecking and possibly evaluating it. + input :: m In + + -- | Produces some output + output :: Out -> m () + + -- | Prompt for some input + prompt :: m () + + -- | Read given file + load :: Text -> m (Either REPLError Text) + +-- | Possible error in REPL interactions +data REPLError + = FileError IOError + | REPLError Text + deriving (Eq, Show) + +instance Exception REPLError + +-- | REPL state +data REPLEnv = REPLEnv + { env :: Env, + context :: Context, + curIndent :: Int, + stepTypeCheck :: Bool, + debugParser :: Bool + } + +initialREPL :: REPLEnv +initialREPL = REPLEnv newEnv newContext 0 False False + +-- | Input +data In + = EOF + | In Text + | Com Command + deriving (Eq, Show, Generic, ToJSON, FromJSON) + +data Command + = ClearEnv + | DumpEnv + | Set Flag + | Load Content + | Help + deriving (Eq, Show, Generic, ToJSON, FromJSON) + +data Content + = File Text + | Data Text + deriving (Eq, Show, Generic, ToJSON, FromJSON) + +data Out + = Defined Text Term + | Evaluated Term Type + | CurrentEnv Env Context + | Msg Text + | Bye + deriving (Eq, Show, Generic) + +data Flag + = StepTypeChecker Bool + | DebugParser Bool + deriving (Eq, Show, Generic, ToJSON, FromJSON) + +-- | "Parse" given `Text` into some input for the REPL +interpret :: + Text -> In +interpret ":q" = EOF +interpret ":quit" = EOF +interpret ":h" = Com Help +interpret ":help" = Com Help +interpret ":e" = Com DumpEnv +interpret ":env" = Com DumpEnv +interpret ":c" = Com ClearEnv +interpret ":clear" = Com ClearEnv +interpret ":set step" = Com $ Set $ StepTypeChecker True +interpret ":unset step" = Com $ Set $ StepTypeChecker False +interpret ":set debug" = Com $ Set $ DebugParser True +interpret ":unset debug" = Com $ Set $ DebugParser False +interpret (unpack -> (':' : 'l' : ' ' : file)) = Com $ Load $ File $ strip $ pack file +interpret (unpack -> (':' : 'l' : 'o' : 'a' : 'd' : ' ' : file)) = Com $ Load $ File $ strip $ pack file +interpret t = In t + +helpText :: Text +helpText = + Text.unlines + [ "REPL Commands Help:", + " :h(elp) : Display this help", + " :q(uit) : Exit the interpreter", + " :e(nv) : Displays the current interpreter's environment", + " This dumps both the Environment, where values are defined,", + " and the typing Context, where types are defined. ", + " :c(lear) : Clear the current interpreter's environment", + " :set <option> : Set an option modifying the interpreter's behaviour", + " :unset <option> : Remove an option that's been set previously", + " :l(oad) <file> : load content of <file> into the interpreter, parsing and type-checking it", + "", + "Options: ", + " step : Run the typechecker step-by-step, pausing at each rule application and", + " waiting for user to hit <enter> key to continue", + " debug : Debug parser, displaying the trail of rules tried and triggered" + ] diff --git a/lambda-calcul/haskell/test/Minilang/IOSpec.hs b/lambda-calcul/haskell/test/Minilang/IOSpec.hs index 80cda6c..f000f0a 100644 --- a/lambda-calcul/haskell/test/Minilang/IOSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/IOSpec.hs @@ -27,7 +27,7 @@ spec = parallel $ out <- readFile outputFileName - out `shouldBe` "V \"z\"\n" + out `shouldBe` "z" withTempFile :: (String -> IO ()) -> IO () withTempFile = diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs index ef8903c..cff047d 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs @@ -1,8 +1,10 @@ +{-# LANGUAGE TypeApplications #-} module Minilang.Lambda.DeBruijnSpec where import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn) import qualified Minilang.Lambda.Eval as Eval import Test.Hspec (Spec, it, shouldBe) +import Data.Text (Text) spec :: Spec spec = do @@ -10,9 +12,9 @@ spec = do let term = Eval.Lam "x" (Eval.Lam "y" (Eval.Var "x")) deBruijn = toDeBruijn term - deBruijn `shouldBe` Lam (Lam (Var 1)) + deBruijn `shouldBe` Lam "x" (Lam "y" (Var "x" 1)) it "evaluates deBruijn term" $ do - let term = App (App (Lam (Lam (Var 1))) (Var 12)) (Var 34) + let term = App (App (Lam "x" (Lam "y" (Var "x" 1))) (FV "z")) (FV "t") - eval term `shouldBe` Var 12 + eval @Text term `shouldBe` FV "z" diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs index 718b46d..89e86b9 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs @@ -2,51 +2,52 @@ module Minilang.Lambda.EvalSpec (spec) where import Control.Concurrent (threadDelay) import Control.Concurrent.Async (race_) -import Minilang.Lambda.Eval (Term (..), Value (..), eval, evalNeed) -import Test.Hspec (Spec, describe, it, shouldBe) +import Minilang.Lambda.Eval (Term (..), eval, evalNeed) +import Test.Hspec (Spec, describe, it, pending, shouldBe) spec :: Spec -spec = do - let fix = - Lam - "f" - ( App - (Lam "x" (App (Var "f") (App (Var "x") (Var "x")))) - (Lam "x" (App (Var "f") (App (Var "x") (Var "x")))) - ) - let omega = App fix fix - let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z") - let fst' = Lam "x" (Lam "y" (Var "x")) +spec = it "evaluates Term" pending - describe "call-by-value eval" $ do - it "evaluates 'x' as itself" $ do - let term = Var "x" - eval term [] `shouldBe` V "x" - it "evaluates '((λ x. x) y)' as 'y'" $ do - let term = App (Lam "x" (Var "x")) (Var "y") - eval term [] `shouldBe` V "y" - it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do - let snd' = Lam "x" (Lam "y" (Var "y")) - let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y") - eval term [] `shouldBe` Ap (V "t") (V "y") - it "evaluates '((λ x y. x) z t)' as 'z'" $ do - let term = App (App fst' (Var "z")) (Var "t") - eval term [] `shouldBe` V "z" - it "diverges on evaluating argument bound to ω" $ - shouldDiverge $ - eval term [] +-- let fix = +-- Lam +-- "f" +-- ( App +-- (Lam "x" (App (Var "f") (App (Var "x") (Var "x")))) +-- (Lam "x" (App (Var "f") (App (Var "x") (Var "x")))) +-- ) +-- let omega = App fix fix +-- let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z") +-- let fst' = Lam "x" (Lam "y" (Var "x")) - describe "call-by-need eval" $ do - it "evaluates 'x' as itself" $ do - evalNeed (Var "x") [] `shouldBe` V "x" - it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do - evalNeed term [] `shouldBe` V "z" - it "diverges on evaluating ω" $ - shouldDiverge $ - evalNeed omega [] +-- describe "call-by-value eval" $ do +-- it "evaluates 'x' as itself" $ do +-- let term = Var "x" +-- eval term [] `shouldBe` V "x" +-- it "evaluates '((λ x. x) y)' as 'y'" $ do +-- let term = App (Lam "x" (Var "x")) (Var "y") +-- eval term [] `shouldBe` V "y" +-- it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do +-- let snd' = Lam "x" (Lam "y" (Var "y")) +-- let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y") +-- eval term [] `shouldBe` Ap (V "t") (V "y") +-- it "evaluates '((λ x y. x) z t)' as 'z'" $ do +-- let term = App (App fst' (Var "z")) (Var "t") +-- eval term [] `shouldBe` V "z" +-- it "diverges on evaluating argument bound to ω" $ +-- shouldDiverge $ +-- eval term [] -shouldDiverge :: Value -> IO () -shouldDiverge t = - race_ - (t `seq` fail "Did not diverge") - (threadDelay 1000000) +-- describe "call-by-need eval" $ do +-- it "evaluates 'x' as itself" $ do +-- evalNeed (Var "x") [] `shouldBe` V "x" +-- it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do +-- evalNeed term [] `shouldBe` V "z" +-- it "diverges on evaluating ω" $ +-- shouldDiverge $ +-- evalNeed omega [] + +-- shouldDiverge :: Value -> IO () +-- shouldDiverge t = +-- race_ +-- (t `seq` fail "Did not diverge") +-- (threadDelay 1000000) diff --git a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs new file mode 100644 index 0000000..b7ca5c9 --- /dev/null +++ b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs @@ -0,0 +1,33 @@ +module Minilang.REPL.HaskelineSpec where + +import Minilang.REPL.Haskeline +import System.Console.Haskeline.Completion +import Test.Hspec +import Prelude hiding + ( lines, + readFile, + writeFile, + ) + +spec :: Spec +spec = parallel $ describe "MiniLang Haskeline REPL" $ do + describe "Completion" $ do + it "returns all commands when input ':' " $ do + (fmap replacement) . snd <$> completion (":", "") + `shouldReturn` [":quit", ":env", ":clear", ":load", ":set", ":unset", ":help"] + + it "returns sub-commands when input ':set' " $ do + (fmap replacement) . snd <$> completion ("tes:", "") + `shouldReturn` [":set step", ":set debug"] + + it "returns sub-commands when input ':unset' " $ do + (fmap replacement) . snd <$> completion ("tesnu:", "") + `shouldReturn` [":unset step", ":unset debug"] + + it "returns list of files when input ':load' " $ do + (fmap replacement) . snd <$> completion ("daol:", "") + `shouldReturn` [":load bool.mtt", ":load nelist.mtt", ":load vector.mtt", ":load indrec.mtt"] + + it "returns filtered list of files when input ':load xxx' " $ do + (fmap replacement) . snd <$> completion ("v daol:", "") + `shouldReturn` [":load vector.mtt"] diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs new file mode 100644 index 0000000..e134810 --- /dev/null +++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs @@ -0,0 +1,74 @@ +module Minilang.REPLSpec where + +import Control.Exception (bracket) +import Data.Text.IO +import Minilang.Lambda.Eval (Term (Var)) +import Minilang.REPL +import Minilang.REPL.Purer +import Minilang.REPL.Types +import System.Directory (getTemporaryDirectory, removeFile) +import System.FilePath ((<.>), (</>)) +import System.IO (IOMode (..), hClose, withFile) +import System.Posix.Temp (mkstemp) +import Test.Hspec +import Prelude hiding (lines, readFile, writeFile) + +spec :: Spec +spec = parallel $ + describe "MiniLang REPL" $ do + it "evaluates MiniLang terms read from pure Monad" $ do + let out = + withInput + [ "rec Nat : U = Sum (zero | succ Nat);", + "id : Π A : U . Π _ : A . A = λ A . λ x . x;", + "id Nat (succ (succ (succ zero)))" + ] + + out + `shouldBe` [ "Bye!", + "$succ $succ $succ $zero : Sum(zero| succ Nat)", + "defined id : Π A : U . A → A", + "defined Nat : U" + ] + + it "shows error when trying to load a non-existent file" $ do + withInput [":load foo"] + `shouldBe` [ "Bye!", + "REPLError \"cannot load file foo in Pure interpreter\"" + ] + + around withTempFile $ + it "evaluates single MiniLang term read from IO" $ \fileName -> do + let outputFileName = fileName <> ".out" + + writeFile fileName "rec Nat : U = Sum (zero | succ Nat);\nid : Π A : U . Π _ : A . A = λ A . λ x . x;\nid Nat (succ (succ (succ zero)))" + + _ <- withFile fileName ReadMode $ \hin -> + withFile outputFileName AppendMode $ \hout -> + withHandles hin hout + + out <- readFile outputFileName + + out + `shouldBe` "\955\928> defined Nat : U\n\955\928> defined id : \928 A : U . A \8594 A\n\955\928> succ succ succ zero : Sum(zero| succ Nat)\n\955\928> Bye!\n" + + describe "Purer REPL" $ do + it "keeps handling Inputs even when they fail" $ do + let inputs = + [ In "Unit : U", + In "Unit : U = Sum(tt)", + Com DumpEnv + ] + + env (purerREPL (withInputs initialREPL inputs)) + `shouldBe` [("Unit", Var "x")] + + outputs (withInputs initialREPL inputs) + `shouldContain` [Msg "cannot find \"Unit\" in empty context"] + +withTempFile :: (String -> IO ()) -> IO () +withTempFile = + bracket mkTempFile rmTempFile + where + mkTempFile = getTemporaryDirectory >>= \dir -> mkstemp (dir </> "test-repl") >>= \(fp, h) -> hClose h >> pure fp + rmTempFile fn = removeFile fn >> removeFile (fn <.> "out") |