diff options
Diffstat (limited to 'lambda-calcul/haskell/src')
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs | 36 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs | 24 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs | 11 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL.hs | 59 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Haskeline.hs | 118 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/IO.hs | 36 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Pure.hs | 42 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Purer.hs | 31 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 89 | ||||
| -rw-r--r-- | lambda-calcul/haskell/src/Minilang/REPL/Types.hs | 125 |
10 files changed, 530 insertions, 41 deletions
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" + ] |