allow to run untyped evaluator

3 files changed, 40 insertions, 9 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
index 9c31987..2282b46 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs
@@ -14,9 +14,10 @@ import Minilang.Lambda (loadProgram)
 import Minilang.Lambda.DeBruijn (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)
+import Minilang.Lambda.Unify (Type (TyVar))
 import Minilang.REPL.Types
-import qualified Minilang.Lambda.Infer as Infer
 
 -- | Run a REPL session
 runREPL ::
@@ -36,16 +37,21 @@ handleUserInput ::
   Text ->
   m ()
 handleUserInput txt = do
-  -- repl@REPLEnv {env, context, debugParser} <- getEnv
+  REPLEnv {language} <- 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 $ Infer.render typeError)
-        Right typ -> do
-          let v = fromDeBruijn $ eval (toDeBruijn term)
-          output (Evaluated v typ)
+          v = fromDeBruijn $ eval (toDeBruijn term)
+      case language of
+        Typed ->
+          case infer term of
+            Left typeError -> output (Msg $ Infer.render typeError)
+            Right typ -> do
+              let
+              output (Evaluated v typ)
+        Untyped ->
+          output (Evaluated v (TyVar "<?>"))
 
 handleCommand ::
   (MonadCatch m, MonadREPL m) =>
@@ -63,6 +69,7 @@ handleCommand (Load (File file)) = do
 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 (SelectLanguage lang)) = getEnv >>= \e -> setEnv (e {language = lang})
 handleCommand Help =
   output (Msg helpText)
 
diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
index 3a82018..4e19c72 100644
--- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
+++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs
@@ -10,6 +10,7 @@ import GHC.Generics
 import Minilang.Lambda.Eval (Env, Term, newEnv)
 import Minilang.Lambda.Infer (Context, newContext)
 import Minilang.Lambda.Unify (Type)
+import Text.Read (readMaybe)
 
 class (Monad m) => MonadREPL m where
   -- | Returns the current environment for this session
@@ -46,11 +47,12 @@ data REPLEnv = REPLEnv
     context :: Context,
     curIndent :: Int,
     stepTypeCheck :: Bool,
-    debugParser :: Bool
+    debugParser :: Bool,
+    language :: Language
   }
 
 initialREPL :: REPLEnv
-initialREPL = REPLEnv newEnv newContext 0 False False
+initialREPL = REPLEnv newEnv newContext 0 False False Typed
 
 -- | Input
 data In
@@ -83,8 +85,12 @@ data Out
 data Flag
   = StepTypeChecker Bool
   | DebugParser Bool
+  | SelectLanguage Language
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
+data Language = Untyped | Typed
+  deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)
+
 -- | "Parse" given `Text` into some input for the REPL
 interpret ::
   Text -> In
@@ -102,6 +108,10 @@ 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 (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
+  case readMaybe lang of
+    Nothing -> Com Help
+    Just l -> Com $ Set $ SelectLanguage l
 interpret t = In t
 
 helpText :: Text
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
index f6279c1..d23ffbd 100644
--- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -36,6 +36,20 @@ spec = parallel $
                      "Cannot unify type variable f with type (e -> f -> e) -> e due to circularity: The variable already occurs in the type."
                    ]
 
+    it "do not typecheck term when language is set to 'untyped'" $ do
+      let out =
+            withInput
+              [ ":lang    Untyped",
+                "(let ((Succ (lam (n z s) (s n))) \
+                \ (Zero (lam (z s) z))) \
+                \ (Succ (Succ Zero)))"
+              ]
+
+      out
+        `shouldBe` [ "Bye!",
+                     "(lam (z s) (s ((lam (n z s) (s n)) (lam (z s) z)))) : <?>"
+                   ]
+
     it "shows error when trying to load a non-existent file" $ do
       withInput [":load foo"]
         `shouldBe` [ "Bye!",