/
Main.hs
304 lines (268 loc) · 12.5 KB
/
Main.hs
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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{- | A Plutus Core debugger TUI application.
The application has two stages: browsing for files to debug, and debugging.
If the argument is a directory, it enters the browsing stage.
If the argument is a file, it enters the debugging stage.
If no argument is provided, it defaults to the current working directory.
-}
module Main (main) where
import PlutusCore qualified as PLC
import PlutusCore.Error
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Executable.Common
import PlutusCore.Executable.Parsers
import PlutusCore.Pretty qualified as PLC
import UntypedPlutusCore as UPLC
import UntypedPlutusCore.Core.Zip
import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Evaluation.Machine.Cek.Debug.Driver qualified as D
import UntypedPlutusCore.Evaluation.Machine.Cek.Debug.Internal
import UntypedPlutusCore.Evaluation.Machine.Cek.StepCounter (newCounter)
import UntypedPlutusCore.Parser qualified as UPLC
import Draw
import Event
import Types
import Brick.AttrMap qualified as B
import Brick.BChan qualified as B
import Brick.Focus qualified as B
import Brick.Main qualified as B
import Brick.Util qualified as B
import Brick.Widgets.Edit qualified as BE
import Control.Concurrent
import Control.Monad.Except
import Control.Monad.ST (RealWorld)
import Data.Coerce
import Data.Maybe
import Data.Text (Text)
import Data.Text.IO qualified as Text
import Data.Traversable
import GHC.IO (stToIO)
import Graphics.Vty qualified as Vty
import Lens.Micro
import Options.Applicative qualified as OA
import Text.Megaparsec as MP
import Text.Megaparsec.Char as MP
import Text.Megaparsec.Char.Lexer as MP
{- NOTE [Budgeting implementation for the debugger]
To retrieve the budget(s) (spent and remaining), we cannot simply
rely on `CekState`: the debuggable version of CEK tries to closely match the original CEK and
so it also inherits its pluggable spenders/emitters approach. Thus, for the debugger as well
we need to construct a budget mode (incl. a spender function) so we can have proper
budget accounting.
We could go with implementing a custom budget mode specifically for the
debugger (e.g. one that can talk directly to brick via events), but we opted instead to reuse
the `counting` and `restricting` modes, already built for the original cek.
-}
debuggerAttrMap :: B.AttrMap
debuggerAttrMap =
B.attrMap
Vty.defAttr
[ (BE.editAttr, Vty.white `B.on` Vty.rgbColor @Int 32 32 32)
, (BE.editFocusedAttr, Vty.white `B.on` Vty.black)
, (menuAttr, Vty.withStyle (Vty.white `B.on` darkGreen) Vty.bold)
, (highlightAttr, Vty.blue `B.on` Vty.white)
]
darkGreen :: Vty.Color
darkGreen = Vty.rgbColor @Int 0 100 0
data Options = Options
{ optUplcInput :: Input
, optUplcInputFormat :: Format
, optHsPath :: Maybe FilePath
, optBudgetLim :: Maybe ExBudget
}
parseOptions :: OA.Parser Options
parseOptions = do
optUplcInput <- input
optUplcInputFormat <- inputformat
optHsPath <- OA.optional $ OA.strOption $
mconcat
[ OA.metavar "HS_FILE"
, OA.long "hs-file"
, OA.help "HS File"
]
-- Having cpu mem as separate options complicates budget modes (counting vs restricting);
-- instead opt for having both present (cpu,mem) or both missing.
optBudgetLim <- OA.optional $ OA.option budgetReader $
mconcat
[ OA.metavar "INT,INT"
, OA.long "budget"
, OA.help "Limit the execution budget, given in terms of CPU,MEMORY"
]
pure Options{optUplcInput, optUplcInputFormat, optHsPath, optBudgetLim}
where
budgetReader = OA.maybeReader $ MP.parseMaybe @() budgetParser
budgetParser = ExBudget <$> MP.decimal <* MP.char ',' <*> MP.decimal
main :: IO ()
main = do
Options{optUplcInput, optUplcInputFormat, optHsPath, optBudgetLim} <-
OA.execParser $
OA.info
(parseOptions OA.<**> OA.helper)
(OA.fullDesc <> OA.header "Plutus Core Debugger")
(uplcText, uplcDAnn) <- getProgramWithText optUplcInputFormat optUplcInput
hsText <- traverse Text.readFile optHsPath
-- The communication "channels" at debugger-driver and at brick
driverMailbox <- newEmptyMVar @(D.Cmd Breakpoints)
-- chan size of 20 is used as default for builtin non-custom events (mouse,key,etc)
brickMailbox <- B.newBChan @CustomBrickEvent 20
let app :: B.App DebuggerState CustomBrickEvent ResourceName
app =
B.App
{ B.appDraw = drawDebugger
, B.appChooseCursor = B.showFirstCursor
, B.appHandleEvent = handleDebuggerEvent driverMailbox
, B.appStartEvent = pure ()
, B.appAttrMap = const debuggerAttrMap
}
initialState =
DebuggerState
{ _dsKeyBindingsMode = KeyBindingsHidden
, _dsFocusRing =
B.focusRing $ catMaybes
[ Just EditorUplc
, EditorSource <$ optHsPath
, Just EditorReturnValue
, Just EditorLogs
]
, _dsUplcEditor = BE.editorText EditorUplc Nothing uplcText
, _dsUplcHighlight = Nothing
, _dsSourceEditor =
BE.editorText
EditorSource
Nothing <$>
hsText
, _dsSourceHighlight = Nothing
, _dsReturnValueEditor =
BE.editorText
EditorReturnValue
Nothing
""
, _dsLogsEditor =
BE.editorText
EditorLogs
Nothing
""
, _dsVLimitBottomEditors = 20
, _dsHLimitRightEditors = 100
, _dsBudgetData = BudgetData
{ _budgetSpent = mempty
-- the initial remaining budget is based on the passed cli arguments
, _budgetRemaining = optBudgetLim
}
}
let builder = Vty.mkVty Vty.defaultConfig
initialVty <- builder
-- TODO: find out if the driver-thread exits when brick exits
-- or should we wait for driver-thread?
_dTid <- forkIO $ driverThread driverMailbox brickMailbox uplcDAnn optBudgetLim
void $ B.customMain initialVty builder (Just brickMailbox) app initialState
{- | The main entrypoint of the driver thread.
The driver operates in IO (not in BrickM): the only way to "influence" Brick is via the mailboxes
-}
driverThread :: forall uni fun ann
. (uni ~ DefaultUni, fun ~ DefaultFun, ann ~ DAnn)
=> MVar (D.Cmd Breakpoints)
-> B.BChan CustomBrickEvent
-> Program Name uni fun ann
-> Maybe ExBudget
-> IO ()
driverThread driverMailbox brickMailbox prog mbudget = do
let term = prog ^. UPLC.progTerm
MachineParameters defaultCosts defaultRuntime = PLC.defaultCekParameters
ndterm <- case runExcept @FreeVariableError $ deBruijnTerm term of
Right t -> pure t
Left _ -> fail $ "deBruijnTerm failed: " <> PLC.displayPlcDef (void term)
-- if user provided `--budget` the mode is restricting; otherwise just counting
-- See NOTE [Budgeting implementation for the debugger]
let ExBudgetMode initExBudgetInfo = case mbudget of
Just budgetLimit -> coerceMode $ restricting $ ExRestrictingBudget budgetLimit
_ -> coerceMode counting
exBudgetInfo@(ExBudgetInfo spender _ _) <- stToIO initExBudgetInfo
ctr <- newCounter 8
let ?cekRuntime = defaultRuntime
?cekEmitter = const $ pure () -- TODO: implement emitter
?cekBudgetSpender = spender
?cekCosts = defaultCosts
-- The slippage optimization must be *off* to effectively
-- get *live* accounting/budgeting that is correct/up-to-date.
-- One way to achieve this is by setting slippage to 0 (1 would also work).
?cekSlippage = 0
?cekStepCounter = ctr
in D.iterM (handle exBudgetInfo) $ D.runDriver ndterm
where
-- this gets rid of the CountingSt/RestrictingSt newtype wrappers
-- See NOTE [Budgeting implementation for the debugger]
coerceMode :: Coercible cost ExBudget
=> ExBudgetMode cost uni fun
-> ExBudgetMode ExBudget uni fun
coerceMode = coerce
-- Peels off one Free monad layer
-- Note to self: for some reason related to implicit params I cannot turn the following
-- into a let block and avoid passing exbudgetinfo as parameter
handle :: (s ~ RealWorld, GivenCekReqs uni fun ann s)
=> ExBudgetInfo ExBudget uni fun s
-> D.DebugF uni fun ann Breakpoints (IO ())
-> IO ()
handle exBudgetInfo = \case
D.StepF prevState k -> do
stepRes <- cekMToIO $ D.tryHandleStep prevState
-- if error then handle it, otherwise "kontinue"
case stepRes of
Left e -> handleError exBudgetInfo e
Right newState -> k newState
D.InputF k -> handleInput >>= k
D.LogF text k -> handleLog text >> k
D.UpdateClientF ds k -> handleUpdate exBudgetInfo ds >> k
handleInput = takeMVar driverMailbox
handleUpdate exBudgetInfo cekState = do
bd <- readBudgetData exBudgetInfo
B.writeBChan brickMailbox $ UpdateClientEvent bd cekState
handleError exBudgetInfo e = do
bd <- readBudgetData exBudgetInfo
B.writeBChan brickMailbox $ ErrorEvent bd e
-- no kontinuation in case of error, the driver thread exits
-- FIXME: decide what should happen after the error occurs
-- e.g. a user dialog to (r)estart the thread with a button
handleLog = B.writeBChan brickMailbox . LogEvent
readBudgetData :: ExBudgetInfo ExBudget uni fun RealWorld -> IO BudgetData
readBudgetData (ExBudgetInfo _ final cumulative) =
stToIO (BudgetData <$> cumulative <*> (for mbudget $ const final))
-- | Read uplc code in a given format
--
-- Adapted from `Common.getProgram`
getProgramWithText :: Format -> Input -> IO (Text, UplcProg DAnn)
getProgramWithText fmt inp =
case fmt of
Textual -> do
-- here we use the original raw uplc text, we do not attempt any prettyfying
(progTextRaw, progWithUplcSpan) <- parseInput inp
let -- IMPORTANT: we cannot have any Tx.SourceSpans available in Textual mode
-- We still show the SourceEditor but TX highlighting (or breakpointing) won't work.
-- TODO: disable setting TX.breakpoints from inside the brick gui interface
addEmptyTxSpans = fmap (`DAnn` mempty)
progWithDAnn = addEmptyTxSpans progWithUplcSpan
pure (progTextRaw, progWithDAnn)
Flat flatMode -> do
-- here comes the dance of flat-parsing->PRETTYfying->text-parsing
-- so we can have artificial SourceSpans in annotations
progWithTxSpans <- loadASTfromFlat @UplcProg @PLC.SrcSpans flatMode inp
-- annotations are not pprinted by default, no need to `void`
let progTextPretty = PLC.displayPlcDef progWithTxSpans
-- the parsed prog with uplc.srcspan
progWithUplcSpan <- either (fail . show @ParserErrorBundle) pure $ runExcept $
PLC.runQuoteT $ UPLC.parseProgram progTextPretty
-- zip back the two programs into one program with their annotations' combined
-- the zip may fail if the AST cannot parse-pretty roundtrip (should not happen).
progWithDAnn <- either fail pure $ runExcept $
pzipWith DAnn progWithUplcSpan progWithTxSpans
pure (progTextPretty, progWithDAnn)