[Builtins] Remove 'HeadSpine' from 'BuiltinRuntime' (#7211)

This removes `HeadSpine` from `BuiltinRuntime` now that we don't need it for pattern matching builtins (because they're removed).

Author: effectfully

plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs

@@ -346,8 +346,8 @@ deriving via PrettyCommon (HeadSpine a b)
 class uni ~ UniOf val => MakeKnownIn uni val a where
     -- | Convert a Haskell value to the corresponding PLC value.
     -- The inverse of 'readKnown'.
-    makeKnown :: a -> BuiltinResult (HeadSpine val val)
-    default makeKnown :: KnownBuiltinType val a => a -> BuiltinResult (HeadSpine val val)
+    makeKnown :: a -> BuiltinResult val
+    default makeKnown :: KnownBuiltinType val a => a -> BuiltinResult val
     -- Everything on evaluation path has to be strict in production, so in theory we don't need to
     -- force anything here. In practice however all kinds of weird things happen in tests and @val@
     -- can be non-strict enough to cause trouble here, so we're forcing the argument. Looking at the
@@ -356,7 +356,7 @@ class uni ~ UniOf val => MakeKnownIn uni val a where
     --
     -- Note that the value is only forced to WHNF, so care must be taken to ensure that every value
     -- of a type from the universe gets forced to NF whenever it's forced to WHNF.
