Sums-of-products in PLC

plutus-benchmark/lists/test/Sum/left-fold-built-in.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 160559654
-| mem: 504532})
+({cpu: 158282654
+| mem: 494632})

plutus-benchmark/lists/test/Sum/left-fold-data.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 450587685
-| mem: 1461262})
+({cpu: 420457685
+| mem: 1330262})

plutus-benchmark/lists/test/Sum/left-fold-scott.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 150781800
-| mem: 566100})
+({cpu: 129897800
+| mem: 475300})

plutus-benchmark/lists/test/Sum/right-fold-built-in.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 167459654
-| mem: 534532})
+({cpu: 165182654
+| mem: 524632})

plutus-benchmark/lists/test/Sum/right-fold-data.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 457487685
-| mem: 1491262})
+({cpu: 427357685
+| mem: 1360262})

plutus-benchmark/lists/test/Sum/right-fold-scott.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 157681800
-| mem: 596100})
+({cpu: 136797800
+| mem: 505300})

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

@@ -1,2 +1,2 @@
-({cpu: 26010640908
-| mem: 111558948})
+({cpu: 11704042908
+| mem: 49356348})

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

@@ -1,2 +1,2 @@
-({cpu: 7264792298
-| mem: 27160640})
+({cpu: 5336978298
+| mem: 18778840})

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

@@ -1,2 +1,2 @@
-({cpu: 14076759305
-| mem: 54314242})
+({cpu: 10698680305
+| mem: 39626942})

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

@@ -1,2 +1,2 @@
-({cpu: 190421748648
-| mem: 720641780})
+({cpu: 145740959648
+| mem: 526377480})

plutus-benchmark/script-contexts/src/PlutusBenchmark/ScriptContexts.hs

@@ -10,6 +10,8 @@ import PlutusLedgerApi.V1.Address
 import PlutusLedgerApi.V1.Value
 import PlutusTx qualified as PlutusTx
 import PlutusTx.Builtins qualified as PlutusTx
+import PlutusTx.Code qualified as PlutusTx
+import PlutusTx.LiftU qualified as LiftU
 import PlutusTx.Prelude qualified as PlutusTx
 
 -- | A very crude deterministic generator for 'ScriptContext's with size
@@ -83,6 +85,34 @@ mkCheckScriptContext2Code sc =
   let d = PlutusTx.toBuiltinData sc
   in $$(PlutusTx.compile [|| checkScriptContext2 ||]) `PlutusTx.applyCode` PlutusTx.liftCode d
 
