Unrestricted force

Don't look here yet. This is an experiment I've wanted to do for a
while, just looking to get some benchmark numbers.

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

@@ -1,3 +1,3 @@
-({ cpu: 37605791908
-| mem: 161972648
+({ cpu: 36552184908
+| mem: 157391748
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 7563493298
-| mem: 28459340
+({ cpu: 7131990298
+| mem: 26583240
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 14229364305
-| mem: 54977742
+({ cpu: 13274289305
+| mem: 50825242
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 191619634648
-| mem: 725849980
+({ cpu: 179471264648
+| mem: 673030980
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 492446997
-| mem: 1613269
+({ cpu: 479244997
+| mem: 1555869
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 141826245
-| mem: 466293
+({ cpu: 138192245
+| mem: 450493
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 438942997
-| mem: 1400528
+({ cpu: 429259997
+| mem: 1358428
 })

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

@@ -1,3 +1,3 @@
-({ cpu: 127689877
-| mem: 410384
+({ cpu: 124998877
+| mem: 398684
 })

plutus-core/plutus-ir/test/datatypes/listMatchEval.golden

@@ -1 +1 @@
-(delay (lam x_0 x_0))
+(lam x_0 x_0)

plutus-core/plutus-ir/test/recursion/even3Eval.golden

@@ -1 +1 @@
-(delay (lam case_True_0 (lam case_False_1 case_False_1)))
+(lam case_True_0 (lam case_False_1 case_False_1))

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs

@@ -702,8 +702,7 @@ enterComputeCek = computeCek (toWordArray 0) where
                 returnCek unbudgetedSteps ctx res
             _ ->
                 throwingWithCause _MachineError BuiltinTermArgumentExpectedMachineError (Just term')
-    forceEvaluate !_ !_ val =
-        throwingDischarged _MachineError NonPolymorphicInstantiationMachineError val
+    forceEvaluate !unbudgetedSteps !ctx val = returnCek unbudgetedSteps ctx val
 
     -- | Apply a function to an argument and proceed.
     -- If the function is a lambda 'lam x ty body' then extend the environment with a binding of @v@

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

@@ -12,5 +12,115 @@ forceDelayCancel = transformOf termSubterms processTerm
 
 processTerm :: Term name uni fun a -> Term name uni fun a
 processTerm = \case
-    Force _ (Delay _ t) -> t
-    t                   -> t
+    Force _ (Delay _ t)          -> t
+    -- TODO: flag to turn this off, see
+    -- Note [Removing delays makes more programs succeed]
+    Delay _ t | canRemoveDelay t -> t
+    Force _ t | canRemoveForce t -> t
+    t                            -> t
+
+{- Note [Removing redundant delays and forces]
+
+We do a few transformations here. The simplest and best is to cancel out
+a force/delay pair. This is a pure win, since it's exactly what the machine
+would do.
+
+The next thing we try and do is to get rid of force/delays that are independently
+pointless. In particular
+- delaying something that does no work does nothing
+- forcing something that cannot be a delay does nothing
+
+So we can remove them in those cases.
+
+However, there are a few wrinkles. The first is that we don't want this to
+cannibalize our opportunities to do force/delay pair cancellations. Consider:
+
+let x = delay (\y . t)
+in force x
+---> (remove delay)
+let x = \y . t
+in force x
+---> (inline)
+force (\y . t)
+
+In this case it's fine because the term _inside_ the delay was something
+that we can remove the force from around (a lambda). But we need to be
+careful that this is always the case. So we require that the set of terms
+that we remove delays from around be a _subset_ of the set of terms that
+we remove forces from around.
+
+The case where this is strange is delay itself. Consider:
+
+let x = delay (delay [f z])
+in force (force x)
+---> (remove delay)
+let x = delay [f z]
+in force (force x)
+---> (inline)
+force (force (delay [f z]))
+---> (force/delay cancel)
+force [f z]
+
+We now can't remove the last force, whereas if we had just
+inlined the first thing we could have removed both by
+repeated force/delay cancellation.
+
+So although it seems like it _should_ be fine to remove a delay
+from around a delay, we don't do this for the above reason.
+In practice this doesn't matter much.
+-}
+
+{- Note [Removing delays makes more programs succeed]
+
+Note that removing redundant delays doesn't quite preserve the
+semantics of the program! It can make some programs that would
+otherwise fail succeed instead, e.g.
+
+let f = delay (\y. t)
+in f x
+
+This would fail with the delay (can't apply a delay!) but will
+succeed if we take it out. That makes this transformation ever
+so slightly questionable, and so we should provide a flag to turn
+it off.
+-}
+
+-- | Can we remove a 'delay' from around this term?
+--
+-- Broadly, this means anything that's a value, but
+-- also this must be a subset of 'canRemoveForce', see
+-- Note [Removing redundant delays and forces] for why.
+canRemoveDelay :: Term name uni fun a -> Bool
+canRemoveDelay = \case
+  LamAbs{}   -> True
+  Constant{} -> True
+  -- You would expect this to be true, since it's a
+  -- value, but that would violate the subset condition.
+  Delay{}    -> False
+  _          -> False
+
+-- | Can we remove a 'force' from around this term?
+--
+-- Broadly, this means anything that we know can't turn
+-- out to be a 'delay' (which would need the 'force').
+canRemoveForce :: Term name uni fun a -> Bool
+canRemoveForce = \case
+  -- Delay is delay
+  Delay{}    -> False
+
+  -- Everything that computes could turn into delay
+
+  -- A variable might be delay, we don't know
+  Var{}      -> False
+  -- An application might compute to anything, including delay
+  Apply{}    -> False
+  -- A force will compute to whatever's inside it,
+  -- which could be a delay
+  Force{}    -> False
+  -- Builtins can't be delay, but they can require forcing
+  Builtin{}  -> False
+
+  -- Everything else can't be delay
+  Constant{} -> True
+  LamAbs{}   -> True
+  Error{}    -> True

plutus-core/untyped-plutus-core/test/Evaluation/Golden/mulInstError3.uplc.golden

@@ -1,3 +1 @@
-(Left An error has occurred:  error:
-Attempted to instantiate a non-polymorphic term.
-Caused by: (con integer 242))
+(Right (con integer 242))

plutus-core/untyped-plutus-core/test/Transform/extraDelays.plc.golden

@@ -1 +1 @@
-(delay (con integer 1))
+(con integer 1)

plutus-tx-plugin/test/Budget/any.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 28136630
-| mem: 110020
+({ cpu: 26641630
+| mem: 103520
 })

plutus-tx-plugin/test/Budget/applicative.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 2023577
-| mem: 8002
+({ cpu: 1862577
+| mem: 7302
 })

plutus-tx-plugin/test/Budget/elem.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 28171990
-| mem: 110020
+({ cpu: 26676990
+| mem: 103520
 })

plutus-tx-plugin/test/Budget/filter.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 28773590
-| mem: 92930
+({ cpu: 27393590
+| mem: 86930
 })

plutus-tx-plugin/test/Budget/find.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 26917630
-| mem: 104720
+({ cpu: 25192630
+| mem: 97220
 })

plutus-tx-plugin/test/Budget/monadicDo.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 2207577
-| mem: 8802
+({ cpu: 2000577
+| mem: 7902
 })

plutus-tx-plugin/test/Budget/patternMatch.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 1540577
-| mem: 5902
+({ cpu: 1425577
+| mem: 5402
 })

plutus-tx-plugin/test/Budget/show.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 9526961630
-| mem: 35235273
+({ cpu: 8910009630
+| mem: 32552873
 })

plutus-tx-plugin/test/Budget/sum.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 23293870
-| mem: 92420
+({ cpu: 22028870
+| mem: 86920
 })

plutus-tx-plugin/test/Budget/toFromData.budget.golden

@@ -1,3 +1,3 @@
-({ cpu: 15479457
-| mem: 51292
+({ cpu: 14950457
+| mem: 48992
 })

plutus-tx-plugin/test/Optimization/maybeFun.plc.golden

@@ -24,13 +24,10 @@
                               [
                                 (lam
                                   arg_0_i0
-                                  (delay
+                                  (lam
+                                    case_Just_i0
                                     (lam
-                                      case_Just_i0
-                                      (lam
-                                        case_Nothing_i0
-                                        [ case_Just_i2 arg_0_i3 ]
-                                      )
+                                      case_Nothing_i0 [ case_Just_i2 arg_0_i3 ]
                                     )
                                   )
                                 )
@@ -51,6 +48,6 @@
         )
       )
     )
-    (delay (delay (lam case_Just_i0 (lam case_Nothing_i0 case_Nothing_i1))))
+    (lam case_Just_i0 (lam case_Nothing_i0 case_Nothing_i1))
   ]
 )