summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/haskell/src')
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Pure.hs1
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Run.hs22
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Types.hs6
3 files changed, 22 insertions, 7 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
index 7ca0c85..8250152 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Pure.hs
@@ -42,6 +42,7 @@ render :: Out -> Text
render = \case
Msg t -> t
Evaluated ast _term typ -> pretty ast <> " : " <> Type.pretty typ
+ Defined ident typ -> ident <> " : " <> Type.pretty typ
Bye -> "Bye!"
other -> pack (show other)
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index bc552cb..a98ff41 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -7,13 +7,14 @@
module Minilang.REPL.Run where
import Control.Monad.Catch
+import Data.Bifunctor (second)
import Data.Text hiding (replicate)
import Minilang.Lambda (loadProgram)
-import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn)
+import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn)
import Minilang.Lambda.Eval (newEnv)
import Minilang.Lambda.Infer (infer, newContext)
import qualified Minilang.Lambda.Infer as Infer
-import Minilang.Lambda.Parser (desugar, parse, resugar)
+import Minilang.Lambda.Parser (AST (..), desugar, parse, resugar)
import Minilang.Lambda.Unify (Type (TyVar))
import Minilang.REPL.Types
@@ -35,12 +36,25 @@ handleUserInput ::
Text ->
m ()
handleUserInput txt = do
- REPLEnv {language} <- getEnv
+ repl@REPLEnv {language, env} <- getEnv
case parse txt of
Left err -> output (Msg $ pack $ show err)
+ Right (Def ident body) -> do
+ let term = desugar body
+ case language of
+ Typed ->
+ case infer term of
+ Left typeError -> output (Msg $ Infer.render typeError)
+ Right typ -> do
+ setEnv $ repl {env = (ident, term) : env}
+ output (Defined ident typ)
+ Untyped -> do
+ setEnv $ repl {env = (ident, term) : env}
+ output (Defined ident (TyVar "<?>"))
Right expr -> do
let term = desugar expr
- v = fromDeBruijn $ eval (toDeBruijn term)
+ env' = second toDeBruijn <$> env
+ v = fromDeBruijn $ eval' env' (toDeBruijn term)
ast = resugar v
case language of
Typed ->
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index b7a324b..baa59ff 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -7,11 +7,11 @@ 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.Eval (Term, Env, newEnv)
import Minilang.Lambda.Infer (Context, newContext)
+import Minilang.Lambda.Parser (AST)
import Minilang.Lambda.Unify (Type)
import Text.Read (readMaybe)
-import Minilang.Lambda.Parser (AST)
class (Monad m) => MonadREPL m where
-- | Returns the current environment for this session
@@ -76,7 +76,7 @@ data Content
deriving (Eq, Show, Generic, ToJSON, FromJSON)
data Out
- = Defined Text Term
+ = Defined Text Type
| Evaluated AST Term Type
| CurrentEnv Env Context Language
| Msg Text