Remove answers from sent challenges

Also fix integration test

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"
     ]