+-- Same as checkScriptContext1, but passing the ScriptContext as a term using LiftU
+{-# INLINABLE checkScriptContext3 #-}
+checkScriptContext3 :: ScriptContext -> ()
+checkScriptContext3 (ScriptContext txi _) =
+  if PlutusTx.length (txInfoOutputs txi) `PlutusTx.modInteger` 2 PlutusTx.== 0
+  then ()
+  else PlutusTx.traceError "Odd number of outputs"
+
+mkCheckScriptContext3Code :: ScriptContext -> PlutusTx.CompiledCode ()
+mkCheckScriptContext3Code sc =
+  $$(PlutusTx.compile [|| checkScriptContext3 ||])
+      `PlutusTx.applyCode` LiftU.liftCode sc
+
+-- Same as checkScriptContext2, but passing the ScriptContext as a term using LiftU
+{-# INLINABLE checkScriptContext4 #-}
+checkScriptContext4 :: ScriptContext -> ()
+checkScriptContext4 sc =
+  case sc of
+    !_ ->
+      if 48*9900 PlutusTx.== (475200 :: Integer)
+      then ()
+      else PlutusTx.traceError "Got my sums wrong"
+
+mkCheckScriptContext4Code :: ScriptContext -> PlutusTx.CompiledCode ()
+mkCheckScriptContext4Code sc =
+  $$(PlutusTx.compile [|| checkScriptContext4 ||])
+      `PlutusTx.applyCode` LiftU.liftCode sc
+
 {- Note [Redundant arguments to equality benchmarks]
 The arguments for the benchmarks are passed as terms created with `liftCode`.
 But the benchmark still needs to _evaluate_ these terms, which adds overhead that

plutus-benchmark/script-contexts/test/Spec.hs

@@ -40,6 +40,32 @@ testCheckSc2 = testGroup "checkScriptContext2"
           mkCheckScriptContext2Code (mkScriptContext 20)
     ]
 
+testCheckSc3 :: TestTree
+testCheckSc3 = testGroup "checkScriptContext3"
+    [ testCase "succeed on 4" $ assertBool "evaluation failed" $ isEvaluationSuccess $
+        runTermCek $ compiledCodeToTerm $ mkCheckScriptContext3Code (mkScriptContext 4)
+    , testCase "fails on 5" $ assertBool "evaluation succeeded" $ isEvaluationFailure $
+        runTermCek $ compiledCodeToTerm $ mkCheckScriptContext3Code (mkScriptContext 5)
+    , Tx.fitsInto "checkScriptContext3 (size)" (mkCheckScriptContext3Code (mkScriptContext 1)) 300
+    , runTestNested $ Tx.goldenBudget "checkScriptContext3-4" $
+        mkCheckScriptContext3Code (mkScriptContext 4)
+    , runTestNested $ Tx.goldenBudget "checkScriptContext3-20" $
+        mkCheckScriptContext3Code (mkScriptContext 20)
+    ]
+
+testCheckSc4 :: TestTree
+testCheckSc4 = testGroup "checkScriptContext4"
+    [ testCase "succeed on 4" $ assertBool "evaluation failed" $ isEvaluationSuccess $
+          runTermCek $ compiledCodeToTerm $ mkCheckScriptContext4Code (mkScriptContext 4)
+    , testCase "succeed on 5" $ assertBool "evaluation failed" $ isEvaluationSuccess $
+          runTermCek $ compiledCodeToTerm $ mkCheckScriptContext4Code (mkScriptContext 5)
+    , Tx.fitsInto "checkScriptContext4 (size)" (mkCheckScriptContext4Code (mkScriptContext 1)) 100
+    , runTestNested $ Tx.goldenBudget "checkScriptContext4-4" $
+          mkCheckScriptContext4Code (mkScriptContext 4)
+    , runTestNested $ Tx.goldenBudget "checkScriptContext4-20" $
+          mkCheckScriptContext4Code (mkScriptContext 20)
+    ]
+
 testCheckScEquality :: TestTree
 testCheckScEquality = testGroup "checkScriptContextEquality"
     [ runTestNested $ Tx.goldenBudget "checkScriptContexEqualityData-20" $
@@ -55,6 +81,8 @@ allTests =
   testGroup "plutus-benchmark script-contexts tests"
     [ testCheckSc1
     , testCheckSc2
+    , testCheckSc3
+    , testCheckSc4
     , testCheckScEquality
     ]
 

plutus-benchmark/script-contexts/test/checkScriptContexEqualityData-20.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 52948597
-| mem: 167402})
+({cpu: 58790597
+| mem: 192802})

plutus-benchmark/script-contexts/test/checkScriptContext1-20.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 460200997
-| mem: 1473069})
+({cpu: 453599997
+| mem: 1444369})

plutus-benchmark/script-contexts/test/checkScriptContext1-4.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 133868245
-| mem: 431693})
+({cpu: 131315245
+| mem: 420593})

plutus-benchmark/script-contexts/test/checkScriptContext2-20.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 436044997
-| mem: 1387928})
+({cpu: 434871997
+| mem: 1382828})

plutus-benchmark/script-contexts/test/checkScriptContext2-4.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 126999877
-| mem: 407384})
+({cpu: 126194877
+| mem: 403884})

plutus-benchmark/script-contexts/test/checkScriptContext3-20.budget.golden

@@ -0,0 +1,2 @@
+({cpu: 23709589
+| mem: 82043})

plutus-benchmark/script-contexts/test/checkScriptContext3-4.budget.golden

@@ -0,0 +1,2 @@
+({cpu: 6789957
+| mem: 22811})

plutus-benchmark/script-contexts/test/checkScriptContext4-20.budget.golden

@@ -0,0 +1,2 @@
+({cpu: 6775589
+| mem: 28302})

plutus-benchmark/script-contexts/test/checkScriptContext4-4.budget.golden

@@ -0,0 +1,2 @@
+({cpu: 2359589
+| mem: 9102})

plutus-benchmark/script-contexts/test/checkScriptContextEqualityOverhead-20.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 37927100
-| mem: 165000})
+({cpu: 43631100
+| mem: 189800})

plutus-benchmark/script-contexts/test/checkScriptContextEqualityTerm-20.budget.golden

@@ -1,2 +1,2 @@
-({cpu: 835870251
-| mem: 3476246})
+({cpu: 632527251
+| mem: 2592146})

plutus-core/cost-model/budgeting-bench/Benchmarks/Data.hs

@@ -5,7 +5,7 @@ module Benchmarks.Data (makeBenchmarks) where
 import Common
 import Generators
 
