wip: port REPL from minilang

17 files changed, 712 insertions, 91 deletions

diff --git a/lambda-calcul/haskell/app/Main.hs b/lambda-calcul/haskell/app/Main.hs
index 5b48c01..0b40f60 100644
--- a/lambda-calcul/haskell/app/Main.hs
+++ b/lambda-calcul/haskell/app/Main.hs
@@ -1,6 +1,12 @@
-import Minilang.IO
+import Minilang.IO (runEval)
 import System.IO (stdin, stdout)
+import System.Posix.Terminal (queryTerminal)
+import System.Posix (stdInput)
+import Minilang.REPL (withTerminal)
 
 main :: IO ()
-main =
-  runEval stdin stdout
+main = do
+  hasTty <- queryTerminal stdInput
+  if hasTty
+    then withTerminal
+    else runEval stdin stdout
diff --git a/lambda-calcul/haskell/minilang.cabal b/lambda-calcul/haskell/minilang.cabal
index a2bb355..039e4f0 100644
--- a/lambda-calcul/haskell/minilang.cabal
+++ b/lambda-calcul/haskell/minilang.cabal
@@ -31,6 +31,13 @@ library
       Minilang.Lambda.Eval
       Minilang.Lambda.Infer
       Minilang.Lambda.Parser
+      Minilang.REPL
+      Minilang.REPL.Haskeline
+      Minilang.REPL.IO
+      Minilang.REPL.Pure
+      Minilang.REPL.Purer
+      Minilang.REPL.Run
+      Minilang.REPL.Types
   hs-source-dirs:
       src
   default-extensions:
@@ -48,16 +55,21 @@ library
     , async
     , base
     , bytestring
+    , cereal
     , containers
     , data-default
     , directory
     , exceptions
     , filepath
+    , haskeline
     , megaparsec
     , mtl
     , stm
     , text
     , unordered-containers
+    , wai
+    , websockets
+    , wai-websockets
   default-language: Haskell2010
 
 test-suite minilang-test
@@ -69,6 +81,8 @@ test-suite minilang-test
       Minilang.Lambda.DeBruijnSpec
       Minilang.Lambda.EvalSpec
       Minilang.Lambda.ParserSpec
+      Minilang.REPLSpec
+      Minilang.REPL.HaskelineSpec
   hs-source-dirs:
       test
   default-extensions:
@@ -93,6 +107,7 @@ test-suite minilang-test
     , directory
     , exceptions
     , filepath
+    , haskeline
     , hspec
     , hspec-discover
     , minilang
@@ -122,4 +137,5 @@ executable lambda
       base
     , containers
     , minilang
+    , unix
   default-language: Haskell2010
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"
+    ]
diff --git a/lambda-calcul/haskell/test/Minilang/IOSpec.hs b/lambda-calcul/haskell/test/Minilang/IOSpec.hs
index 80cda6c..f000f0a 100644
--- a/lambda-calcul/haskell/test/Minilang/IOSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/IOSpec.hs
@@ -27,7 +27,7 @@ spec = parallel $
 
         out <- readFile outputFileName
 
-        out `shouldBe` "V \"z\"\n"
+        out `shouldBe` "z"
 
 withTempFile :: (String -> IO ()) -> IO ()
 withTempFile =
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
index ef8903c..cff047d 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
@@ -1,8 +1,10 @@
+{-# LANGUAGE TypeApplications #-}
 module Minilang.Lambda.DeBruijnSpec where
 
 import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn)
 import qualified Minilang.Lambda.Eval as Eval
 import Test.Hspec (Spec, it, shouldBe)
+import Data.Text (Text)
 
 spec :: Spec
 spec = do
@@ -10,9 +12,9 @@ spec = do
     let term = Eval.Lam "x" (Eval.Lam "y" (Eval.Var "x"))
         deBruijn = toDeBruijn term
 
-    deBruijn `shouldBe` Lam (Lam (Var 1))
+    deBruijn `shouldBe` Lam "x" (Lam "y" (Var "x" 1))
 
   it "evaluates deBruijn term" $ do
-    let term = App (App (Lam (Lam (Var 1))) (Var 12)) (Var 34)
+    let term = App (App (Lam "x" (Lam "y" (Var "x" 1))) (FV "z")) (FV "t")
 