-    makeKnown x = pure . HeadOnly . fromValue $! x
+    makeKnown x = pure . fromValue $! x
     {-# INLINE makeKnown #-}
 
 type MakeKnown val = MakeKnownIn (UniOf val) val
@@ -374,7 +374,7 @@ class uni ~ UniOf val => ReadKnownIn uni val a where
 type ReadKnown val = ReadKnownIn (UniOf val) val
 
 -- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
-makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult (HeadSpine val val)
+makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
 makeKnownOrFail x = case makeKnown x of
     BuiltinSuccess val           -> EvaluationSuccess val
     BuiltinSuccessWithLogs _ val -> EvaluationSuccess val
@@ -420,21 +420,17 @@ instance
     {-# INLINE readKnown #-}
 
 instance HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) where
-    makeKnown = coerceArg $ pure . HeadOnly . fromConstant
+    makeKnown = coerceArg $ pure . fromConstant
     {-# INLINE makeKnown #-}
 
 instance HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) where
     readKnown = coerceVia (fmap SomeConstant .) asConstant
     {-# INLINE readKnown #-}
 
 instance uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) where
-    makeKnown = coerceArg $ pure . HeadOnly
+    makeKnown = coerceArg pure
     {-# INLINE makeKnown #-}
 
 instance uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) where
     readKnown = coerceArg pure
     {-# INLINE readKnown #-}
-
-instance uni ~ UniOf val => MakeKnownIn uni val (Opaque (HeadSpine val val) rep) where
-    makeKnown = coerceArg pure
-    {-# INLINE makeKnown #-}

plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs

@@ -30,7 +30,7 @@ import NoThunks.Class
 -- Evaluators that ignore the entire concept of costing (e.g. the CK machine) may of course force
 -- the result of the builtin application unconditionally.
 data BuiltinRuntime val
-    = BuiltinCostedResult ExBudgetStream ~(BuiltinResult (HeadSpine val val))
+    = BuiltinCostedResult ExBudgetStream ~(BuiltinResult val)
     | BuiltinExpectArgument (val -> BuiltinRuntime val)
     | BuiltinExpectForce (BuiltinRuntime val)
 

plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs

@@ -56,7 +56,6 @@ import GHC.Types (Int (..))
 import NoThunks.Class (NoThunks)
 import Prettyprinter (viaShow)
 
--- See Note [Pattern matching on built-in types].
 -- TODO: should we have the commonest built-in functions at the front to have more compact encoding?
 -- | Default built-in functions.
 --
@@ -111,7 +110,7 @@ data DefaultFun
     | TailList
     | NullList
     -- Data
-    -- See Note [Pattern matching on built-in types].
+    -- See Note [Legacy pattern matching on built-in types].
     -- It is convenient to have a "choosing" function for a data type that has more than two
     -- constructors to get pattern matching over it and we may end up having multiple such data
     -- types, hence we include the name of the data type as a suffix.
@@ -941,82 +940,10 @@ goes without saying that this is not supposed to be done.
 
 So overall one needs to be very careful when defining built-in functions that have explicit
 'Opaque' and 'SomeConstant' arguments. Expressiveness doesn't come for free.
-
-Read Note [Pattern matching on built-in types] next.
--}
-
-{- Note [Pattern matching on built-in types]
-Pattern matching over an enumeration built-in type ('Void', 'Unit', 'Bool' etc) is trivially
-implementable, see the 'IfThenElse' example in Note [How to add a built-in function: simple cases].
-Not so much for algebraic data types with at least one constructor carrying some kind of content.
-For example the @(:)@ constructor of @[a]@ has two arguments (an @a@ and a @[a]@) and all
-constructors of 'Data' carry something (e.g. 'I' carries an 'Integer' and 'Constr' carries an
-@Integer@ and a @[Data]@).
-
-In Haskell we'd represent the pattern matching function for lists as follows:
-
-    caseList f z xs0 = case xs0 of
-       []   -> z
-       x:xs -> f x xs
-
-but in the denotation of a built-in function all those @f@, @z@ and @xs0@ are of type @val@, i.e.
-the type of values that the given evaluator uses (e.g. 'CkValue' for the CK machine or 'CekValue'
-for the CEK machine) and we don't know to apply one @val@ to another. We could try to constrain
-@val@ to implement some kind of "apply" function or try to somehow "parse" it into Haskell so that
-it becomes @val -> val@, but even if there was a way of doing either thing, it would be very
-complex and, more importantly, it's just not the job of the builtins machinery to evaluate such
-applications, it's what the actual evaluator is supposed to do.
-
-Hence we employ a very simple strategy: whenever we want to return an iterated application of a
-@val@ to a bunch of @val@s from a built-in function, we just construct it as is without trying to
-evaluate it and let the evaluator perform all the necessary reductions.
-
-So if you want to return an application from a built-in function, you need to use 'HeadSpine' at the
-type level and 'headSpine' at the term level, where the latter has the following signature:
-
-    headSpineOpaque :: Opaque val asToB -> [val] -> Opaque (MonoHeadSpine val) b
-
-'headSpine' takes the head of the application, i.e. a function from @a0@, @a1@ ... @an@ to @b@, and
-applies it to a list of values of respective types, returning a `b`. Whether types match or not is
-not checked, since that would be hard and largely pointless, so don't make mistakes.
-
-Back to the pattern matcher for lists:
-
-    caseList f z xs0 = case xs0 of
-       []   -> z
-       x:xs -> f x xs
-
-Here's how we can define it as a built-in function using 'headSpine':
-
-    toBuiltinMeaning _ver CaseList =
-        let caseListDenotation
-                :: Opaque val b
-                -> Opaque val (a -> [a] -> b)
-                -> SomeConstant uni [a]
-                -> BuiltinResult (Opaque (MonoHeadSpine val) b)
-            caseListDenotation z f (SomeConstant (Some (ValueOf uniListA xs0))) = do
-                case uniListA of
-                    DefaultUniList uniA -> pure $ case xs0 of
-                        []     -> headSpineOpaque z []                                             -- [1]
-                        x : xs -> headSpineOpaque f [fromValueOf uniA x, fromValueOf uniListA xs]  -- [2]
-                    _ ->
-                        throwError $ structuralUnliftingError "Expected a list but got something else"
-            {-# INLINE caseListDenotation #-}
-        in makeBuiltinMeaning
-            caseListDenotation
-            <costingFunction>
-
-All the unlifting logic is the same as with, say, 'NullList' from
-Note [How to add a built-in function: complicated cases], the only things that are different are [1]
-and [2]. In [2] we have an iterated application of the given function @f@ to the head of the list
-@x@ (lifted from a constant value to @val@ via 'fromValueOf') and the tail of the list @xs@ (lifted
-to @val@ the same way). In [1] we return the given @z@, but since we need to return a 'HeadSpine'
-(required by [2]), we have to use 'headSpine' just like in [2] except with an empty spine, since @z@
-isn't applied to anything.
 -}
 
 {- Note [Representable built-in functions over polymorphic built-in types]
-In Note [Pattern matching on built-in types] we discussed how general higher-order polymorphic
+Note [Legacy pattern matching on built-in types] discusses how general higher-order polymorphic
 built-in functions are troubling, but polymorphic built-in functions can be troubling even in
 the first-order case. In a Plutus program we always pair constants of built-in types with their
 tags from the universe, which means that in order to produce a constant embedded into a program
@@ -1103,17 +1030,6 @@ throw an "operational" evaluation error). Please respect the distinction when ad
 functions.
 -}
 
--- | Take a function and a list of arguments and apply the former to the latter.
-headSpineOpaque :: Opaque val asToB -> [val] -> Opaque (MonoHeadSpine val) b
-headSpineOpaque (Opaque f) = Opaque . \case
-    []      -> HeadOnly f
-    x0 : xs ->
-        -- It's critical to use 'foldr' here, so that deforestation kicks in.
-        -- See Note [Definition of foldl'] in "GHC.List" and related Notes around for an explanation
-        -- of the trick.
-        HeadSpine f $ foldr (\x2 r x1 -> SpineCons x1 $ r x2) SpineLast xs x0
-{-# INLINE headSpineOpaque #-}
-
 instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
     type CostingPart uni DefaultFun = BuiltinCostModel
 
@@ -2346,7 +2262,7 @@ instance Flat DefaultFun where
 
 {- Note [Legacy pattern matching on built-in types]
 We used to only support direct pattern matching on enumeration types: 'Void', 'Unit', 'Bool'
-etc. This is because it was impossible to return an iterated application from a built-in function.
+etc. This is because it was impossible to 'Case' on a value of a built-in type.
 
 So e.g. if we wanted to add the following data type:
 
@@ -2413,5 +2329,5 @@ concerns are omitted for clarity):
 which, for example, evaluates to @fMap es@ when @d@ is @Map es@
 
 We decided to handle lists the same way by using @chooseList@ rather than @null@ for consistency,
-before introduction of pattern matching builtins.
+before introduction of casing on values of built-in types.
 -}

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs

@@ -251,27 +251,9 @@ FrameCase cs : stack <| e = case e of
             Right (HeadSpine f xs) -> transferConstantSpine xs stack |> f
     _ -> throwErrorWithCause (StructuralError NonConstrScrutinizedMachineError) $ ckValueToTerm e
 
--- | Transfers a 'Spine' onto the stack. The first argument will be at the top of the stack.
---
--- >>> import PlutusCore.Default
--- >>> import PlutusCore.Builtin
--- >>> transferValueSpine (SpineCons (fromValue (1 :: Integer)) (SpineLast (fromValue (2 :: Integer)))) [FrameUnwrap :: Frame DefaultUni DefaultFun]
--- [FrameAwaitFunValue (VCon (Some (ValueOf DefaultUniInteger 1))),FrameAwaitFunValue (VCon (Some (ValueOf DefaultUniInteger 2))),FrameUnwrap]
-transferValueSpine :: Spine (CkValue uni fun) -> Context uni fun -> Context uni fun
-transferValueSpine args ctx = foldr ((:) . FrameAwaitFunValue) ctx args
-
 transferConstantSpine :: Spine (Some (ValueOf uni)) -> Context uni fun -> Context uni fun
 transferConstantSpine args ctx = foldr ((:) . FrameAwaitFunValue . VCon) ctx args
 
--- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with
--- the returning phase of the CK machine, i.e. @<|@.
-returnCkHeadSpine
-    :: Context uni fun
-    -> HeadSpine (CkValue uni fun) (CkValue uni fun)
-    -> CkM uni fun s (Term TyName Name uni fun ())
-returnCkHeadSpine stack (HeadOnly  x)    = stack <| x
-returnCkHeadSpine stack (HeadSpine f xs) = transferValueSpine xs stack <| f
-
 -- | Take a possibly partial builtin application and
 --
 -- - either create a 'CkValue' by evaluating the application if it's saturated (emitting logs, if
@@ -286,9 +268,9 @@ evalBuiltinApp
     -> CkM uni fun s (Term TyName Name uni fun ())
 evalBuiltinApp stack term runtime = case runtime of
     BuiltinCostedResult _ getFXs -> case getFXs of
-        BuiltinSuccess fXs              -> returnCkHeadSpine stack fXs
-        BuiltinSuccessWithLogs logs fXs -> emitCkM logs *> returnCkHeadSpine stack fXs
-        BuiltinFailure logs err         -> emitCkM logs *> throwBuiltinErrorWithCause term err
+        BuiltinSuccess y              -> stack <| y
+        BuiltinSuccessWithLogs logs y -> emitCkM logs *> (stack <| y)
+        BuiltinFailure logs err       -> emitCkM logs *> throwBuiltinErrorWithCause term err
     _ -> stack <| VBuiltin term runtime
 
 -- | Instantiate a term with a type and proceed.

plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/List.hs

@@ -31,7 +31,6 @@ import PlutusCore.StdLib.Data.Unit
 list :: uni `HasTypeLevel` [] => Type tyname uni ()
 list = mkTyBuiltin @_ @[] ()
 
--- See Note [Pattern matching on built-in types].
 -- | Pattern matching on built-in lists. @matchList {a} xs@ on built-in lists is
 -- equivalent to @unwrap xs@ on lists defined in PLC itself (hence why we bind @r@ after @xs@).
 --

plutus-core/plutus-core/test/Evaluation/Spec.hs

@@ -123,7 +123,7 @@ prop_builtinEvaluation ::
     -- outcome, and decides whether to pass or fail the property.
     (fun ->
         [Term uni fun] ->
-        Either SomeException (BuiltinResult (MonoHeadSpine (Term uni fun))) ->
+        Either SomeException (BuiltinResult (Term uni fun)) ->
         PropertyT IO ()) ->
     Property
 prop_builtinEvaluation runtimes bn mkGen f = property $ do
@@ -132,9 +132,9 @@ prop_builtinEvaluation runtimes bn mkGen f = property $ do
         eval ::
             [Term uni fun] ->
             BuiltinRuntime (Term uni fun) ->
-            BuiltinResult (MonoHeadSpine (Term uni fun))
-        eval [] (BuiltinCostedResult _ getFxs) =
-            getFxs
+            BuiltinResult (Term uni fun)
+        eval [] (BuiltinCostedResult _ y) =
+            y
         eval (arg : args) (BuiltinExpectArgument toRuntime) =
             eval args (toRuntime arg)
         eval args (BuiltinExpectForce runtime) =

plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs

@@ -11,7 +11,6 @@ module PlutusIR.Transform.EvaluateBuiltins
     ) where
 
 import PlutusCore.Builtin
-import PlutusCore.MkPlc (headSpineToTermNoAnn)
 import PlutusIR.Contexts
 import PlutusIR.Core
 
@@ -56,19 +55,18 @@ evaluateBuiltins preserveLogging binfo costModel = transformOf termSubterms proc
       -> Maybe (Term tyname name uni fun ())
     eval (BuiltinCostedResult _ getFXs) AppContextEnd =
         case getFXs of
-            BuiltinSuccess fXs -> Just $ headSpineToTermNoAnn fXs
+            BuiltinSuccess y           -> Just y
             -- Evaluates successfully, but does logging. If we're being conservative
             -- then we should leave these in, so we don't remove people's logging!
             -- Otherwise `trace "hello" x` is a prime candidate for evaluation!
-            BuiltinSuccessWithLogs _ fXs ->
-                if preserveLogging then Nothing else Just $ headSpineToTermNoAnn fXs
+            BuiltinSuccessWithLogs _ y -> if preserveLogging then Nothing else Just y
             -- Evaluation failure. This can mean that the evaluation legitimately
             -- failed (e.g. `divideInteger 1 0`), or that it failed because the
             -- argument terms are not currently in the right form (because they're
             -- not evaluated, we're in the middle of a term here!). Since we can't
             -- distinguish these, we have to assume it's the latter case and just leave
             -- things alone.
-            BuiltinFailure{} -> Nothing
+            BuiltinFailure{}           -> Nothing
     eval (BuiltinExpectArgument toRuntime) (TermAppContext arg _ ctx) =
         -- Builtin evaluation does not work with annotations, so we have to throw
         -- the argument annotation away here

plutus-core/testlib/PlutusCore/Generators/Hedgehog/Test.hs

@@ -115,5 +115,5 @@ propEvaluate eval genTermOfTbv = withTests 200 . property $ do
         Left (TypeEvalCheckErrorException err)             -> fail err
         Left (TypeEvalCheckErrorIllEvaled expected actual) ->
             -- Ditto.
-            ShowPretty expected === ShowPretty (fmap HeadOnly actual)
+            ShowPretty expected === ShowPretty actual
         Right _                                            -> return ()

plutus-core/testlib/PlutusCore/Generators/Hedgehog/TypeEvalCheck.hs

@@ -51,7 +51,7 @@ data TypeEvalCheckError uni fun
           !(Normalized (Type TyName uni ()))
     | TypeEvalCheckErrorException !String
     | TypeEvalCheckErrorIllEvaled
-          !(EvaluationResult (MonoHeadSpine (Term TyName Name uni fun ())))
+          !(EvaluationResult (Term TyName Name uni fun ()))
           !(EvaluationResult (Term TyName Name uni fun ()))
       -- ^ The former is an expected result of evaluation, the latter -- is an actual one.
 
@@ -65,7 +65,6 @@ data TypeEvalCheckResult uni fun = TypeEvalCheckResult
 
 instance ( PrettyBy config (Type TyName uni ())
          , PrettyBy config (Term TyName Name uni fun ())
-         , PrettyBy config (MonoHeadSpine (Term TyName Name uni fun ()))
          , PrettyBy config (Error uni fun ())
          ) => PrettyBy config (TypeEvalCheckError uni fun) where
     prettyBy config (TypeEvalCheckErrorIllFormed err)             =
@@ -105,7 +104,7 @@ typeEvalCheckBy eval (TermOf term (x :: a)) = TermOf term <$> do
     if tyExpected == tyActual
         then case splitStructuralOperational $ eval term of
                 Right valActual ->
-                    if valExpected == fmap HeadOnly valActual
+                    if valExpected == valActual
                         then return $ TypeEvalCheckResult tyExpected valActual
                         else throwError $ TypeEvalCheckErrorIllEvaled valExpected valActual
                 Left exc        -> throwError $ TypeEvalCheckErrorException $ show exc

plutus-core/testlib/PlutusCore/Generators/Hedgehog/TypedBuiltinGen.hs

@@ -67,9 +67,7 @@ attachCoercedTerm a = do
             [ "Got 'EvaluationFailure' when generating a value of a built-in type: "
             , render $ prettyConst botRenderContext x
             ]
-        EvaluationSuccess res -> case res of
-            HeadOnly v -> pure $ TermOf v x
-            _          -> fail "Iterated application is not supported"
+        EvaluationSuccess res -> pure $ TermOf res x
 
 -- | Update a typed built-ins generator by overwriting the generator for a certain built-in.
 updateTypedBuiltinGen