From 4710dff2e30ce131191a6a1ccbe43595b2e3af24 Mon Sep 17 00:00:00 2001 From: effectfully Date: Sat, 8 Jan 2022 20:20:33 +0300 Subject: [PATCH] [Builtins] Drop a couple more 'Proxy's from 'TypeScheme' --- plutus-core/executables/Common.hs | 6 +++--- .../PlutusCore/Generators/Internal/Denotation.hs | 9 ++++----- .../PlutusCore/Generators/Internal/Entity.hs | 6 +++--- .../src/PlutusCore/Constant/Function.hs | 5 +++-- .../plutus-core/src/PlutusCore/Constant/Meaning.hs | 4 ++-- .../plutus-core/src/PlutusCore/Constant/Typed.hs | 8 ++++++-- .../src/PlutusCore/Evaluation/Machine/Ck.hs | 6 +++--- plutus-core/plutus-ir/src/PlutusIR/Purity.hs | 14 +++++++------- .../Evaluation/Machine/Cek/Internal.hs | 4 ++-- 9 files changed, 33 insertions(+), 29 deletions(-) diff --git a/plutus-core/executables/Common.hs b/plutus-core/executables/Common.hs index 90c66bb6a71..87b6ca1a5d6 100644 --- a/plutus-core/executables/Common.hs +++ b/plutus-core/executables/Common.hs @@ -616,9 +616,9 @@ typeSchemeToSignature = toSig [] where toSig :: [QVarOrType] -> PLC.TypeScheme PlcTerm args res -> Signature toSig acc = \case - PLC.TypeSchemeResult pR -> Signature acc (PLC.toTypeAst pR) - PLC.TypeSchemeArrow pA schB -> - toSig (acc ++ [Type $ PLC.toTypeAst pA]) schB + pR@PLC.TypeSchemeResult -> Signature acc (PLC.toTypeAst pR) + arr@(PLC.TypeSchemeArrow schB) -> + toSig (acc ++ [Type $ PLC.toTypeAst $ PLC.argOf arr]) schB PLC.TypeSchemeAll proxy schK -> case proxy of (_ :: Proxy '(text, uniq, kind)) -> diff --git a/plutus-core/generators/PlutusCore/Generators/Internal/Denotation.hs b/plutus-core/generators/PlutusCore/Generators/Internal/Denotation.hs index a24ecc02e2e..316f5ccad30 100644 --- a/plutus-core/generators/PlutusCore/Generators/Internal/Denotation.hs +++ b/plutus-core/generators/PlutusCore/Generators/Internal/Denotation.hs @@ -25,7 +25,6 @@ import PlutusCore.Name import Data.Dependent.Map (DMap) import Data.Dependent.Map qualified as DMap import Data.Functor.Compose -import Data.Proxy -- | Haskell denotation of a PLC object. An object can be a 'Builtin' or a variable for example. data Denotation term object res = forall args. Denotation @@ -62,15 +61,15 @@ newtype DenotationContext term = DenotationContext -- | The resulting type of a 'TypeScheme'. typeSchemeResult :: TypeScheme term args res -> AsKnownType term res -typeSchemeResult (TypeSchemeResult _) = AsKnownType -typeSchemeResult (TypeSchemeArrow _ schB) = typeSchemeResult schB -typeSchemeResult (TypeSchemeAll _ schK) = typeSchemeResult schK +typeSchemeResult TypeSchemeResult = AsKnownType +typeSchemeResult (TypeSchemeArrow schB) = typeSchemeResult schB +typeSchemeResult (TypeSchemeAll _ schK) = typeSchemeResult schK -- | Get the 'Denotation' of a variable. denoteVariable :: KnownType (Term TyName Name uni fun ()) res => Name -> res -> Denotation (Term TyName Name uni fun ()) Name res -denoteVariable name meta = Denotation name (Var ()) meta (TypeSchemeResult Proxy) +denoteVariable name meta = Denotation name (Var ()) meta TypeSchemeResult -- | Insert the 'Denotation' of an object into a 'DenotationContext'. insertDenotation diff --git a/plutus-core/generators/PlutusCore/Generators/Internal/Entity.hs b/plutus-core/generators/PlutusCore/Generators/Internal/Entity.hs index 763f4aa31c7..1bc3dea2a6b 100644 --- a/plutus-core/generators/PlutusCore/Generators/Internal/Entity.hs +++ b/plutus-core/generators/PlutusCore/Generators/Internal/Entity.hs @@ -153,17 +153,17 @@ genIterAppValue (Denotation object embed meta scheme) = result where -> ([Plain Term uni fun] -> [Plain Term uni fun]) -> FoldArgs args res -> PlcGenT uni fun m (IterAppValue uni fun head (Plain Term uni fun) res) - go (TypeSchemeResult _) term args y = do -- Computed the result. + go TypeSchemeResult term args y = do -- Computed the result. let pia = IterApp object $ args [] return $ IterAppValue term pia y - go (TypeSchemeArrow _ schB) term args f = do -- Another argument is required. + go (TypeSchemeArrow schB) term args f = do -- Another argument is required. BuiltinGensT genTb <- ask TermOf v x <- liftT $ genTb AsKnownType -- Get a Haskell and the correspoding PLC values. let term' = Apply () term v -- Apply the term to the PLC value. args' = args . (v :) -- Append the PLC value to the spine. y = f x -- Apply the Haskell function to the generated argument. go schB term' args' y - go (TypeSchemeAll _ schK) term args f = + go (TypeSchemeAll _ schK) term args f = go schK term args f -- | Generate a PLC 'Term' of the specified type and the corresponding Haskell value. diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Function.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Function.hs index f3df2f64272..2338c304e5d 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Function.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Function.hs @@ -18,8 +18,9 @@ import GHC.TypeLits -- | Convert a 'TypeScheme' to the corresponding 'Type'. -- Basically, a map from the PHOAS representation to the FOAS one. typeSchemeToType :: TypeScheme term args res -> Type TyName (UniOf term) () -typeSchemeToType (TypeSchemeResult pR) = toTypeAst pR -typeSchemeToType (TypeSchemeArrow pA schB) = TyFun () (toTypeAst pA) $ typeSchemeToType schB +typeSchemeToType sch@TypeSchemeResult = toTypeAst sch +typeSchemeToType sch@(TypeSchemeArrow schB) = + TyFun () (toTypeAst $ argOf sch) $ typeSchemeToType schB typeSchemeToType (TypeSchemeAll proxy schK) = case proxy of (_ :: Proxy '(text, uniq, kind)) -> let text = Text.pack $ symbolVal @text Proxy diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 191809603d2..1bfc2437307 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -184,12 +184,12 @@ class KnownMonotype term args res a | args res -> a, a -> res where -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'. instance (res ~ res', KnownType term res) => KnownMonotype term '[] res res' where - knownMonotype = TypeSchemeResult Proxy + knownMonotype = TypeSchemeResult -- | Every term-level argument becomes as 'TypeSchemeArrow'. instance (KnownType term arg, KnownMonotype term args res a) => KnownMonotype term (arg ': args) res (arg -> a) where - knownMonotype = Proxy `TypeSchemeArrow` knownMonotype + knownMonotype = TypeSchemeArrow knownMonotype -- | A class that allows us to derive a polytype for a builtin. class KnownPolytype (binds :: [Some TyNameRep]) term args res a | args res -> a, a -> res where diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 0f636f55a98..b6736e98078 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -25,6 +25,7 @@ module PlutusCore.Constant.Typed ( TypeScheme (..) + , argOf , FoldArgs , FoldArgsEx , TyNameRep (..) @@ -87,10 +88,10 @@ infixr 9 `TypeSchemeArrow` data TypeScheme term (args :: [GHC.Type]) res where TypeSchemeResult :: KnownType term res - => Proxy res -> TypeScheme term '[] res + => TypeScheme term '[] res TypeSchemeArrow :: KnownType term arg - => Proxy arg -> TypeScheme term args res -> TypeScheme term (arg ': args) res + => TypeScheme term args res -> TypeScheme term (arg ': args) res TypeSchemeAll :: (KnownSymbol text, KnownNat uniq, KnownKind kind) -- Here we require the user to manually provide the unique of a type variable. @@ -99,6 +100,9 @@ data TypeScheme term (args :: [GHC.Type]) res where -> TypeScheme term args res -> TypeScheme term args res +argOf :: TypeScheme term (arg ': args) res -> Proxy arg +argOf _ = Proxy + -- | Turn a list of Haskell types @args@ into a functional type ending in @res@. -- -- >>> :set -XDataKinds diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs index f80019fe52c..a3f4b4cb279 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs @@ -67,8 +67,8 @@ evalBuiltinApp -> BuiltinRuntime (CkValue uni fun) -> CkM uni fun s (CkValue uni fun) evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of - TypeSchemeResult _ -> makeKnown emitCkM (Just term) x - _ -> pure $ VBuiltin term runtime + TypeSchemeResult -> makeKnown emitCkM (Just term) x + _ -> pure $ VBuiltin term runtime ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun () ckValueToTerm = \case @@ -300,7 +300,7 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do case sch of -- It's only possible to apply a builtin application if the builtin expects a term -- argument next. - TypeSchemeArrow _ schB -> do + TypeSchemeArrow schB -> do x <- liftEither $ readKnown (Just argTerm) arg let noCosting = error "The CK machine does not support costing" runtime' = BuiltinRuntime schB (f x) noCosting diff --git a/plutus-core/plutus-ir/src/PlutusIR/Purity.hs b/plutus-core/plutus-ir/src/PlutusIR/Purity.hs index 2badcf04b01..21be327ab60 100644 --- a/plutus-core/plutus-ir/src/PlutusIR/Purity.hs +++ b/plutus-core/plutus-ir/src/PlutusIR/Purity.hs @@ -18,16 +18,16 @@ data BuiltinApp tyname name uni fun a = BuiltinApp fun [Arg tyname name uni fun saturatesScheme :: [Arg tyname name uni fun a] -> TypeScheme term args res -> Maybe Bool -- We've passed enough arguments that the builtin will reduce. Note that this also accepts over-applied builtins. -saturatesScheme _ TypeSchemeResult{} = Just True +saturatesScheme _ TypeSchemeResult{} = Just True -- Consume one argument -saturatesScheme (TermArg _ : args) (TypeSchemeArrow _ sch) = saturatesScheme args sch -saturatesScheme (TypeArg _ : args) (TypeSchemeAll _ sch) = saturatesScheme args sch +saturatesScheme (TermArg _ : args) (TypeSchemeArrow sch) = saturatesScheme args sch +saturatesScheme (TypeArg _ : args) (TypeSchemeAll _ sch) = saturatesScheme args sch -- Under-applied, not saturated -saturatesScheme [] TypeSchemeArrow{} = Just False -saturatesScheme [] TypeSchemeAll{} = Just False +saturatesScheme [] TypeSchemeArrow{} = Just False +saturatesScheme [] TypeSchemeAll{} = Just False -- These cases are only possible in case we have an ill-typed builtin application, so we can't give an answer. -saturatesScheme (TypeArg _ : _) TypeSchemeArrow{} = Nothing -saturatesScheme (TermArg _ : _) TypeSchemeAll{} = Nothing +saturatesScheme (TypeArg _ : _) TypeSchemeArrow{} = Nothing +saturatesScheme (TermArg _ : _) TypeSchemeAll{} = Nothing -- | Is the given 'BuiltinApp' saturated? Returns 'Nothing' if something is badly wrong and we can't tell. isSaturated diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs index cc930ce2df4..735648b706f 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs @@ -539,7 +539,7 @@ evalBuiltinApp -> BuiltinRuntime (CekValue uni fun) -> CekM uni fun s (CekValue uni fun) evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of - TypeSchemeResult _ -> do + TypeSchemeResult -> do spendBudgetCek (BBuiltinApp fun) cost makeKnown ?cekEmitter (Just term) x _ -> pure $ VBuiltin fun term env runtime @@ -681,7 +681,7 @@ enterComputeCek = computeCek (toWordArray 0) where case sch of -- It's only possible to apply a builtin application if the builtin expects a term -- argument next. - TypeSchemeArrow _ schB -> do + TypeSchemeArrow schB -> do x <- liftEither $ readKnown (Just argTerm) arg -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it. -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.