[Builtins] add 'constrTermFromConstrData'

effectfully · effectfully · commit 4712cf3104f1 · 2024-02-18T02:14:16.000+01:00
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
@@ -203,6 +203,7 @@ library
     Data.Aeson.THReader
     Data.Functor.Foldable.Monadic
     PlutusCore.Builtin.HasConstant
+    PlutusCore.Builtin.HasConstr
     PlutusCore.Builtin.KnownKind
     PlutusCore.Builtin.KnownType
     PlutusCore.Builtin.KnownTypeAst
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin.hs
@@ -6,6 +6,7 @@ module PlutusCore.Builtin
 
 import PlutusCore.Builtin.Emitter as Export
 import PlutusCore.Builtin.HasConstant as Export
+import PlutusCore.Builtin.HasConstr as Export
 import PlutusCore.Builtin.KnownKind as Export
 import PlutusCore.Builtin.KnownType as Export
 import PlutusCore.Builtin.KnownTypeAst as Export
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/HasConstant.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/HasConstant.hs
@@ -14,7 +14,6 @@ module PlutusCore.Builtin.HasConstant
 
 import PlutusCore.Builtin.Result
 import PlutusCore.Core
-import PlutusCore.Name
 
 import Universe
 
@@ -54,7 +53,7 @@ fromValue :: (HasConstant term, UniOf term `HasTermLevel` a) => a -> term
 fromValue = fromValueOf knownUni
 {-# INLINE fromValue #-}
 
-instance HasConstant (Term TyName Name uni fun ()) where
+instance HasConstant (Term tyname name uni fun ()) where
     asConstant (Constant _ val) = pure val
     asConstant _                = throwNotAConstant
 
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/HasConstr.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/HasConstr.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE InstanceSigs           #-}
+{-# LANGUAGE LambdaCase             #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+module PlutusCore.Builtin.HasConstr
+    ( ToConstr (..)
+    ) where
+
+import PlutusCore.Builtin.KnownTypeAst
+import PlutusCore.Builtin.Polymorphism
+import PlutusCore.Core
+import PlutusCore.Name
+
+import Data.Proxy
+import Data.Word
+
+class ToConstr term where
+    toConstr
+        :: forall rep. KnownTypeAst TyName (UniOf term) rep
+        => Word64 -> [term] -> Opaque term rep
+
+instance ToConstr (Term TyName name uni fun ()) where
+    toConstr
+        :: forall rep. KnownTypeAst TyName uni rep
+        => Word64 -> [Term TyName name uni fun ()] -> Opaque (Term TyName name uni fun ()) rep
+    toConstr ix = Opaque . Constr () (toTypeAst $ Proxy @rep) ix
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
@@ -20,6 +20,7 @@ import PlutusPrelude
 
 import PlutusCore.Builtin.Elaborate
 import PlutusCore.Builtin.HasConstant
+import PlutusCore.Builtin.HasConstr
 import PlutusCore.Builtin.KnownKind
 import PlutusCore.Builtin.KnownType
 import PlutusCore.Builtin.KnownTypeAst
@@ -67,7 +68,7 @@ data BuiltinMeaning val cost =
         (cost -> BuiltinRuntime val)
 
 -- | Constraints available when defining a built-in function.
-type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val)
+type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val, ToConstr val)
 
 -- | A type class for \"each function from a set of built-in functions has a 'BuiltinMeaning'\".
 class
diff --git a/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs b/plutus-core/plutus-core/src/PlutusCore/Core/Type.hs
@@ -176,7 +176,8 @@ type HasTermLevel :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint
 type HasTermLevel uni = Includes uni
 
 -- | Extract the universe from a type.
-type family UniOf a :: GHC.Type -> GHC.Type
+type UniOf :: GHC.Type -> GHC.Type -> GHC.Type
+type family UniOf a
 
 type instance UniOf (Term tyname name uni fun ann) = uni
 
diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
@@ -20,10 +20,11 @@ import PlutusCore.Builtin
 import PlutusCore.Data (Data (..))
 import PlutusCore.Default.Universe
 import PlutusCore.Evaluation.Machine.BuiltinCostModel
-import PlutusCore.Evaluation.Machine.ExBudgetStream (ExBudgetStream)
+import PlutusCore.Evaluation.Machine.ExBudgetStream (ExBudgetStream (..))
 import PlutusCore.Evaluation.Machine.ExMemoryUsage (ExMemoryUsage, LiteralByteSize (..),
                                                     memoryUsage, singletonRose)
-import PlutusCore.Evaluation.Result (EvaluationResult (..))
+import PlutusCore.Evaluation.Result (EvaluationResult (..), evaluationFailure)
+import PlutusCore.Name (TyName)
 import PlutusCore.Pretty (PrettyConfigPlc)
 
 import PlutusCore.Bitwise.Convert as Convert
@@ -107,6 +108,7 @@ data DefaultFun
     -- types, hence we include the name of the data type as a suffix.
     | ChooseData
     | ConstrData
+    | ConstrTermFromConstrData
     | MapData
     | ListData
     | IData
@@ -1503,6 +1505,20 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
             constrDataDenotation
             (runCostingFunTwoArguments . paramConstrData)
 
