1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
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
-- )
-- <> "\""
|
