wip: port REPL from minilang

6 files changed, 441 insertions, 0 deletions

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