+    toBuiltinMeaning _semvar ConstrTermFromConstrData =
+        let constrTermFromConstrDataDenotation
+                :: KnownTypeAst TyName DefaultUni sop => Data -> BuiltinResult (Opaque val sop)
+            constrTermFromConstrDataDenotation (Constr iInteger ds) = do
+                -- What? Lol, surely there should exist a better way to do it. Looks like we need
+                -- to separate a big chunk of 'ReadKnown' into 'ReadKnownConstant' or something.
+                iWord64 <- either (BuiltinFailure mempty) pure . readKnown $ fromValue @val iInteger
+                pure . toConstr iWord64 $ map fromValue ds
+            constrTermFromConstrDataDenotation _ = evaluationFailure
+            {-# INLINE constrTermFromConstrDataDenotation #-}
+        in makeBuiltinMeaning
+            constrTermFromConstrDataDenotation
+            (\_ _ -> ExBudgetLast mempty)
+
     toBuiltinMeaning _semvar MapData =
         let mapDataDenotation :: [(Data, Data)] -> Data
             mapDataDenotation = Map
@@ -1928,6 +1944,7 @@ instance Flat DefaultFun where
 
               IntegerToByteString             -> 73
               ByteStringToInteger             -> 74
+              ConstrTermFromConstrData        -> 75
 
     decode = go =<< decodeBuiltin
         where go 0  = pure AddInteger
@@ -2005,6 +2022,7 @@ instance Flat DefaultFun where
               go 72 = pure Blake2b_224
               go 73 = pure IntegerToByteString
               go 74 = pure ByteStringToInteger
+              go 75 = pure ConstrTermFromConstrData
               go t  = fail $ "Failed to decode builtin tag, got: " ++ show t
 
     size _ n = n + builtinTagWidth
diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
@@ -418,6 +418,22 @@ instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Word8 wher
                _       -> throwing_ _EvaluationFailure
     {-# INLINE readKnown #-}
 
+instance KnownTypeAst tyname DefaultUni Word64 where
+    toTypeAst _ = toTypeAst $ Proxy @Integer
+
+-- See Note [Integral types as Integer].
+instance HasConstantIn DefaultUni term => MakeKnownIn DefaultUni term Word64 where
+    makeKnown = makeKnown . toInteger
+    {-# INLINE makeKnown #-}
+
+instance HasConstantIn DefaultUni term => ReadKnownIn DefaultUni term Word64 where
+    readKnown term =
+        inline readKnownConstant term >>= oneShot \(i :: Integer) ->
+           case toIntegralSized i of
+               Just w64 -> pure w64
+               _        -> throwing_ _EvaluationFailure
+    {-# INLINE readKnown #-}
+
 -- deriving newtype doesn't work here (or at least not easily), so we have an explicit instance.
 instance KnownTypeAst tyname DefaultUni LiteralByteSize where
      toTypeAst _ = toTypeAst $ Proxy @Integer
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
@@ -4,10 +4,12 @@
 {-# LANGUAGE DeriveAnyClass            #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE InstanceSigs              #-}
 {-# LANGUAGE LambdaCase                #-}
 {-# LANGUAGE MultiParamTypeClasses     #-}
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE RankNTypes                #-}
+{-# LANGUAGE TypeApplications          #-}
 {-# LANGUAGE TypeFamilies              #-}
 {-# LANGUAGE TypeOperators             #-}
 {-# LANGUAGE UndecidableInstances      #-}
@@ -44,6 +46,7 @@ import Control.Monad.ST
 import Data.DList (DList)
 import Data.DList qualified as DList
 import Data.List.Extras (wix)
+import Data.Proxy
 import Data.STRef
 import Data.Text (Text)
 import Data.Word
@@ -135,6 +138,12 @@ instance HasConstant (CkValue uni fun) where
 
     fromConstant = VCon
 
+instance ToConstr (CkValue uni fun) where
+    toConstr
+        :: forall rep. KnownTypeAst TyName uni rep
+        => Word64 -> [CkValue uni fun] -> Opaque (CkValue uni fun) rep
+    toConstr ix = Opaque . VConstr (toTypeAst $ Proxy @rep) ix
+
 data Frame uni fun
     = FrameAwaitArg (CkValue uni fun)                       -- ^ @[V _]@
     | FrameAwaitFunTerm (Term TyName Name uni fun ())       -- ^ @[_ N]@
diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/DefaultFun/ConstrTermFromConstrData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/DefaultFun/ConstrTermFromConstrData.plc.golden
@@ -0,0 +1 @@
+all a. data -> a
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Core/Type.hs b/plutus-core/plutus-ir/src/PlutusIR/Core/Type.hs
@@ -1,9 +1,11 @@
 -- editorconfig-checker-disable-file
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE InstanceSigs          #-}
 {-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE UndecidableInstances  #-}
 
@@ -37,19 +39,19 @@ import PlutusPrelude
 import Control.Lens.TH
 import PlutusCore (Kind, Name, TyName, Type (..), Version (..))
 import PlutusCore qualified as PLC
-import PlutusCore.Builtin (HasConstant (..), throwNotAConstant)
+import PlutusCore.Builtin qualified as PLC
 import PlutusCore.Core (UniOf)
+import PlutusCore.Error (ApplyProgramError (MkApplyProgramError))
 import PlutusCore.Evaluation.Machine.ExMemoryUsage
 import PlutusCore.Flat ()
 import PlutusCore.MkPlc (Def (..), TermLike (..), TyVarDecl (..), VarDecl (..))
 import PlutusCore.Name qualified as PLC
 
-import Universe
-
 import Data.Hashable
+import Data.Proxy
 import Data.Text qualified as T
 import Data.Word
-import PlutusCore.Error (ApplyProgramError (MkApplyProgramError))
+import Universe
 
 -- Datatypes
 
@@ -157,12 +159,18 @@ instance ExMemoryUsage (Term tyname name uni fun ann) where
 
 type instance UniOf (Term tyname name uni fun ann) = uni
 
-instance HasConstant (Term tyname name uni fun ()) where
+instance PLC.HasConstant (Term tyname name uni fun ()) where
     asConstant (Constant _ val) = pure val
-    asConstant _                = throwNotAConstant
+    asConstant _                = PLC.throwNotAConstant
 
     fromConstant = Constant ()
 
+instance PLC.ToConstr (Term TyName name uni fun ()) where
+    toConstr
+        :: forall rep. PLC.KnownTypeAst TyName uni rep
+        => Word64 -> [Term TyName name uni fun ()] -> PLC.Opaque (Term TyName name uni fun ()) rep
+    toConstr ix = PLC.Opaque . Constr () (PLC.toTypeAst $ Proxy @rep) ix
+
 instance TermLike (Term tyname name uni fun) tyname name uni fun where
     var      = Var
     tyAbs    = TyAbs
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs
@@ -35,24 +35,39 @@ evaluateBuiltinsPass tcconfig conservative binfo costModel =
       [Typechecks tcconfig]
       [ConstCondition (Typechecks tcconfig)]
 
+-- >>> import PlutusCore.Builtin
+-- >>> import PlutusCore
+-- >>> fromValue (I 42) :: Term Name DefaultUni DefaultFun
+-- <interactive>:47:2: error: [GHC-39999]
+--     • Ambiguous type variable ‘a0’ arising from a use of ‘print’
+--       prevents the constraint ‘(Show a0)’ from being solved.
+--       Probable fix: use a type annotation to specify what ‘a0’ should be.
+--       Potentially matching instances:
+--         instance (Show a, Show b) => Show (Either a b)
+--           -- Defined in ‘Data.Either’
+--         instance Show Ordering -- Defined in ‘GHC.Show’
+--         ...plus 30 others
+--         ...plus 559 instances involving out-of-scope types
+--         (use -fprint-potential-instances to see them all)
+--     • In a stmt of an interactive GHCi command: print it
+
 evaluateBuiltins
-  :: forall tyname name uni fun a
+  :: forall name uni fun a
   . (ToBuiltinMeaning uni fun
-  , Typeable tyname
   , Typeable name)
   => Bool
   -- ^ Whether to be conservative and try to retain logging behaviour.
   -> BuiltinsInfo uni fun
   -> CostingPart uni fun
-  -> Term tyname name uni fun a
-  -> Term tyname name uni fun a
+  -> Term TyName name uni fun a
+  -> Term TyName name uni fun a
 evaluateBuiltins conservative binfo costModel = transformOf termSubterms processTerm
   where
     -- Nothing means "leave the original term as it was"
     eval
-      :: BuiltinRuntime (Term tyname name uni fun ())
-      -> AppContext tyname name uni fun a
-      -> Maybe (Term tyname name uni fun ())
+      :: BuiltinRuntime (Term TyName name uni fun ())
+      -> AppContext TyName name uni fun a
+      -> Maybe (Term TyName name uni fun ())
     eval (BuiltinCostedResult _ getX) AppContextEnd =
         case getX of
             BuiltinSuccess v           -> Just v
@@ -76,7 +91,7 @@ evaluateBuiltins conservative binfo costModel = transformOf termSubterms process
     -- arg mismatch, including under-application, just leave it alone
     eval _ _ = Nothing
 
-    processTerm :: Term tyname name uni fun a -> Term tyname name uni fun a
+    processTerm :: Term TyName name uni fun a -> Term TyName name uni fun a
     -- See Note [Context splitting in a recursive pass]
     processTerm t@(splitApplication -> (Builtin x bn, argCtx)) =
       let runtime = toBuiltinRuntime costModel (toBuiltinMeaning (binfo ^. biSemanticsVariant) bn)
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
@@ -556,6 +556,12 @@ instance HasConstant (CekValue uni fun ann) where
     fromConstant = VCon
     {-# INLINE fromConstant #-}
 
+instance ToConstr (CekValue uni fun ann) where
+    -- It's critical for this to be defined in terms of 'foldl', so that fusion kicks in and
+    -- the list of arguments gets converted to an 'ArgStack' statically.
+    toConstr ix = Opaque . VConstr ix . foldl (flip ConsStack) EmptyStack
+    {-# INLINE toConstr #-}
+
 {-|
 The context in which the machine operates.
 