-    eval term `shouldBe` Var 12
+    eval @Text term `shouldBe` FV "z"
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index 718b46d..89e86b9 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -2,51 +2,52 @@ module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), Value (..), eval, evalNeed)
-import Test.Hspec (Spec, describe, it, shouldBe)
+import Minilang.Lambda.Eval (Term (..), eval, evalNeed)
+import Test.Hspec (Spec, describe, it, pending, shouldBe)
 
 spec :: Spec
-spec = do
-  let fix =
-        Lam
-          "f"
-          ( App
-              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
-              (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
-          )
-  let omega = App fix fix
-  let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
-  let fst' = Lam "x" (Lam "y" (Var "x"))
+spec = it "evaluates Term" pending
 
-  describe "call-by-value eval" $ do
-    it "evaluates 'x' as itself" $ do
-      let term = Var "x"
-      eval term [] `shouldBe` V "x"
-    it "evaluates '((λ x. x) y)' as 'y'" $ do
-      let term = App (Lam "x" (Var "x")) (Var "y")
-      eval term [] `shouldBe` V "y"
-    it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
-      let snd' = Lam "x" (Lam "y" (Var "y"))
-      let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
-      eval term [] `shouldBe` Ap (V "t") (V "y")
-    it "evaluates '((λ x y. x) z t)' as 'z'" $ do
-      let term = App (App fst' (Var "z")) (Var "t")
-      eval term [] `shouldBe` V "z"
-    it "diverges on evaluating argument bound to ω" $
-      shouldDiverge $
-        eval term []
+--   let fix =
+--         Lam
+--           "f"
+--           ( App
+--               (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+--               (Lam "x" (App (Var "f") (App (Var "x") (Var "x"))))
+--           )
+--   let omega = App fix fix
+--   let term = App (App (Lam "x" (Lam "y" (Var "y"))) omega) (Var "z")
+--   let fst' = Lam "x" (Lam "y" (Var "x"))
 
-  describe "call-by-need eval" $ do
-    it "evaluates 'x' as itself" $ do
-      evalNeed (Var "x") [] `shouldBe` V "x"
-    it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
-      evalNeed term [] `shouldBe` V "z"
-    it "diverges on evaluating ω" $
-      shouldDiverge $
-        evalNeed omega []
+--   describe "call-by-value eval" $ do
+--     it "evaluates 'x' as itself" $ do
+--       let term = Var "x"
+--       eval term [] `shouldBe` V "x"
+--     it "evaluates '((λ x. x) y)' as 'y'" $ do
+--       let term = App (Lam "x" (Var "x")) (Var "y")
+--       eval term [] `shouldBe` V "y"
+--     it "evaluates '((λ x y. y) z t y)' as '(t y)'" $ do
+--       let snd' = Lam "x" (Lam "y" (Var "y"))
+--       let term = App (App (App snd' (Var "z")) (Var "t")) (Var "y")
+--       eval term [] `shouldBe` Ap (V "t") (V "y")
+--     it "evaluates '((λ x y. x) z t)' as 'z'" $ do
+--       let term = App (App fst' (Var "z")) (Var "t")
+--       eval term [] `shouldBe` V "z"
+--     it "diverges on evaluating argument bound to ω" $
+--       shouldDiverge $
+--         eval term []
 
-shouldDiverge :: Value -> IO ()
-shouldDiverge t =
-  race_
-    (t `seq` fail "Did not diverge")
-    (threadDelay 1000000)
+--   describe "call-by-need eval" $ do
+--     it "evaluates 'x' as itself" $ do
+--       evalNeed (Var "x") [] `shouldBe` V "x"
+--     it "evaluates '(λ x y . y) ⊥ z' as 'z'" $ do
+--       evalNeed term [] `shouldBe` V "z"
+--     it "diverges on evaluating ω" $
+--       shouldDiverge $
+--         evalNeed omega []
+
+-- shouldDiverge :: Value -> IO ()
+-- shouldDiverge t =
+--   race_
+--     (t `seq` fail "Did not diverge")
+--     (threadDelay 1000000)
diff --git a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs
new file mode 100644
index 0000000..b7ca5c9
--- /dev/null
+++ b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs
@@ -0,0 +1,33 @@
+module Minilang.REPL.HaskelineSpec where
+
+import Minilang.REPL.Haskeline
+import System.Console.Haskeline.Completion
+import Test.Hspec
+import Prelude hiding
+  ( lines,
+    readFile,
+    writeFile,
+  )
+
+spec :: Spec
+spec = parallel $ describe "MiniLang Haskeline REPL" $ do
+  describe "Completion" $ do
+    it "returns all commands when input ':' " $ do
+      (fmap replacement) . snd <$> completion (":", "")
+        `shouldReturn` [":quit", ":env", ":clear", ":load", ":set", ":unset", ":help"]
+
+    it "returns sub-commands when input ':set' " $ do
+      (fmap replacement) . snd <$> completion ("tes:", "")
+        `shouldReturn` [":set step", ":set debug"]
+
+    it "returns sub-commands when input ':unset' " $ do
+      (fmap replacement) . snd <$> completion ("tesnu:", "")
+        `shouldReturn` [":unset step", ":unset debug"]
+
+    it "returns list of files when input ':load' " $ do
+      (fmap replacement) . snd <$> completion ("daol:", "")
+        `shouldReturn` [":load bool.mtt", ":load nelist.mtt", ":load vector.mtt", ":load indrec.mtt"]
+
+    it "returns filtered list of files when input ':load xxx' " $ do
+      (fmap replacement) . snd <$> completion ("v daol:", "")
+        `shouldReturn` [":load vector.mtt"]
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
new file mode 100644
index 0000000..e134810
--- /dev/null
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -0,0 +1,74 @@
+module Minilang.REPLSpec where
+
+import Control.Exception (bracket)
+import Data.Text.IO
+import Minilang.Lambda.Eval (Term (Var))
+import Minilang.REPL
+import Minilang.REPL.Purer
+import Minilang.REPL.Types
+import System.Directory (getTemporaryDirectory, removeFile)
+import System.FilePath ((<.>), (</>))
+import System.IO (IOMode (..), hClose, withFile)
+import System.Posix.Temp (mkstemp)
+import Test.Hspec
+import Prelude hiding (lines, readFile, writeFile)
+
+spec :: Spec
+spec = parallel $
+  describe "MiniLang REPL" $ do
+    it "evaluates MiniLang terms read from pure Monad" $ do
+      let out =
+            withInput
+              [ "rec Nat : U = Sum (zero | succ Nat);",
+                "id : Π A : U . Π _ : A . A = λ A . λ x . x;",
+                "id Nat (succ (succ (succ zero)))"
+              ]
+
+      out
+        `shouldBe` [ "Bye!",
+                     "$succ $succ $succ $zero  : Sum(zero| succ Nat)",
+                     "defined id : Π A : U . A → A",
+                     "defined Nat : U"
+                   ]
+
+    it "shows error when trying to load a non-existent file" $ do
+      withInput [":load foo"]
+        `shouldBe` [ "Bye!",
+                     "REPLError \"cannot load file foo in Pure interpreter\""
+                   ]
+
+    around withTempFile $
+      it "evaluates single MiniLang term read from IO" $ \fileName -> do
+        let outputFileName = fileName <> ".out"
+
+        writeFile fileName "rec Nat : U = Sum (zero | succ Nat);\nid : Π A : U . Π _ : A . A = λ A . λ x . x;\nid Nat (succ (succ (succ zero)))"
+
+        _ <- withFile fileName ReadMode $ \hin ->
+          withFile outputFileName AppendMode $ \hout ->
+            withHandles hin hout
+
+        out <- readFile outputFileName
+
+        out
+          `shouldBe` "\955\928> defined Nat : U\n\955\928> defined id : \928 A : U . A \8594 A\n\955\928> succ succ succ zero  : Sum(zero| succ Nat)\n\955\928> Bye!\n"
+
+    describe "Purer REPL" $ do
+      it "keeps handling Inputs even when they fail" $ do
+        let inputs =
+              [ In "Unit : U",
+                In "Unit : U = Sum(tt)",
+                Com DumpEnv
+              ]
+
+        env (purerREPL (withInputs initialREPL inputs))
+          `shouldBe` [("Unit", Var "x")]
+
+        outputs (withInputs initialREPL inputs)
+          `shouldContain` [Msg "cannot find \"Unit\" in empty context"]
+
+withTempFile :: (String -> IO ()) -> IO ()
+withTempFile =
+  bracket mkTempFile rmTempFile
+  where
+    mkTempFile = getTemporaryDirectory >>= \dir -> mkstemp (dir </> "test-repl") >>= \(fp, h) -> hClose h >> pure fp
+    rmTempFile fn = removeFile fn >> removeFile (fn <.> "out")