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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
{-# 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.Parser (AST)
import Minilang.Lambda.Unify (Type)
import Text.Read (readMaybe)
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
, language :: Language
, evaluator :: Evaluator
}
initialREPL :: REPLEnv
initialREPL = REPLEnv newEnv newContext 0 False False Untyped DeBruijn
-- | 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 (Maybe Type)
| Evaluated AST Term (Maybe Type)
| CurrentEnv Env Context Language
| Msg Text
| Bye
deriving (Eq, Show, Generic, ToJSON, FromJSON)
data Flag
= StepTypeChecker Bool
| DebugParser Bool
| SelectLanguage Language
| SelectEvaluator Evaluator
deriving (Eq, Show, Generic, ToJSON, FromJSON)
data Language = Untyped | Typed
deriving (Eq, Show, Read, Generic, ToJSON, FromJSON)
-- | Which reduction strategy to use.
--
-- * 'DeBruijn' — call-by-value head reduction on De Bruijn-indexed terms
-- (the original evaluator).
-- * 'NbE' — Normalisation by Evaluation: eval to a 'Value' semantic domain,
-- then read back to a 'Term'. Reduces under lambda binders and therefore
-- produces fully-normalised terms.
data Evaluator = DeBruijn | NbE
deriving (Eq, Show, Read, 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 (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) =
case readMaybe lang of
Nothing -> Com Help
Just l -> Com $ Set $ SelectLanguage l
interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) =
case readMaybe ev of
Nothing -> Com Help
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"
]
|