-import PlutusCore
+import PlutusCore hiding (Constr)
 import PlutusCore.Data
 
 import Criterion.Main

plutus-core/cost-model/budgeting-bench/Common.hs

@@ -9,15 +9,15 @@
 module Common
 where
 
-import PlutusCore
+import PlutusCore hiding (Constr)
 import PlutusCore.Compiler.Erase
 import PlutusCore.Data
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults
 import PlutusCore.Evaluation.Machine.ExMemory
 import PlutusCore.Evaluation.Machine.MachineParameters
 import PlutusCore.MkPlc
 import PlutusCore.Pretty (Pretty)
-import UntypedPlutusCore as UPLC
+import UntypedPlutusCore as UPLC hiding (Constr)
 import UntypedPlutusCore.Evaluation.Machine.Cek
 
 import Control.DeepSeq (NFData, force)

plutus-core/plutus-core.cabal

@@ -160,6 +160,7 @@ library
     UntypedPlutusCore.Core.Zip
     UntypedPlutusCore.DeBruijn
     UntypedPlutusCore.Evaluation.Machine.Cek
+    UntypedPlutusCore.Evaluation.Machine.Cek.ArgQueue
     UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts
     UntypedPlutusCore.Evaluation.Machine.Cek.Debug.Driver
     UntypedPlutusCore.Evaluation.Machine.Cek.Debug.Internal
@@ -230,6 +231,7 @@ library
     UntypedPlutusCore.Simplify
     UntypedPlutusCore.Size
     UntypedPlutusCore.Subst
+    UntypedPlutusCore.Transform.CaseReduce
     UntypedPlutusCore.Transform.ForceDelay
     UntypedPlutusCore.Transform.Inline
 
@@ -296,6 +298,7 @@ library
     , time
     , transformers
     , unordered-containers
+    , vector
     , witherable
     , word-array                  ^>=1.1
 

plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs

@@ -16,6 +16,7 @@ import PlutusCore.Core
 import PlutusCore.Error
 
 import Control.Monad.Except
+import Data.Foldable (traverse_)
 
 -- | Ensure that all types in the 'Program' are normalized.
 checkProgram
@@ -37,6 +38,8 @@ check (Unwrap _ t)           = check t
 check (LamAbs _ _ ty t)      = normalType ty >> check t
 check (Apply _ t1 t2)        = check t1 >> check t2
 check (TyAbs _ _ _ t)        = check t
+check (Constr _ ty _ es)     = normalType ty >> traverse_ check es
+check (Case _ ty arg cs)     = normalType ty >> check arg >> traverse_ check cs
 check Var{}                  = pure ()
 check Constant{}             = pure ()
 check Builtin{}              = pure ()
