[PLC] [Builtin] [Evaluation] Return unannotated things from the machines

language-plutus-core/common/PlcTestUtils.hs

@@ -60,7 +60,7 @@ runPlc
     :: ( GetProgram a uni, GShow uni, GEq uni, DefaultUni <: uni
        , Closed uni, uni `Everywhere` ExMemoryUsage, uni `Everywhere` PrettyConst, Typeable uni
        )
-    => [a] -> ExceptT SomeException IO (EvaluationResult (Term TyName Name uni ExMemory))
+    => [a] -> ExceptT SomeException IO (EvaluationResult (Plain Term uni))
 runPlc values = do
     ps <- traverse getProgram values
     let p = foldl1 applyProgram ps

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/TypeEvalCheck.hs

@@ -87,11 +87,10 @@ type TypeEvalCheckM uni = Either (TypeEvalCheckError uni)
 -- See Note [Type-eval checking].
 -- | Type check and evaluate a term and check that the expected result is equal to the actual one.
 typeEvalCheckBy
-    :: ( Pretty internal, KnownType (Term TyName Name uni ()) a, GShow uni, GEq uni, DefaultUni <: uni
-       , Closed uni, uni `Everywhere` Eq, uni `Everywhere` PrettyConst
+    :: ( KnownType (Term TyName Name uni ()) a, GShow uni, GEq uni, DefaultUni <: uni
+       , Closed uni, uni `Everywhere` Eq, Pretty internal, PrettyPlc termErr
        )
-    => (Term TyName Name uni () ->
-            Either (EvaluationException (WithMemory Term uni) internal user) (WithMemory Term uni))
+    => (Plain Term uni -> Either (EvaluationException internal user termErr) (Plain Term uni))
        -- ^ An evaluator.
     -> TermOf uni a
     -> TypeEvalCheckM uni (TermOf uni (TypeEvalCheckResult uni))

language-plutus-core/generators/Language/PlutusCore/Generators/Test.hs

@@ -82,12 +82,9 @@ sampleProgramValueGolden folder name genTerm = do
 -- indeed computes to that value according to the provided evaluate.
 propEvaluate
     :: ( uni ~ DefaultUni, KnownType (Term TyName Name uni ()) a
-       , Pretty internal, uni `Everywhere` PrettyConst
+       , Pretty internal, PrettyPlc termErr
        )
-    => (Term TyName Name uni () ->
-            Either
-                (EvaluationException (WithMemory Term uni) internal user)
-                (WithMemory Term uni))
+    => (Plain Term uni -> Either (EvaluationException internal user termErr) (Plain Term uni))
                       -- ^ An evaluator.
     -> TermGen uni a  -- ^ A term/value generator.
     -> Property

language-plutus-core/src/Language/PlutusCore/Constant/Apply.hs

@@ -57,7 +57,7 @@ integerToInt64 = fromIntegral
 -- Checks that the constants are of expected types.
 applyTypeSchemed
     :: forall err m args term res.
-       ( MonadError (ErrorWithCause term err) m, AsUnliftingError err, AsConstAppError err term
+       ( MonadError (ErrorWithCause err term) m, AsUnliftingError err, AsConstAppError err term
        , SpendBudget m term
        )
     => StagedBuiltinName
@@ -102,7 +102,7 @@ applyTypeSchemed name = go where
 -- | Apply a 'TypedBuiltinName' to a list of 'Constant's (unwrapped from 'Value's)
 -- Checks that the constants are of expected types.
 applyTypedBuiltinName
-    :: ( MonadError (ErrorWithCause term err) m, AsUnliftingError err, AsConstAppError err term
+    :: ( MonadError (ErrorWithCause err term) m, AsUnliftingError err, AsConstAppError err term
        , SpendBudget m term
        )
     => TypedBuiltinName term args res
@@ -117,7 +117,7 @@ applyTypedBuiltinName (TypedBuiltinName name schema) =
 -- Checks that the values are of expected types.
 applyBuiltinName
     :: forall m err uni term
-    .  ( MonadError (ErrorWithCause term err) m, AsUnliftingError err, AsConstAppError err term
+    .  ( MonadError (ErrorWithCause err term) m, AsUnliftingError err, AsConstAppError err term
        , SpendBudget m term, HasConstantIn uni term, GShow uni, GEq uni, DefaultUni <: uni
        )
     => BuiltinName -> [term] -> m (ConstAppResult term)

language-plutus-core/src/Language/PlutusCore/Constant/Typed.hs

@@ -224,7 +224,7 @@ instance (HasConstant term, GShow (UniOf term), GEq (UniOf term), UniOf term `In
 -- (or throw an error if the term is not a 'Constant' or the constant is not of the expected type).
 unliftConstant
     :: forall a m term err.
-       (MonadError (ErrorWithCause term err) m, AsUnliftingError err, KnownBuiltinType term a)
+       (MonadError (ErrorWithCause err term) m, AsUnliftingError err, KnownBuiltinType term a)
     => term -> m a
 unliftConstant term = case asConstant term of
     Just (Some (ValueOf uniAct x)) -> do
@@ -302,10 +302,10 @@ class KnownTypeAst (UniOf term) a => KnownType term a where
     -- | Convert a PLC term to the corresponding Haskell value.
     -- The inverse of 'makeKnown'.
     readKnown
-        :: (MonadError (ErrorWithCause term err) m, AsUnliftingError err)
+        :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err)
         => term -> m a
     default readKnown
-        :: (MonadError (ErrorWithCause term err) m, AsUnliftingError err, KnownBuiltinType term a)
+        :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err, KnownBuiltinType term a)
         => term -> m a
     readKnown = unliftConstant
 

language-plutus-core/src/Language/PlutusCore/Evaluation/Machine/Cek.hs

@@ -89,11 +89,11 @@ data CekUserError
 
 -- | The CEK machine-specific 'MachineException'.
 type CekMachineException uni =
-    MachineException (WithMemory Term uni) UnknownDynamicBuiltinNameError
+    MachineException UnknownDynamicBuiltinNameError (WithMemory Term uni)
 
 -- | The CEK machine-specific 'EvaluationException'.
 type CekEvaluationException uni =
-    EvaluationException (WithMemory Term uni) UnknownDynamicBuiltinNameError CekUserError
+    EvaluationException UnknownDynamicBuiltinNameError CekUserError (WithMemory Term uni)
 
 instance Pretty CekUserError where
     pretty (CekOutOfExError (ExRestrictingBudget res) b) =
@@ -245,7 +245,7 @@ substitution, anything).
 -- 4. looks up a variable in the environment and calls 'returnCek' ('Var')
 computeCek
     :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Context uni -> WithMemory Term uni -> CekM uni (WithMemory Term uni)
+    => Context uni -> WithMemory Term uni -> CekM uni (Plain Term uni)
 computeCek con t@(TyInst _ body ty) = do
     spendBudget BTyInst t (ExBudget 1 1) -- TODO
     computeCek (FrameTyInstArg ty : con) body
@@ -279,9 +279,9 @@ computeCek con t@(Var _ varName)   = do
 -- 4. grows the resulting term ('FrameWrap')
 returnCek
     :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Context uni -> WithMemory Value uni -> CekM uni (WithMemory Term uni)
+    => Context uni -> WithMemory Value uni -> CekM uni (Plain Term uni)
 -- Instantiate all the free variable of the resulting term in case there are any.
-returnCek [] res = getVarEnv <&> \varEnv -> dischargeVarEnv varEnv res
+returnCek [] res = getVarEnv <&> \varEnv -> void $ dischargeVarEnv varEnv res
 returnCek (FrameTyInstArg ty : con) fun = instantiateEvaluate con ty fun
 returnCek (FrameApplyArg argVarEnv arg : con) fun = do
     funVarEnv <- getVarEnv
@@ -302,7 +302,7 @@ returnCek (FrameUnwrap : con) dat = case dat of
 -- apply the term to the type via 'TyInst'.
 instantiateEvaluate
     :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Context uni -> Type TyName uni ExMemory -> WithMemory Term uni -> CekM uni (WithMemory Term uni)
+    => Context uni -> Type TyName uni ExMemory -> WithMemory Term uni -> CekM uni (Plain Term uni)
 instantiateEvaluate con _ (TyAbs _ _ _ body) = computeCek con body
 instantiateEvaluate con ty fun
     | isJust $ termAsPrimIterApp fun = returnCek con $ TyInst (memoryUsage () <> memoryUsage fun <> memoryUsage ty) fun ty
@@ -381,7 +381,7 @@ applyEvaluate
     -> Context uni
     -> WithMemory Value uni
     -> WithMemory Value uni
-    -> CekM uni (WithMemory Term uni)
+    -> CekM uni (Plain Term uni)
 applyEvaluate funVarEnv argVarEnv con (LamAbs _ name _ body) arg =
     withVarEnv (extendVarEnv name arg argVarEnv funVarEnv) $ computeCek con body
 applyEvaluate funVarEnv argVarEnv con fun arg = do
@@ -415,7 +415,7 @@ runCek
     -> ExBudgetMode
     -> CostModel
     -> Plain Term uni
-    -> (Either (CekEvaluationException uni) (WithMemory Term uni), ExBudgetState)
+    -> (Either (CekEvaluationException uni) (Plain Term uni), ExBudgetState)
 runCek means mode params term =
     runCekM (CekEnv means mempty mode params)
             (ExBudgetState mempty mempty)
@@ -434,7 +434,7 @@ runCekCounting
     => DynamicBuiltinNameMemoryMeanings uni
     -> CostModel
     -> Plain Term uni
-    -> (Either (CekEvaluationException uni) (WithMemory Term uni), ExBudgetState)
+    -> (Either (CekEvaluationException uni) (Plain Term uni), ExBudgetState)
 runCekCounting means = runCek means Counting
 
 -- | Evaluate a term using the CEK machine.
@@ -443,7 +443,7 @@ evaluateCek
     => DynamicBuiltinNameMemoryMeanings uni
     -> CostModel
     -> Plain Term uni
-    -> Either (CekEvaluationException uni) (WithMemory Term uni)
+    -> Either (CekEvaluationException uni) (Plain Term uni)
 evaluateCek means params = fst . runCekCounting means params
 
 -- | Evaluate a term using the CEK machine. May throw a 'CekMachineException'.
@@ -454,16 +454,17 @@ unsafeEvaluateCek
     => DynamicBuiltinNameMemoryMeanings uni
     -> CostModel
     -> Plain Term uni
-    -> EvaluationResult (Term TyName Name uni ExMemory)
+    -> EvaluationResult (Plain Term uni)
 unsafeEvaluateCek means params = either throw id . extractEvaluationResult . evaluateCek means params
 
 -- | Unlift a value using the CEK machine.
 readKnownCek
     :: ( GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage
-       , KnownType (WithMemory Term uni) a
+       , KnownType (Plain Term uni) a
        )
     => DynamicBuiltinNameMemoryMeanings uni
     -> CostModel
     -> Plain Term uni
     -> Either (CekEvaluationException uni) a
-readKnownCek means params = evaluateCek means params >=> readKnown
+-- Calling 'withMemory' just to unify the monads that 'readKnown' and the CEK machine run in.
+readKnownCek means params = evaluateCek means params >=> first (fmap withMemory) . readKnown

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

@@ -7,9 +7,9 @@
 {-# LANGUAGE TypeOperators         #-}
 
 module Language.PlutusCore.Evaluation.Machine.Ck
-    ( CkMachineException
+    ( EvaluationResult (..)
     , CkEvaluationException
-    , EvaluationResult (..)
+    , CkM
     , evaluateCk
     , unsafeEvaluateCk
     ) where
@@ -21,7 +21,7 @@ import           Language.PlutusCore.Core
 import           Language.PlutusCore.Evaluation.Machine.ExBudgeting
 import           Language.PlutusCore.Evaluation.Machine.ExBudgetingDefaults
 import           Language.PlutusCore.Evaluation.Machine.Exception
-import           Language.PlutusCore.Evaluation.Machine.ExMemory
+import           Language.PlutusCore.Evaluation.Machine.ExMemory            (Plain)
 import           Language.PlutusCore.Evaluation.Result
 import           Language.PlutusCore.Name
 import           Language.PlutusCore.Pretty                                 (PrettyConst)
@@ -35,27 +35,23 @@ data NoDynamicBuiltinNamesMachineError
     = NoDynamicBuiltinNamesMachineError
     deriving (Show, Eq)
 
--- | The CK machine-specific 'MachineException'.
-type CkMachineException uni =
-    MachineException (WithMemory Term uni) NoDynamicBuiltinNamesMachineError
-
 -- | The CK machine-specific 'EvaluationException'.
 type CkEvaluationException uni =
-    EvaluationException (WithMemory Term uni) NoDynamicBuiltinNamesMachineError ()
+    EvaluationException NoDynamicBuiltinNamesMachineError () (Plain Term uni)
 
 type CkM uni = Either (CkEvaluationException uni)
 
-instance SpendBudget (CkM uni) (Term TyName Name uni ExMemory) where
+instance SpendBudget (CkM uni) (Term TyName Name uni ()) where
     spendBudget _ _ _ = pure ()
-    feedBudgeter exF  = pure . exF . termAnn
+    feedBudgeter exF _ = pure $ exF 0
     builtinCostParams = pure defaultCostModel
 
 data Frame uni
-    = FrameApplyFun (WithMemory Value uni)                                       -- ^ @[V _]@
-    | FrameApplyArg (WithMemory Term uni)                                        -- ^ @[_ N]@
-    | FrameTyInstArg (Type TyName uni ExMemory)                                  -- ^ @{_ A}@
-    | FrameUnwrap                                                                -- ^ @(unwrap _)@
-    | FrameIWrap ExMemory (Type TyName uni ExMemory) (Type TyName uni ExMemory)  -- ^ @(iwrap A B _)@
+    = FrameApplyFun (Plain Value uni)                          -- ^ @[V _]@
+    | FrameApplyArg (Plain Term uni)                           -- ^ @[_ N]@
+    | FrameTyInstArg (Type TyName uni ())                      -- ^ @{_ A}@
+    | FrameUnwrap                                              -- ^ @(unwrap _)@
+    | FrameIWrap () (Type TyName uni ()) (Type TyName uni ())  -- ^ @(iwrap A B _)@
 
 type Context uni = [Frame uni]
 
@@ -93,19 +89,19 @@ substituteDb varFor new = go where
 -- > s ▷ con cn     ↦ s ◁ con cn
 -- > s ▷ error A    ↦ ◆
 (|>)
-    :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Context uni -> WithMemory Term uni -> CkM uni (WithMemory Term uni)
-stack |> TyInst _ fun ty        = FrameTyInstArg ty      : stack |> fun
-stack |> Apply _ fun arg        = FrameApplyArg arg      : stack |> fun
-stack |> IWrap ann pat arg term = FrameIWrap ann pat arg : stack |> term
-stack |> Unwrap _ term          = FrameUnwrap            : stack |> term
-stack |> tyAbs@TyAbs{}          = stack <| tyAbs
-stack |> lamAbs@LamAbs{}        = stack <| lamAbs
-stack |> bi@Builtin{}           = stack <| bi
-stack |> constant@Constant{}    = stack <| constant
-_     |> err@Error{}            =
+    :: (GShow uni, GEq uni, DefaultUni <: uni)
+    => Context uni -> Plain Term uni -> CkM uni (Plain Term uni)
+stack |> TyInst _ fun ty      = FrameTyInstArg ty     : stack |> fun
+stack |> Apply _ fun arg      = FrameApplyArg arg     : stack |> fun
+stack |> IWrap _ pat arg term = FrameIWrap () pat arg : stack |> term
+stack |> Unwrap _ term        = FrameUnwrap           : stack |> term
+stack |> tyAbs@TyAbs{}        = stack <| tyAbs
+stack |> lamAbs@LamAbs{}      = stack <| lamAbs
+stack |> bi@Builtin{}         = stack <| bi
+stack |> constant@Constant{}  = stack <| constant
+_     |> err@Error{}          =
     throwingWithCause _EvaluationError (UserEvaluationError ()) $ Just err
-_     |> var@Var{}              =
+_     |> var@Var{}            =
     throwingWithCause _MachineError OpenTermEvaluatedMachineError $ Just var
 
 -- | The returning part of the CK machine. Rules are as follows:
@@ -119,8 +115,8 @@ _     |> var@Var{}              =
 -- > s , (wrap α S _)    ◁ V          ↦ s ◁ wrap α S V
 -- > s , (unwrap _)      ◁ wrap α A V ↦ s ◁ V
 (<|)
-    :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Context uni -> WithMemory Value uni -> CkM uni (WithMemory Term uni)
+    :: (GShow uni, GEq uni, DefaultUni <: uni)
+    => Context uni -> Plain Value uni -> CkM uni (Plain Term uni)
 []                             <| term    = pure term
 FrameTyInstArg ty      : stack <| fun     = instantiateEvaluate stack ty fun
 FrameApplyArg arg      : stack <| fun     = FrameApplyFun fun : stack |> arg
@@ -135,14 +131,14 @@ FrameUnwrap            : stack <| wrapped = case wrapped of
 -- iterated application of a 'BuiltinName' to a list of 'Value's and, if succesful,
 -- apply the term to the type via 'TyInst'.
 instantiateEvaluate
-    :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
+    :: (GShow uni, GEq uni, DefaultUni <: uni)
     => Context uni
-    -> Type TyName uni ExMemory
-    -> WithMemory Term uni
-    -> CkM uni (WithMemory Term uni)
+    -> Type TyName uni ()
+    -> Plain Term uni
+    -> CkM uni (Plain Term uni)
 instantiateEvaluate stack _  (TyAbs _ _ _ body) = stack |> body
 instantiateEvaluate stack ty fun
-    | isJust $ termAsPrimIterApp fun = stack <| TyInst (memoryUsage ()) fun ty
+    | isJust $ termAsPrimIterApp fun = stack <| TyInst () fun ty
     | otherwise                      =
           throwingWithCause _MachineError NonPrimitiveInstantiationMachineError $ Just fun
 
@@ -152,14 +148,14 @@ instantiateEvaluate stack ty fun
 -- If succesful, proceed with either this same term or with the result of the computation
 -- depending on whether 'BuiltinName' is saturated or not.
 applyEvaluate
-    :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
+    :: (GShow uni, GEq uni, DefaultUni <: uni)
     => Context uni
-    -> WithMemory Value uni
-    -> WithMemory Value uni
-    -> CkM uni (WithMemory Term uni)
+    -> Plain Value uni
+    -> Plain Value uni
+    -> CkM uni (Plain Term uni)
 applyEvaluate stack (LamAbs _ name _ body) arg = stack |> substituteDb name arg body
 applyEvaluate stack fun                    arg =
-    let term = Apply (memoryUsage ()) fun arg in
+    let term = Apply () fun arg in
         case termAsPrimIterApp term of
             Nothing ->
                 throwingWithCause _MachineError NonPrimitiveApplicationMachineError $ Just term
@@ -174,7 +170,7 @@ applyEvaluate stack fun                    arg =
                     ConstAppStuck       -> stack <| term
 
 
--- | Evaluate a term using the CK machine. May throw a 'CkMachineException'.
+-- | Evaluate a term using the CK machine. May throw a 'CkEvaluationException'.
 -- This differs from the spec version: we do not have the following rule:
 --
 -- > s , {_ A} ◁ F ↦ s ◁ W  -- Fully saturated constant, {F A} ~> W.
@@ -183,14 +179,14 @@ applyEvaluate stack fun                    arg =
 -- unaffected by types as it supports full type erasure, hence @{F A}@ can never compute
 -- if @F@ does not compute, so we simply do not introduce a rule that can't possibly fire.
 evaluateCk
-    :: (GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage)
-    => Plain Term uni -> Either (CkEvaluationException uni) (WithMemory Term uni)
-evaluateCk term = [] |> withMemory term
+    :: (GShow uni, GEq uni, DefaultUni <: uni)
+    => Plain Term uni -> Either (CkEvaluationException uni) (Plain Term uni)
+evaluateCk term = [] |> term
 
--- | Evaluate a term using the CK machine. May throw a 'CkMachineException'.
+-- | Evaluate a term using the CK machine. May throw a 'CkEvaluationException'.
 unsafeEvaluateCk
-    :: ( GShow uni, GEq uni, DefaultUni <: uni, Closed uni, uni `Everywhere` ExMemoryUsage
+    :: ( GShow uni, GEq uni, DefaultUni <: uni, Closed uni
        , Typeable uni, uni `Everywhere` PrettyConst
        )
-    => Plain Term uni -> EvaluationResult (Term TyName Name uni ExMemory)
+    => Plain Term uni -> EvaluationResult (Plain Term uni)
 unsafeEvaluateCk = either throw id . extractEvaluationResult . evaluateCk