SCP-3392 UPLC simplifier

Don't look here yet, just benchmarking something.

Author: michaelpj

plutus-benchmark/nofib/test/Spec.hs

@@ -46,7 +46,7 @@ testClausify = testGroup "clausify"
                , testCase "formula3" $ mkClausifyTest Clausify.F3
                , testCase "formula4" $ mkClausifyTest Clausify.F4
                , testCase "formula5" $ mkClausifyTest Clausify.F5
-               , Tx.fitsInto "formula1 (size)" (Clausify.mkClausifyCode Clausify.F1) 5190
+               , Tx.fitsInto "formula1 (size)" (Clausify.mkClausifyCode Clausify.F1) 5824
                , runTestNested $ Tx.goldenBudget "formulaBudget" $ Clausify.mkClausifyCode Clausify.F1
                ]
 
@@ -64,7 +64,7 @@ testKnights = testGroup "knights"  -- Odd sizes call "error" because there are n
               , testCase "depth 100, 4x4" $ mkKnightsTest 100 4
               , testCase "depth 100, 6x6" $ mkKnightsTest 100 6
               , testCase "depth 100, 8x8" $ mkKnightsTest 100 8
-              , Tx.fitsInto "depth 10, 4x4 (size)" (Knights.mkKnightsCode 10 4) 3669
+              , Tx.fitsInto "depth 10, 4x4 (size)" (Knights.mkKnightsCode 10 4) 3724
               , runTestNested $ Tx.goldenBudget "knightsBudget" $ Knights.mkKnightsCode 10 4
               ]
 

plutus-benchmark/nofib/test/formulaBudget.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 52200152258
-| mem: 174669548
+({ cpu: 48335021398
+| mem: 161687548
 })

plutus-benchmark/nofib/test/knightsBudget.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 10658709240
-| mem: 33475372
+({ cpu: 9122720170
+| mem: 28316372
 })

plutus-benchmark/nofib/test/queens4budget.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 19730440366
-| mem: 62692642
+({ cpu: 17086419328
+| mem: 53812042
 })

plutus-benchmark/nofib/test/queens5budget.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 263250282408
-| mem: 828489180
+({ cpu: 228731019613
+| mem: 712547680
 })

plutus-core/plutus-core.cabal

@@ -143,6 +143,7 @@ library
         UntypedPlutusCore.Evaluation.Machine.Cek.Internal
         UntypedPlutusCore.Parser
         UntypedPlutusCore.Rename
+        UntypedPlutusCore.MkUPlc
         UntypedPlutusCore.Check.Scope
         UntypedPlutusCore.Check.Uniques
         UntypedPlutusCore.Core.Type
@@ -220,6 +221,7 @@ library
         PlutusIR.TypeCheck.Internal
 
         UntypedPlutusCore.Analysis.Definitions
+        UntypedPlutusCore.Analysis.Usages
         UntypedPlutusCore.Core
         UntypedPlutusCore.Core.Instance
         UntypedPlutusCore.Core.Instance.Eq
@@ -236,9 +238,11 @@ library
         UntypedPlutusCore.Evaluation.Machine.Cek.EmitterMode
         UntypedPlutusCore.Mark
         UntypedPlutusCore.Rename.Internal
+        UntypedPlutusCore.Simplify
         UntypedPlutusCore.Size
         UntypedPlutusCore.Subst
-        UntypedPlutusCore.Transform.Simplify
+        UntypedPlutusCore.Transform.ForceDelay
+        UntypedPlutusCore.Transform.Inline
 
         Data.Aeson.Flatten
         Data.Aeson.THReader
@@ -452,6 +456,7 @@ test-suite untyped-plutus-core-test
         bytestring -any,
         hedgehog -any,
         flat -any,
+        lens -any,
         mtl -any,
         plutus-core -any,
         plutus-core-testlib -any,

plutus-core/plutus-ir/src/PlutusIR/Compiler.hs

