Skip to content

Commit cea546c

Browse files
authored
plutus exe: Also run a final check after the programs are applied together (#6753)
Co-authored-by: Nikolaos Bezirgiannis <bezirg@users.noreply.github.com>
1 parent 292d0d7 commit cea546c

File tree

2 files changed

+37
-8
lines changed

2 files changed

+37
-8
lines changed

plutus-core/executables/plutus/AnyProgram/Compile.hs

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
{-# LANGUAGE ViewPatterns #-}
66
module AnyProgram.Compile
77
( compileProgram
8+
, checkProgram
89
, toOutAnn
910
, plcToOutName
1011
, uplcToOutName
@@ -95,6 +96,7 @@ compileProgram = curry $ \case
9596
compileProgram sng1 (SPlc n2 a1)
9697
>=> pure . embedProgram
9798
-- here we also run the pir typechecker, and pir optimiser
99+
-- MAYBE: we shouldn't do the above?
98100
>=> compileProgram (SPir n2 a1) (SPir n2 a2)
99101

100102
-- pir to uplc
@@ -301,3 +303,15 @@ uplcToOutName' _ _ = error "this is complete, but i don't want to use -fno-warn-
301303
throwingPIR :: (PIR.AsError e uni fun a, MonadError e m)
302304
=> Text -> b -> m c
303305
throwingPIR = const . throwing PIR._Error . PIR.OptionsError
306+
307+
checkProgram :: (e ~ PIR.Provenance (FromAnn (US_ann s)),
308+
MonadError (PIR.Error DefaultUni DefaultFun e) m)
309+
=> SLang s
310+
-> FromLang s
311+
-> m ()
312+
checkProgram sng p = modifyError (fmap PIR.Original) $ case sng of
313+
SPlc n a -> modifyError PIR.PLCError $ plcTypecheck n a p
314+
SUplc n a -> uplcTypecheck n a p
315+
SPir SName a -> pirTypecheck a p
316+
SData -> pure () -- data is type correct by construction
317+
SPir{} -> throwingPIR "PIR: Cannot typecheck non-names" ()

plutus-core/executables/plutus/Mode/Compile.hs

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -31,18 +31,20 @@ runCompile afterCompile = case ?opts of
3131
-- compile the tail targetting sngT, and fold-apply the results together with the head
3232
astT <- foldlM (readCompileApply sngT) hdT tlS
3333

34-
optAstT <- if _wholeOpt ?opts
35-
-- self-compile one last time for optimisation
36-
then compile sngT sngT astT
37-
else pure astT
34+
appliedAstT <-
35+
if _wholeOpt ?opts
36+
then -- self-compile one last time for optimisation (also runs the checks)
37+
compile sngT sngT astT
38+
else -- The checks should run also at the whole (applied) program
39+
check sngT astT
3840

39-
writeProgram sngT optAstT fileT afterCompile
41+
writeProgram sngT appliedAstT fileT afterCompile
4042

4143
case afterCompile of
4244
Exit{} -> exitSuccess -- nothing left to do
43-
Run{} -> runRun sngT optAstT
44-
Bench{} -> runBench sngT optAstT
45-
Debug{} -> runDebug sngT optAstT
45+
Run{} -> runRun sngT appliedAstT
46+
Bench{} -> runBench sngT appliedAstT
47+
Debug{} -> runDebug sngT appliedAstT
4648

4749
readCompileApply :: (?opts :: Opts)
4850
=> SLang t -> FromLang t -> SomeFile -> IO (FromLang t)
@@ -70,3 +72,16 @@ compile sngS sngT astS =
7072
Left err -> withA @Pretty (_sann sngS) $ failE $ show err
7173
Right res -> pure res
7274

75+
check :: (?opts :: Opts)
76+
=> SLang t -> FromLang t -> IO (FromLang t)
77+
check sngT astT =
78+
if length (_inputs ?opts) == 1
79+
-- optimization: no need to do more checks if there was no application involved
80+
then pure astT
81+
else case checkProgram sngT astT of
82+
-- compilation errors use the annotation type of the sources
83+
Left err -> do
84+
printE "Failed to typecheck fully-applied program. The error was:"
85+
withA @Pretty (_sann sngT) $ failE $ show err
86+
-- passed the checks, return it
87+
_ -> pure astT

0 commit comments

Comments
 (0)