summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/REPL
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/REPL')
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Pure.hs21
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Run.hs50
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Types.hs58
3 files changed, 67 insertions, 62 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
index 8250152..d9dbbbe 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
@@ -13,9 +13,9 @@ import qualified Minilang.Lambda.Unify as Type
import Minilang.REPL.Types
data PureEnv = PureEnv
- { inputText :: [Text],
- outputText :: [Text],
- pureREPL :: REPLEnv
+ { inputText :: [Text]
+ , outputText :: [Text]
+ , pureREPL :: REPLEnv
}
newtype PureREPL a = PureREPL {runPure :: CatchT (State PureEnv) a}
@@ -26,25 +26,30 @@ instance MonadREPL PureREPL where
ins <- gets inputText
case ins of
[] -> pure EOF
- (t : ts) -> modify (\e -> e {inputText = ts}) >> pure (interpret t)
+ (t : ts) -> modify (\e -> e{inputText = ts}) >> pure (interpret t)
- output t = modify $ \e -> e {outputText = render t : outputText e}
+ output t = modify $ \e -> e{outputText = render t : outputText e}
prompt = pure ()
getEnv = gets pureREPL
- setEnv e' = modify $ \e -> e {pureREPL = e'}
+ 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
- Evaluated ast _term typ -> pretty ast <> " : " <> Type.pretty typ
- Defined ident typ -> ident <> " : " <> Type.pretty typ
+ Evaluated ast _term typ -> pretty ast <> renderType typ
+ Defined ident typ -> ident <> renderType typ
Bye -> "Bye!"
other -> pack (show other)
+renderType :: Maybe Type.Type -> Text
+renderType typ = case typ of
+ Nothing -> ""
+ Just t -> " : " <> Type.pretty t
+
instance MonadThrow PureREPL where
throwM = throw
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index 26f3cad..ba09007 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -8,7 +8,7 @@ module Minilang.REPL.Run where
import Control.Monad.Catch
import Data.Text hiding (replicate)
-import Minilang.Lambda (loadProgram, evalInEnvWith)
+import Minilang.Lambda (evalInEnvWith, loadProgram)
import Minilang.Lambda.Eval (newEnv)
import Minilang.Lambda.Infer (extendContext, infer, newContext)
import qualified Minilang.Lambda.Infer as Infer
@@ -20,21 +20,21 @@ import Minilang.REPL.Types
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
+ 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 {language, evaluator, env, context} <- getEnv
+ repl@REPLEnv{language, evaluator, env, context} <- getEnv
case parse txt of
Left err -> output (Msg $ pack $ show err)
Right (Def ident body) -> do
@@ -46,13 +46,13 @@ handleUserInput txt = do
Right typ -> do
setEnv $
repl
- { env = (ident, v) : env,
- context = extendContext ident typ context
+ { env = (ident, v) : env
+ , context = extendContext ident typ context
}
- output (Defined ident typ)
+ output (Defined ident (Just typ))
Untyped -> do
- setEnv $ repl {env = (ident, v) : env}
- output (Defined ident (TyVar "<?>"))
+ setEnv $ repl{env = (ident, v) : env}
+ output (Defined ident Nothing)
Right expr -> do
let v = evalInEnvWith evaluator env expr
ast = resugar v
@@ -62,17 +62,17 @@ handleUserInput txt = do
Left typeError -> output (Msg $ Infer.render typeError)
Right typ -> do
let
- output (Evaluated ast v typ)
+ output (Evaluated ast v (Just typ))
Untyped ->
- output (Evaluated ast v (TyVar "<?>"))
+ output (Evaluated ast v Nothing)
handleCommand ::
(MonadCatch m, MonadREPL m) =>
Command ->
m ()
-handleCommand ClearEnv = getEnv >>= \e -> setEnv (e {env = newEnv, context = newContext})
+handleCommand ClearEnv = getEnv >>= \e -> setEnv (e{env = newEnv, context = newContext})
handleCommand DumpEnv =
- getEnv >>= \REPLEnv {..} ->
+ getEnv >>= \REPLEnv{..} ->
output (CurrentEnv env context language)
handleCommand (Load (File file)) = do
t <- load file
@@ -80,15 +80,15 @@ handleCommand (Load (File file)) = do
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 (Set (StepTypeChecker st)) = getEnv >>= \e -> setEnv (e{stepTypeCheck = st})
+handleCommand (Set (DebugParser st)) = getEnv >>= \e -> setEnv (e{debugParser = st})
handleCommand (Set (SelectLanguage lang)) =
getEnv >>= \e ->
- setEnv (e {language = lang})
+ setEnv (e{language = lang})
>> output (Msg $ "Language set to " <> pack (show lang))
handleCommand (Set (SelectEvaluator ev)) =
getEnv >>= \e ->
- setEnv (e {evaluator = ev})
+ setEnv (e{evaluator = ev})
>> output (Msg $ "Evaluator set to " <> pack (show ev))
handleCommand Help =
output (Msg helpText)
@@ -98,12 +98,12 @@ loadProgramInEnv ::
Text ->
m ()
loadProgramInEnv prog = do
- repl@REPLEnv {env, context, language, evaluator} <- getEnv
+ repl@REPLEnv{env, context, language, evaluator} <- getEnv
case parseProgram prog of
Left err -> output (Msg $ pack $ show err)
Right exprs -> do
case loadProgram evaluator language env context exprs of
Left typeError -> output (Msg $ pack $ show typeError)
Right (results, env', context') -> do
- setEnv (repl {env = env', context = context'})
+ setEnv (repl{env = env', context = context'})
mapM_ (\(term, typ) -> output (Evaluated (resugar term) term typ)) results
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index 0b0472e..3bcbbb1 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -7,13 +7,13 @@ import Control.Exception (Exception)
import Data.Aeson (FromJSON, ToJSON)
import Data.Text as Text hiding (replicate)
import GHC.Generics
-import Minilang.Lambda.Eval (Term, Env, newEnv)
+import Minilang.Lambda.Eval (Env, Term, newEnv)
import Minilang.Lambda.Infer (Context, newContext)
import Minilang.Lambda.Parser (AST)
import Minilang.Lambda.Unify (Type)
import Text.Read (readMaybe)
-class (Monad m) => MonadREPL m where
+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.
@@ -44,13 +44,13 @@ instance Exception REPLError
-- | REPL state
data REPLEnv = REPLEnv
- { env :: Env,
- context :: Context,
- curIndent :: Int,
- stepTypeCheck :: Bool,
- debugParser :: Bool,
- language :: Language,
- evaluator :: Evaluator
+ { env :: Env
+ , context :: Context
+ , curIndent :: Int
+ , stepTypeCheck :: Bool
+ , debugParser :: Bool
+ , language :: Language
+ , evaluator :: Evaluator
}
initialREPL :: REPLEnv
@@ -77,8 +77,8 @@ data Content
deriving (Eq, Show, Generic, ToJSON, FromJSON)
data Out
- = Defined Text Type
- | Evaluated AST Term Type
+ = Defined Text (Maybe Type)
+ | Evaluated AST Term (Maybe Type)
| CurrentEnv Env Context Language
| Msg Text
| Bye
@@ -128,27 +128,27 @@ interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) =
case readMaybe ev of
Nothing -> Com Help
- Just e -> Com $ Set $ SelectEvaluator e
+ Just e -> Com $ Set $ SelectEvaluator e
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",
- " :lang <Language> : Switch type-checking language (Untyped | Typed)",
- " :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)",
- "",
- "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"
+ [ "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"
+ , " :lang <Language> : Switch type-checking language (Untyped | Typed)"
+ , " :eval <Evaluator>: Switch reduction strategy (DeBruijn | NbE)"
+ , ""
+ , "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"
]
generated by cgit v1.3.1 (git 2.54.0) at 2026-10-24 03:32:20 +0000