Skip to content

Commit

Permalink
plutus exe: Also run a final check after the programs are applied tog…
Browse files Browse the repository at this point in the history
…ether
  • Loading branch information
bezirg committed Jan 13, 2025
1 parent 292d0d7 commit 697a2ab
Show file tree
Hide file tree
Showing 2 changed files with 37 additions and 8 deletions.
14 changes: 14 additions & 0 deletions plutus-core/executables/plutus/AnyProgram/Compile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
{-# LANGUAGE ViewPatterns #-}
module AnyProgram.Compile
( compileProgram
, checkProgram
, toOutAnn
, plcToOutName
, uplcToOutName
Expand Down Expand Up @@ -95,6 +96,7 @@ compileProgram = curry $ \case
compileProgram sng1 (SPlc n2 a1)
>=> pure . embedProgram
-- here we also run the pir typechecker, and pir optimiser
-- MAYBE: we shouldn't do the above?
>=> compileProgram (SPir n2 a1) (SPir n2 a2)

-- pir to uplc
Expand Down Expand Up @@ -301,3 +303,15 @@ uplcToOutName' _ _ = error "this is complete, but i don't want to use -fno-warn-
throwingPIR :: (PIR.AsError e uni fun a, MonadError e m)
=> Text -> b -> m c
throwingPIR = const . throwing PIR._Error . PIR.OptionsError

checkProgram :: (e ~ PIR.Provenance (FromAnn (US_ann s)),
MonadError (PIR.Error DefaultUni DefaultFun e) m)
=> SLang s
-> FromLang s
-> m ()
checkProgram sng p = modifyError (fmap PIR.Original) $ case sng of
SPlc n a -> modifyError PIR.PLCError $ plcTypecheck n a p
SUplc n a -> uplcTypecheck n a p
SPir SName a -> pirTypecheck a p
SData -> pure () -- data is type correct by construction
SPir{} -> throwingPIR "PIR: Cannot typecheck non-names" ()
31 changes: 23 additions & 8 deletions plutus-core/executables/plutus/Mode/Compile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,18 +31,20 @@ runCompile afterCompile = case ?opts of
-- compile the tail targetting sngT, and fold-apply the results together with the head
astT <- foldlM (readCompileApply sngT) hdT tlS

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

writeProgram sngT optAstT fileT afterCompile
writeProgram sngT appliedAstT fileT afterCompile

case afterCompile of
Exit{} -> exitSuccess -- nothing left to do
Run{} -> runRun sngT optAstT
Bench{} -> runBench sngT optAstT
Debug{} -> runDebug sngT optAstT
Run{} -> runRun sngT appliedAstT
Bench{} -> runBench sngT appliedAstT
Debug{} -> runDebug sngT appliedAstT

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

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

0 comments on commit 697a2ab

Please sign in to comment.