@@ -12,6 +12,7 @@ module PlutusIR.Compiler (
     AsTypeError (..),
     AsTypeErrorExt (..),
     Provenance (..),
+    DatatypeComponent (..),
     noProvenance,
     CompilationOpts,
     coOptimize,

plutus-core/plutus-ir/src/PlutusIR/Compiler/Datatype.hs

@@ -308,7 +308,9 @@ mkConstructorType :: Datatype TyName Name uni fun (Provenance a) -> VarDecl TyNa
 -- we don't need to do anything to the declared type
 -- see note [Abstract data types]
 -- FIXME: normalize constructors also here
-mkConstructorType (Datatype _ _ tvs _ _) constr = PIR.mkIterTyForall  tvs $ _varDeclType constr
+mkConstructorType (Datatype _ _ tvs _ _) constr =
+    let constrTy = PIR.mkIterTyForall tvs $ _varDeclType constr
+    in fmap (\a -> DatatypeComponent ConstructorType a) constrTy
 
 -- See note [Scott encoding of datatypes]
 -- | Make a constructor of a 'Datatype' with the given pattern functor. The constructor argument mostly serves to identify the constructor
@@ -333,34 +335,35 @@ mkConstructor dty d@(Datatype ann _ tvs _ constrs) index = do
           pure $ zipWith (VarDecl ann) caseArgNames caseTypes
 
     -- This is inelegant, but it should never fail
-    let constr = constrs !! index
+    let thisConstr = constrs !! index
     let thisCase = PIR.mkVar ann $ casesAndTypes !! index
 
     -- constructor args and their types
     argsAndTypes <- do
         -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
         -- see note [Abstract data types]
         -- FIXME: normalize datacons' types also here
-        let argTypes = unveilDatatype (getType dty) d <$> constructorArgTypes constr
+        let argTypes = unveilDatatype (getType dty) d <$> constructorArgTypes thisConstr
         -- we don't have any names for these things, we just had the type, so we call them "arg_i
         argNames <- for [0..(length argTypes -1)] (\i -> safeFreshName $ "arg_" <> showText i)
         pure $ zipWith (VarDecl ann) argNames argTypes
 
 
-    pure $
-        -- /\t_1 .. t_n
-        PIR.mkIterTyAbs tvs $
-        -- \arg_1 .. arg_m
-        PIR.mkIterLamAbs argsAndTypes $
-        -- See Note [Recursive datatypes]
-        -- wrap
-        wrap ann dty (fmap (PIR.mkTyVar ann) tvs)$
-        -- forall out
-        TyAbs ann resultType (Type ann) $
-        -- \case_1 .. case_j
-        PIR.mkIterLamAbs casesAndTypes $
-        -- c_i arg_1 .. arg_m
-        PIR.mkIterApp ann thisCase (fmap (PIR.mkVar ann) argsAndTypes)
+    let constr =
+            -- /\t_1 .. t_n
+            PIR.mkIterTyAbs tvs $
+            -- \arg_1 .. arg_m
+            PIR.mkIterLamAbs argsAndTypes $
+            -- See Note [Recursive datatypes]
+            -- wrap
+            wrap ann dty (fmap (PIR.mkTyVar ann) tvs)$
+            -- forall out
+            TyAbs ann resultType (Type ann) $
+            -- \case_1 .. case_j
+            PIR.mkIterLamAbs casesAndTypes $
+            -- c_i arg_1 .. arg_m
+            PIR.mkIterApp ann thisCase (fmap (PIR.mkVar ann) argsAndTypes)
+    pure $ fmap (\a -> DatatypeComponent Constructor a) constr
 
 -- Destructors
 
@@ -379,15 +382,16 @@ mkDestructor dty (Datatype ann _ tvs _ _) = do
     let appliedReal = PIR.mkIterTyApp ann (getType dty) (fmap (PIR.mkTyVar ann) tvs)
 
     xn <- safeFreshName "x"
-    pure $
-        -- /\t_1 .. t_n
-        PIR.mkIterTyAbs tvs $
-        -- \x
-        LamAbs ann xn appliedReal $
-        -- See note [Recursive datatypes]
-        -- unwrap
-        unwrap ann dty $
-        Var ann xn
+    let destr =
+            -- /\t_1 .. t_n
+            PIR.mkIterTyAbs tvs $
+            -- \x
+            LamAbs ann xn appliedReal $
+            -- See note [Recursive datatypes]
+            -- unwrap
+            unwrap ann dty $
+            Var ann xn
+    pure $ fmap (\a -> DatatypeComponent Destructor a) destr
 
 -- See note [Scott encoding of datatypes]
 -- | Make the type of a destructor for a 'Datatype'.
@@ -396,8 +400,8 @@ mkDestructor dty (Datatype ann _ tvs _ _) = do
 --         = forall (a :: *) . (List a) -> (<pattern functor of List>)
 --         = forall (a :: *) . (List a) -> (forall (out_List :: *) . (out_List -> (a -> List a -> out_List) -> out_List))
 -- @
-mkDestructorTy :: ann -> Type TyName uni ann -> Datatype TyName Name uni fun ann -> Type TyName uni ann
-mkDestructorTy ann pf dt@(Datatype _ _ tvs _ _) =
+mkDestructorTy :: PIRType uni a -> Datatype TyName Name uni fun (Provenance a) -> PIRType uni a
+mkDestructorTy pf dt@(Datatype ann _ tvs _ _) =
     -- we essentially "unveil" the abstract type, so this
     -- is a function from the (instantiated) abstract type
     -- to the (unwrapped, i.e. the pattern functor of the) "real" Scott-encoded type that we can use as
@@ -409,9 +413,8 @@ mkDestructorTy ann pf dt@(Datatype _ _ tvs _ _) =
     -- t t_1 .. t_n
     let appliedAbstract = mkDatatypeValueType ann dt
     -- forall t_1 .. t_n
-    in
-        PIR.mkIterTyForall tvs $
-        TyFun ann appliedAbstract pf
+        destrTy = PIR.mkIterTyForall tvs $ TyFun ann appliedAbstract pf
+    in fmap (\a -> DatatypeComponent DestructorType a) destrTy
 
 -- The main function
 
@@ -425,8 +428,8 @@ compileDatatype r body d = do
     let
         tyVars = [PIR.defVar concreteTyDef]
         tys = [getType $ PIR.defVal concreteTyDef]
-        vars = fmap PIR.defVar constrDefs ++ [PIR.defVar destrDef]
-        vals = fmap PIR.defVal constrDefs ++ [PIR.defVal destrDef]
+        vars = fmap PIR.defVar constrDefs ++ [ PIR.defVar destrDef ]
+        vals = fmap PIR.defVal constrDefs ++ [ PIR.defVal destrDef ]
     -- See note [Abstract data types]
     pure $ PIR.mkIterApp p (PIR.mkIterInst p (PIR.mkIterTyAbs tyVars (PIR.mkIterLamAbs vars body)) tys) vals
 
@@ -443,11 +446,11 @@ compileDatatypeDefs r d@(Datatype ann tn _ destr constrs) = do
 
     constrDefs <- for (zip constrs [0..]) $ \(c, i) -> do
         let constrTy = mkConstructorType d c
-        PIR.Def (VarDecl ann (_varDeclName c) constrTy) <$> mkConstructor (PIR.defVal concreteTyDef) d i
+        PIR.Def (VarDecl (DatatypeComponent Constructor ann) (_varDeclName c) constrTy) <$> mkConstructor (PIR.defVal concreteTyDef) d i
 
     destrDef <- do
-        let destTy = mkDestructorTy ann pf d
-        PIR.Def (VarDecl ann destr destTy) <$> mkDestructor (PIR.defVal concreteTyDef) d
+        let destTy = mkDestructorTy pf d
+        PIR.Def (VarDecl (DatatypeComponent Destructor ann) destr destTy) <$> mkDestructor (PIR.defVal concreteTyDef) d
 
     pure (concreteTyDef, constrDefs, destrDef)
 

plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs

@@ -57,7 +57,7 @@ data CompilationOpts = CompilationOpts {
 makeLenses ''CompilationOpts
 
 defaultCompilationOpts :: CompilationOpts
-defaultCompilationOpts = CompilationOpts True False False False 8 True True True False
+defaultCompilationOpts = CompilationOpts True False False False 12 True True True False
 
 data CompilationCtx uni fun a = CompilationCtx {
     _ccOpts              :: CompilationOpts

plutus-core/untyped-plutus-core/src/UntypedPlutusCore.hs

@@ -14,9 +14,9 @@ import PlutusCore.Name as Export
 import UntypedPlutusCore.Core as Export
 import UntypedPlutusCore.Core.Instance.Flat as Export
 import UntypedPlutusCore.DeBruijn as Export
+import UntypedPlutusCore.Simplify as Export
 import UntypedPlutusCore.Size as Export
 import UntypedPlutusCore.Subst as Export
-import UntypedPlutusCore.Transform.Simplify as Export
 -- Also has some functions