[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))
@@ -100,7 +99,7 @@ typeEvalCheckBy eval (TermOf term x) = TermOf term <$> do
     let valExpected = case makeKnown x of
             Error _ _ -> EvaluationFailure
             t         -> EvaluationSuccess t
-    fmap (TypeEvalCheckResult termTy) $ case fmap void <$> extractEvaluationResult (eval term) of
+    fmap (TypeEvalCheckResult termTy) $ case extractEvaluationResult (eval term) of
         Right valActual
             | valExpected == valActual -> return valActual
             | otherwise                ->

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/Function.hs

@@ -13,7 +13,6 @@ module Language.PlutusCore.Constant.Function
 import           Language.PlutusCore.Constant.Typed
 import           Language.PlutusCore.Core
 import           Language.PlutusCore.Name
-import           Language.PlutusCore.Quote
 
 import qualified Data.Map                           as Map
 import           Data.Proxy
@@ -23,16 +22,14 @@ import           GHC.TypeLits
 -- | Convert a 'TypeScheme' to the corresponding 'Type'.
 -- Basically, a map from the PHOAS representation to the FOAS one.
 typeSchemeToType :: UniOf term ~ uni => TypeScheme term as r -> Type TyName uni ()
-typeSchemeToType = runQuote . go 0 where
-    go :: UniOf term ~ uni => Int -> TypeScheme term as r -> Quote (Type TyName uni ())
-    go _ (TypeSchemeResult pR)          = pure $ toTypeAst pR
-    go i (TypeSchemeArrow pA schB)      = TyFun () (toTypeAst pA) <$> go i schB
-    go i (TypeSchemeAllType proxy schK) = case proxy of
-        (_ :: Proxy '(text, uniq)) -> do
-            let text = Text.pack $ symbolVal @text Proxy
-                uniq = fromIntegral $ natVal @uniq Proxy
-                a    = TyName $ Name text $ Unique uniq
-            TyForall () a (Type ()) <$> go i (schK Proxy)
+typeSchemeToType (TypeSchemeResult pR)          = toTypeAst pR
+typeSchemeToType (TypeSchemeArrow pA schB)      = TyFun () (toTypeAst pA) $ typeSchemeToType schB
+typeSchemeToType (TypeSchemeAllType proxy schK) = case proxy of
+    (_ :: Proxy '(text, uniq)) ->
+        let text = Text.pack $ symbolVal @text Proxy
+            uniq = fromIntegral $ natVal @uniq Proxy
+            a    = TyName $ Name text $ Unique uniq
+        in TyForall () a (Type ()) $ typeSchemeToType (schK Proxy)
 
 -- | Extract the 'TypeScheme' from a 'DynamicBuiltinNameMeaning' and
 -- convert it to the corresponding 'Type'.

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

@@ -61,6 +61,8 @@ infixr 9 `TypeSchemeArrow`
 
 type family UniOf a :: * -> *
 
+type instance UniOf (Term tyname name uni ann) = uni
+
 -- | Type schemes of primitive operations.
 -- @as@ is a list of types of arguments, @r@ is the resulting type.
 -- E.g. @Char -> Bool -> Integer@ is encoded as @TypeScheme term [Char, Bool] Integer@.
@@ -214,17 +216,11 @@ newtype Opaque term (text :: Symbol) (unique :: Nat) = Opaque
     { unOpaque :: term
     } deriving newtype (Pretty)
 
--- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
-class    (HasConstant term, GShow (UniOf term), GEq (UniOf term), UniOf term `Includes` a) =>
-            KnownBuiltinType term a
-instance (HasConstant term, GShow (UniOf term), GEq (UniOf term), UniOf term `Includes` a) =>
-            KnownBuiltinType term a
-
 -- | Extract the 'Constant' from a 'Term'
 -- (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
@@ -267,11 +263,9 @@ instance ToAnnotation uni () where
 
 
 
-type instance UniOf (Term tyname name uni ann) = uni
-
 class HasConstant term where
-    asConstant   :: term -> Maybe (Some (ValueOf (UniOf term)))
-    fromConstant :: Some (ValueOf (UniOf term)) -> term
+    asConstant :: term -> Maybe (Some (ValueOf (UniOf term)))
+    toConstant :: Some (ValueOf (UniOf term)) -> term
 
 instance ToAnnotation uni ann => HasConstant (Term tyname name uni ann) where
     asConstant (Constant _ con) = Just con
@@ -287,6 +281,10 @@ class KnownTypeAst uni a where
     default toTypeAst :: uni `Includes` a => proxy a -> Type TyName uni ()
     toTypeAst _ = mkTyBuiltin @a ()
 
+-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
+type KnownBuiltinType term a =
+    (HasConstant term, GShow (UniOf term), GEq (UniOf term), UniOf term `Includes` a)
+
 -- See Note [KnownType's defaults]
 -- | Haskell types known to exist on the PLC side.
 class KnownTypeAst (UniOf term) a => KnownType term a where
@@ -302,10 +300,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