@@ -48,6 +51,8 @@ normalType :: Type tyname uni ann -> Either (NormCheckError tyname name uni fun
 normalType (TyFun _ i o)       = normalType i >> normalType o
 normalType (TyForall _ _ _ ty) = normalType ty
 normalType (TyIFix _ pat arg)  = normalType pat >> normalType arg
+normalType (TyProd _ tys)      = traverse_ normalType tys
+normalType (TySum _ tys)       = traverse_ normalType tys
 normalType (TyLam _ _ _ ty)    = normalType ty
 -- See Note [PLC types and universes].
 normalType TyBuiltin{}         = pure ()

plutus-core/plutus-core/src/PlutusCore/Compiler/Erase.hs

@@ -15,6 +15,8 @@ eraseTerm (TyInst ann term _)      = UPLC.Force ann (eraseTerm term)
 eraseTerm (Unwrap _ term)          = eraseTerm term
 eraseTerm (IWrap _ _ _ term)       = eraseTerm term
 eraseTerm (Error ann _)            = UPLC.Error ann
+eraseTerm (Constr ann _ i args)    = UPLC.Constr ann i (fmap eraseTerm args)
+eraseTerm (Case ann _ arg cs)      = UPLC.Case ann (eraseTerm arg) (fmap eraseTerm cs)
 
 eraseProgram :: Program tyname name uni fun ann -> UPLC.Program name uni fun ann
 eraseProgram (Program a v t) = UPLC.Program a v $ eraseTerm t

plutus-core/plutus-core/src/PlutusCore/Core/Instance/Eq.hs

@@ -20,6 +20,7 @@ import PlutusCore.Eq
 import PlutusCore.Name
 import PlutusCore.Rename.Monad
 
+import Data.Foldable (for_)
 import Universe
 
 instance (GEq uni, Eq ann) => Eq (Type TyName uni ann) where
@@ -89,13 +90,25 @@ eqTypeM (TyFun ann1 dom1 cod1) (TyFun ann2 dom2 cod2) = do
 eqTypeM (TyBuiltin ann1 bi1) (TyBuiltin ann2 bi2) = do
     eqM ann1 ann2
     eqM bi1 bi2
+eqTypeM (TyProd ann1 tys1) (TyProd ann2 tys2) = do
+    eqM ann1 ann2
+    case zipExact tys1 tys2 of
+        Just ps -> for_ ps $ \(t1, t2) -> eqTypeM t1 t2
+        Nothing -> empty
+eqTypeM (TySum ann1 tys1) (TySum ann2 tys2) = do
+    eqM ann1 ann2
+    case zipExact tys1 tys2 of
+        Just ps -> for_ ps $ \(t1, t2) -> eqTypeM t1 t2
+        Nothing -> empty
 eqTypeM TyVar{}     _ = empty
 eqTypeM TyLam{}     _ = empty
 eqTypeM TyForall{}  _ = empty
 eqTypeM TyIFix{}    _ = empty
 eqTypeM TyApp{}     _ = empty
 eqTypeM TyFun{}     _ = empty
 eqTypeM TyBuiltin{} _ = empty
+eqTypeM TyProd{} _ = empty
+eqTypeM TySum{} _ = empty
 
 -- See Note [Modulo alpha].
 -- See Note [Scope tracking]
@@ -141,6 +154,20 @@ eqTermM (Constant ann1 con1) (Constant ann2 con2) = do
 eqTermM (Builtin ann1 bi1) (Builtin ann2 bi2) = do
     eqM ann1 ann2
     eqM bi1 bi2
+eqTermM (Constr ann1 ty1 i1 args1) (Constr ann2 ty2 i2 args2) = do
+    eqM ann1 ann2
+    eqTypeM ty1 ty2
+    eqM i1 i2
+    case zipExact args1 args2 of
+        Just ps -> for_ ps $ \(t1, t2) -> eqTermM t1 t2
+        Nothing -> empty
+eqTermM (Case ann1 ty1 a1 cs1) (Case ann2 ty2 a2 cs2) = do
+    eqM ann1 ann2
+    eqTypeM ty1 ty2
+    eqTermM a1 a2
+    case zipExact cs1 cs2 of
+        Just ps -> for_ ps $ \(t1, t2) -> eqTermM t1 t2
+        Nothing -> empty
 eqTermM LamAbs{}   _ = empty
 eqTermM TyAbs{}    _ = empty
 eqTermM IWrap{}    _ = empty
@@ -151,3 +178,5 @@ eqTermM TyInst{}   _ = empty
 eqTermM Var{}      _ = empty
 eqTermM Constant{} _ = empty
 eqTermM Builtin{}  _ = empty
+eqTermM Constr{}  _ = empty
+eqTermM Case{}  _ = empty

plutus-core/plutus-core/src/PlutusCore/Core/Instance/Pretty/Classic.hs

@@ -55,6 +55,10 @@ instance (PrettyClassicBy configName tyname, Pretty (SomeTypeIn uni), Pretty ann
         TyLam ann n k t    ->
             sexp "lam" (consAnnIf config ann
                 [prettyBy config n, prettyBy config k, prettyBy config t])
+        TyProd ann tys    ->
+            sexp "prod" (consAnnIf config ann (fmap (prettyBy config) tys))
+        TySum ann tys    ->
+            sexp "sum" (consAnnIf config ann (fmap (prettyBy config) tys))
 
 instance
         ( PrettyClassicBy configName tyname
@@ -90,6 +94,12 @@ instance
                 [prettyBy config ty1, prettyBy config ty2, prettyBy config t])
         Unwrap ann t ->
             sexp "unwrap" (consAnnIf config ann [prettyBy config t])
+        Constr ann ty i es ->
+            sexp "constr" (consAnnIf config ann ([prettyBy config ty, pretty i ]
+                                                 ++ (fmap (prettyBy config) es)))
+        Case ann ty arg cs ->
+            sexp "case" (consAnnIf config ann ([prettyBy config arg, prettyBy config ty ]
+                                               ++ (fmap (prettyBy config) cs)))
       where
         prettyTypeOf :: Pretty (SomeTypeIn t) => Some (ValueOf t) -> Doc dann
         prettyTypeOf (Some (ValueOf uni _ )) = pretty $ SomeTypeIn uni