Skip to content

Commit

Permalink
Add improvements to the PIR compiler
Browse files Browse the repository at this point in the history
- pedantic typechecking will typecheck between simplifier passes,
- add option for being verbose about simplifier passes, and
- add option for dumping PIR to stdout before and after a pass.
  • Loading branch information
Jakub Zalewski committed Aug 4, 2021

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent a2ce648 commit 597960b
Showing 14 changed files with 238 additions and 166 deletions.
1 change: 1 addition & 0 deletions plutus-core/plutus-core.cabal
Original file line number Diff line number Diff line change
@@ -271,6 +271,7 @@ library
deriving-compat -any,
dlist -any,
exceptions -any,
extra -any,
filepath -any,
flat -any,
ghc-prim -any,
97 changes: 83 additions & 14 deletions plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module PlutusIR.Compiler (
compileTerm,
compileToReadable,
@@ -13,6 +15,14 @@ module PlutusIR.Compiler (
noProvenance,
CompilationOpts,
coOptimize,
coPedantic,
coVerbose,
coDebug,
coMaxSimplifierIterations,
coDoSimplifierUnwrapCancel,
coDoSimplifierBeta,
coDoSimplifierInline,
coDoSimplifierRemoveDeadBindings,
defaultCompilationOpts,
CompilationCtx,
ccOpts,
@@ -40,24 +50,78 @@ import qualified PlutusIR.Transform.Unwrap as Unwrap
import PlutusIR.TypeCheck.Internal

import qualified PlutusCore as PLC
import qualified PlutusCore.Constant.Meaning as M

import Control.Lens
import Control.Monad
import Control.Monad.Extra (orM, whenM)
import Control.Monad.Reader
import Debug.Trace (traceM)
import PlutusPrelude

-- Simplifier passes
data Pass uni fun =
Pass { _name :: String
, _shouldRun :: forall m e a. Compiling m e uni fun a => m Bool
, _pass :: forall m e a b. Compiling m e uni fun a => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
}

onOption :: Compiling m e uni fun a => Lens' CompilationOpts Bool -> m Bool
onOption coOpt = view (ccOpts . coOpt)

isVerbose :: Compiling m e uni fun a => m Bool
isVerbose = view $ ccOpts . coVerbose

isDebug :: Compiling m e uni fun a => m Bool
isDebug = view $ ccOpts . coDebug

applyPass :: (Compiling m e uni fun a, b ~ Provenance a) => Pass uni fun -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
applyPass pass = runIf (_shouldRun pass) $ \term -> do
let passName = _name pass
whenM (orM [isVerbose, isDebug]) $ traceM (" !!! " ++ passName)
whenM isDebug $ do
traceM $ " !!! Before " ++ passName
traceM $ show $ pretty term
term' <- _pass pass term
whenM isDebug $ do
traceM $ " !!! After " ++ passName
traceM $ show $ pretty term'
check term'
pure term'

availablePasses :: [Pass uni fun]
availablePasses =
[ Pass "unwrap cancel" (onOption coDoSimplifierUnwrapCancel) (pure . Unwrap.unwrapCancel)
, Pass "beta" (onOption coDoSimplifierBeta) (pure . Beta.beta)
, Pass "inline" (onOption coDoSimplifierInline) Inline.inline
, Pass "remove dead bindings" (onOption coDoSimplifierRemoveDeadBindings) DeadCode.removeDeadBindings
]

-- | Actual simplifier
simplify
:: (M.ToBuiltinMeaning uni fun, PLC.MonadQuote m)
:: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
=> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify = DeadCode.removeDeadBindings <=< Inline.inline . Beta.beta . Unwrap.unwrapCancel
simplify = foldl' (>=>) pure (map applyPass availablePasses)

-- | Perform some simplification of a 'Term'.
simplifyTerm :: Compiling m e uni fun a => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm = PLC.rename >=> runIfOpts simplify
-- Note: There was a bug in renamer handling non-rec terms, so we need to rename
-- again.
-- https://jira.iohk.io/browse/SCP-2156
simplifyTerm
:: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
=> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm = runIfOpts $ DeadCode.removeDeadBindings >=> simplify'
-- NOTE: we need at least one pass of dead code elimination
where
simplify' :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify' t = do
maxIterations <- view (ccOpts . coMaxSimplifierIterations)
simplifyNTimes maxIterations t
-- Run the simplifier @n@ times
simplifyNTimes :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyNTimes n = foldl' (>=>) pure (map simplifyStep [1 .. n])
-- generate simplification step
simplifyStep :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyStep i term = do
whenM (orM [isVerbose, isDebug]) $ traceM $ "!!! simplifier pass " ++ show i
simplify term


-- | Perform floating/merging of lets in a 'Term' to their nearest lambda/Lambda/letStrictNonValue.
-- Note: It assumes globally unique names
@@ -66,7 +130,7 @@ floatTerm = runIfOpts $ pure . LetFloat.floatTerm

-- | Typecheck a PIR Term iff the context demands it.
-- Note: assumes globally unique names
typeCheckTerm :: Compiling m e uni fun b => Term TyName Name uni fun (Provenance b) -> m ()
typeCheckTerm :: (Compiling m e uni fun a, b ~ Provenance a) => Term TyName Name uni fun b -> m ()
typeCheckTerm t = do
mtcconfig <- asks _ccTypeCheckConfig
case mtcconfig of
@@ -75,15 +139,16 @@ typeCheckTerm t = do

check :: Compiling m e uni fun b => Term TyName Name uni fun (Provenance b) -> m ()
check arg = do
shouldCheck <- view (ccOpts . coParanoidTypechecking)
shouldCheck <- view (ccOpts . coPedantic)
if shouldCheck then typeCheckTerm arg else pure ()

-- | The 1st half of the PIR compiler pipeline up to floating/merging the lets.
-- We stop momentarily here to give a chance to the tx-plugin
-- to dump a "readable" version of pir (i.e. floated).
compileToReadable :: Compiling m e uni fun a
=> Term TyName Name uni fun a
-> m (Term TyName Name uni fun (Provenance a))
compileToReadable
:: (Compiling m e uni fun a, b ~ Provenance a)
=> Term TyName Name uni fun a
-> m (Term TyName Name uni fun b)
compileToReadable =
(pure . original)
-- We need globally unique names for typechecking, floating, and compiling non-strict bindings
@@ -99,7 +164,7 @@ compileToReadable =
-- | The 2nd half of the PIR compiler pipeline.
-- Compiles a 'Term' into a PLC Term, by removing/translating step-by-step the PIR's language construsts to PLC.
-- Note: the result *does* have globally unique names.
compileReadableToPlc :: Compiling m e uni fun a => Term TyName Name uni fun (Provenance a) -> m (PLCTerm uni fun a)
compileReadableToPlc :: (Compiling m e uni fun a, b ~ Provenance a) => Term TyName Name uni fun b -> m (PLCTerm uni fun a)
compileReadableToPlc =
NonStrict.compileNonStrictBindings
>=> through check
@@ -111,6 +176,10 @@ compileReadableToPlc =
>=> through check
-- We introduce some non-recursive let bindings while eliminating recursive let-bindings, so we
-- can eliminate any of them which are unused here.
>=> PLC.rename
-- NOTE: There was a bug in renamer handling non-rec terms, so we need to
-- rename again.
-- https://jira.iohk.io/browse/SCP-2156
>=> simplifyTerm
>=> Let.compileLets Let.Types
>=> Let.compileLets Let.NonRecTerms
33 changes: 27 additions & 6 deletions plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
Original file line number Diff line number Diff line change
@@ -18,6 +18,7 @@ import Control.Lens

import qualified PlutusCore as PLC
import qualified PlutusCore.MkPlc as PLC
import qualified PlutusCore.Pretty as PLC
import PlutusCore.Quote
import qualified PlutusCore.StdLib.Type as Types
import qualified PlutusCore.TypeCheck.Internal as PLC
@@ -41,14 +42,22 @@ instance PLC.HasTypeCheckConfig (PirTCConfig uni fun) uni fun where
typeCheckConfig = pirConfigTCConfig

data CompilationOpts = CompilationOpts {
_coOptimize :: Bool
, _coParanoidTypechecking :: Bool
_coOptimize :: Bool
, _coPedantic :: Bool
, _coVerbose :: Bool
, _coDebug :: Bool
, _coMaxSimplifierIterations :: Int
-- Simplifier passes
, _coDoSimplifierUnwrapCancel :: Bool
, _coDoSimplifierBeta :: Bool
, _coDoSimplifierInline :: Bool
, _coDoSimplifierRemoveDeadBindings :: Bool
} deriving (Eq, Show)

makeLenses ''CompilationOpts

defaultCompilationOpts :: CompilationOpts
defaultCompilationOpts = CompilationOpts True False
defaultCompilationOpts = CompilationOpts True False False False 8 True True True True

data CompilationCtx uni fun a = CompilationCtx {
_ccOpts :: CompilationOpts
@@ -68,10 +77,17 @@ getEnclosing = view ccEnclosing
withEnclosing :: MonadReader (CompilationCtx uni fun a) m => (Provenance a -> Provenance a) -> m b -> m b
withEnclosing f = local (over ccEnclosing f)

runIf
:: MonadReader (CompilationCtx uni fun a) m
=> m Bool
-> (b -> m b)
-> (b -> m b)
runIf condition pass arg = do
doPass <- condition
if doPass then pass arg else pure arg

runIfOpts :: MonadReader (CompilationCtx uni fun a) m => (b -> m b) -> (b -> m b)
runIfOpts pass arg = do
doOpt <- view (ccOpts . coOptimize)
if doOpt then pass arg else pure arg
runIfOpts = runIf $ view (ccOpts . coOptimize)

type PLCTerm uni fun a = PLC.Term PLC.TyName PLC.Name uni fun (Provenance a)
type PLCType uni a = PLC.Type PLC.TyName uni (Provenance a)
@@ -113,6 +129,11 @@ type Compiling m e uni fun a =
, Ord a
, PLC.Typecheckable uni fun
, PLC.GEq uni
-- Pretty printing instances
, PLC.Pretty fun
, PLC.Closed uni
, PLC.GShow uni
, uni `PLC.Everywhere` PLC.PrettyConst
)

type TermDef tyname name uni fun a = PLC.Def (PLC.VarDecl tyname name uni fun a) (PIR.Term tyname name uni fun a)
3 changes: 2 additions & 1 deletion plutus-core/plutus-ir/test/TestLib.hs
Original file line number Diff line number Diff line change
@@ -24,6 +24,7 @@ import Control.Monad.Reader as Reader
import qualified PlutusCore as PLC
import PlutusCore.Name
import PlutusCore.Pretty
import qualified PlutusCore.Pretty as PLC
import PlutusCore.Quote
import PlutusIR as PIR
import PlutusIR.Compiler as PIR
@@ -58,7 +59,7 @@ asIfThrown
asIfThrown = withExceptT SomeException . hoist (pure . runIdentity)

compileAndMaybeTypecheck
:: (PLC.GEq uni, PLC.Typecheckable uni fun, Ord a)
:: (PLC.GEq uni, PLC.Typecheckable uni fun, Ord a, PLC.Pretty fun, PLC.Closed uni, PLC.GShow uni, uni `PLC.Everywhere` PLC.PrettyConst)
=> Bool
-> Term TyName Name uni fun a
-> Except (PIR.Error uni fun (PIR.Provenance a)) (PLC.Term TyName Name uni fun (PIR.Provenance a))
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/test/datatypes/listMatchEval.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(delay (lam x_195 x_195))
(delay (lam x_877 x_877))
39 changes: 10 additions & 29 deletions plutus-core/plutus-ir/test/datatypes/maybe.golden
Original file line number Diff line number Diff line change
@@ -1,37 +1,18 @@
(program 1.0.0
[
[
[
(lam
Just_i0
(all a_i0 (type) (fun a_i1 [(lam a_i0 (type) (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))) a_i1]))
(lam
Nothing_i0
(all a_i0 (type) [(lam a_i0 (type) (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))) a_i1])
(lam
Just_i0
(all a_i0 (type) (fun a_i1 [(lam a_i0 (type) (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))) a_i1]))
(lam
match_Maybe_i0
(all a_i0 (type) (fun [(lam a_i0 (type) (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))) a_i1] (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))))
[
{ Just_i2 (all a_i0 (type) (fun a_i1 a_i1)) }
(abs a_i0 (type) (lam x_i0 a_i2 x_i1))
]
)
)
)
(abs
a_i0
(type)
(abs
out_Maybe_i0
(type)
(lam
case_Nothing_i0
out_Maybe_i2
(lam case_Just_i0 (fun a_i4 out_Maybe_i3) case_Nothing_i2)
)
)
match_Maybe_i0
(all a_i0 (type) (fun [(lam a_i0 (type) (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))) a_i1] (all out_Maybe_i0 (type) (fun out_Maybe_i1 (fun (fun a_i2 out_Maybe_i1) out_Maybe_i1)))))
[
{ Just_i2 (all a_i0 (type) (fun a_i1 a_i1)) }
(abs a_i0 (type) (lam x_i0 a_i2 x_i1))
]
)
]
)
(abs
a_i0
(type)
60 changes: 20 additions & 40 deletions plutus-core/plutus-ir/test/recursion/even3.golden
Original file line number Diff line number Diff line change
@@ -322,50 +322,30 @@
by_i0
(fun (all Q_i0 (type) (fun [F_i3 Q_i1] Q_i1)) (all Q_i0 (type) (fun [F_i3 Q_i1] Q_i1)))
[
{
(abs
b_i0
(type)
(lam
f_i0
(fun (fun (all Q_i0 (type) (fun [F_i4 Q_i1] [F_i4 Q_i1])) (all Q_i0 (type) (fun [F_i4 Q_i1] Q_i1))) (fun (all Q_i0 (type) (fun [F_i4 Q_i1] [F_i4 Q_i1])) (all Q_i0 (type) (fun [F_i4 Q_i1] Q_i1))))
[
(lam
f_i0
(fun (fun (all Q_i0 (type) (fun [F_i5 Q_i1] [F_i5 Q_i1])) b_i2) (fun (all Q_i0 (type) (fun [F_i5 Q_i1] [F_i5 Q_i1])) b_i2))
[
s_i0
[(lam a_i0 (type) (ifix (lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1))) a_i1)) (fun (all Q_i0 (type) (fun [F_i5 Q_i1] [F_i5 Q_i1])) (all Q_i0 (type) (fun [F_i5 Q_i1] Q_i1)))]
[ (unwrap s_i1) s_i1 ]
)
(iwrap
(lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1)))
(fun (all Q_i0 (type) (fun [F_i4 Q_i1] [F_i4 Q_i1])) (all Q_i0 (type) (fun [F_i4 Q_i1] Q_i1)))
(lam
s_i0
[(lam a_i0 (type) (ifix (lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1))) a_i1)) (fun (all Q_i0 (type) (fun [F_i5 Q_i1] [F_i5 Q_i1])) (all Q_i0 (type) (fun [F_i5 Q_i1] Q_i1)))]
(lam
s_i0
[(lam a_i0 (type) (ifix (lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1))) a_i1)) (fun (all Q_i0 (type) (fun [F_i6 Q_i1] [F_i6 Q_i1])) b_i3)]
[ (unwrap s_i1) s_i1 ]
x_i0
(all Q_i0 (type) (fun [F_i6 Q_i1] [F_i6 Q_i1]))
[ [ f_i3 [ (unwrap s_i2) s_i2 ] ] x_i1 ]
)
(iwrap
(lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1)))
(fun (all Q_i0 (type) (fun [F_i5 Q_i1] [F_i5 Q_i1])) b_i2)
(lam
s_i0
[(lam a_i0 (type) (ifix (lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1))) a_i1)) (fun (all Q_i0 (type) (fun [F_i6 Q_i1] [F_i6 Q_i1])) b_i3)]
(lam
x_i0
(all Q_i0 (type) (fun [F_i7 Q_i1] [F_i7 Q_i1]))
[
[
f_i3
[
(lam
s_i0
[(lam a_i0 (type) (ifix (lam self_i0 (fun (type) (type)) (lam a_i0 (type) (fun [self_i2 a_i1] a_i1))) a_i1)) (fun (all Q_i0 (type) (fun [F_i8 Q_i1] [F_i8 Q_i1])) b_i5)]
[ (unwrap s_i1) s_i1 ]
)
s_i2
]
]
x_i1
]
)
)
)
]
)
)
)
(all Q_i0 (type) (fun [F_i3 Q_i1] Q_i1))
}
]
)
(lam
rec_i0
(fun (all Q_i0 (type) (fun [F_i4 Q_i1] [F_i4 Q_i1])) (all Q_i0 (type) (fun [F_i4 Q_i1] Q_i1)))
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/test/recursion/even3Eval.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(delay (lam case_True_635 (lam case_False_636 case_False_636)))
(delay (lam case_True_2675 (lam case_False_2676 case_False_2676)))
Loading

0 comments on commit 597960b

Please sign in to comment.