Skip to content

[Builtin] Add "dumb" Data matching #7209

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
+194 −44
Open

[Builtin] Add "dumb" Data matching #7209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b03059d
Add `Data` matching
SeungheonOh Jul 14, 2025
5aa6ceb
Make builtin use casing + goldens
SeungheonOh Jul 14, 2025
4037219
More golden
SeungheonOh Jul 14, 2025
f95da90
Merge branch 'master' into sho/6602-data
SeungheonOh Aug 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 27 additions & 2 deletions plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ import PlutusCore.Core.Type (Type (..))
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
import PlutusCore.Data (Data)
import PlutusCore.Data (Data (..))
import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
NumBytesCostedAsNumWords (..))
import PlutusCore.Pretty.Extra (juxtRenderContext)
Expand Down Expand Up @@ -544,7 +544,18 @@ instance AnnotateCaseBuiltin DefaultUni where
[cons] -> Right [(cons, [argTy, listTy])]
[cons, nil] -> Right [(cons, [argTy, listTy]), (nil, [])]
_ -> Left $ "Casing on list requires exactly one branch or two branches"
_ -> Left $ display (() <$ ty) <> " isn't supported in 'case'"
TyBuiltin ann (SomeTypeIn DefaultUniData) ->
case branches of
[constr, maep, list, i , b] ->
Right
[ (constr, [mkTyBuiltin @_ @Integer ann, mkTyBuiltin @_ @[Data] ann])
, (maep, [mkTyBuiltin @_ @[(Data, Data)] ann])
, (list, [mkTyBuiltin @_ @[Data] ann])
, (i, [mkTyBuiltin @_ @Integer ann])
, (b, [mkTyBuiltin @_ @ByteString ann])
]
_ -> Left $ "Casing on data requires exactly five branches"
_ -> Left $ display (() <$ ty) <> " isn't supported in 'case'"

instance CaseBuiltin DefaultUni where
caseBuiltin someVal@(Some (ValueOf uni x)) branches = case uni of
Expand All @@ -568,6 +579,20 @@ instance CaseBuiltin DefaultUni where
[] -> Right $ HeadOnly $ branches Vector.! 1
(y : ys) -> Right $ headSpine (branches Vector.! 0) [someValueOf ty y, someValueOf uni ys]
| otherwise -> Left $ outOfBoundsErr someVal branches
DefaultUniData
| len == 5 ->
case x of
Constr idx ds ->
Right $ headSpine (branches Vector.! 0) [someValue @Integer idx, someValue @[Data] ds]
Map ds ->
Right $ headSpine (branches Vector.! 1) [someValue @[(Data, Data)] ds]
List ds ->
Right $ headSpine (branches Vector.! 2) [someValue @[Data] ds]
I i ->
Right $ headSpine (branches Vector.! 3) [someValue @Integer i]
B b ->
Right $ headSpine (branches Vector.! 4) [someValue @ByteString b]
| otherwise -> Left $ outOfBoundsErr someVal branches
_ -> Left $ display uni <> " isn't supported in 'case'"
where
!len = Vector.length branches
Expand Down
38 changes: 19 additions & 19 deletions plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,29 +1,29 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Utils.Decidable where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Bool qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Irrelevant qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.Code.Relation.Nullary.Reflects qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
word64ToNat)
import MAlonzo.RTE qualified
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Utils.Decidable.dmap
d_dmap_12 ::
Expand Down
46 changes: 23 additions & 23 deletions plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,32 +1,32 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Utils.Reflection where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.List qualified
import MAlonzo.Code.Agda.Builtin.Maybe qualified
import MAlonzo.Code.Agda.Builtin.Reflection qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Builtin.String qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Char.Base qualified
import MAlonzo.Code.Data.List.Base qualified
import MAlonzo.Code.Data.String.Base qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
word64ToNat)
import MAlonzo.RTE qualified
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Reflection
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Char.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Utils.Reflection.constructors
d_constructors_4 ::
Expand Down Expand Up @@ -62,7 +62,7 @@ d_lastName_14 v0 v1
(case coe v2 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v3 -> coe v3
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> coe v0
_ -> MAlonzo.RTE.mazUnreachableError)
_ -> MAlonzo.RTE.mazUnreachableError)
-- Utils.Reflection.getLastName
d_getLastName_34 ::
AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6
Expand Down
125 changes: 125 additions & 0 deletions plutus-tx-plugin/src/PlutusTx/Compiler/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -451,6 +451,131 @@ defineBuiltinTerms = do
[PIR.var () f, PIR.var () z]


defineBuiltinTerm annMayInline 'Builtins.caseData' $ case datatypeStyle of
style | style == PIR.ScottEncoding || style == PIR.SumsOfProducts ->
-- > /\r ->
-- > \(fConstr : integer -> list data -> r)
-- > (fMap : list (pair data data) -> r)
-- > (fList : list data -> r)
-- > (fI : integer -> r)
-- > (fB : bytestring -> r)
-- > (d : data) ->
-- > chooseData
-- > {all dead. r}
-- > d
-- > (/\dead ->
-- > (/\a b c ->
-- > \(f : a -> b -> c) (p : pair a b) ->
-- > f (fstPair {a} {b} p) (sndPair {a} {b} p))
-- > {integer}
-- > {list data}
-- > {r}
-- > fConstr
-- > (unConstrData d))
-- > (/\dead -> fMap (unMapData d))
-- > (/\dead -> fList (unListData d))
-- > (/\dead -> fI (unIData d))
-- > (/\dead -> fB (unBData d))
-- > {r}
fmap (const annMayInline) . runQuote $ do
r <- freshTyName "r"
dead <- freshTyName "dead"
fConstr <- freshName "fConstr"
fMap <- freshName "fMap"
fList <- freshName "fList"
fI <- freshName "fI"
fB <- freshName "fB"
d <- freshName "d"
let integer = PLC.mkTyBuiltin @_ @Integer ()
listData = PLC.mkTyBuiltin @_ @[PLC.Data] ()
listPairData = PLC.mkTyBuiltin @_ @[(PLC.Data, PLC.Data)] ()
bytestring = PLC.mkTyBuiltin @_ @BS.ByteString ()
return
. PIR.tyAbs () r (PLC.Type ())
. PIR.lamAbs
()
fConstr
(PLC.TyFun () integer . PLC.TyFun () listData $ PLC.TyVar () r)
. PIR.lamAbs () fMap (PLC.TyFun () listPairData $ PLC.TyVar () r)
. PIR.lamAbs () fList (PLC.TyFun () listData $ PLC.TyVar () r)
. PIR.lamAbs () fI (PLC.TyFun () integer $ PLC.TyVar () r)
. PIR.lamAbs () fB (PLC.TyFun () bytestring $ PLC.TyVar () r)
. PIR.lamAbs () d (PLC.mkTyBuiltin @_ @PLC.Data ())
. PIR.tyInst
()
( PIR.mkIterAppNoAnn
( PIR.tyInst () (PIR.builtin () PLC.ChooseData)
. PLC.TyForall () dead (PLC.Type ())
$ PLC.TyVar () r
)
[ PIR.var () d
, PIR.tyAbs () dead (PLC.Type ()) $
PIR.mkIterAppNoAnn
( PIR.mkIterInstNoAnn
PLC.uncurry
[integer, listData, PLC.TyVar () r]
)
[ PIR.var () fConstr
, PIR.apply () (PIR.builtin () PLC.UnConstrData) $
PIR.var () d
]
, PIR.tyAbs () dead (PLC.Type ())
. PIR.apply () (PIR.var () fMap)
. PIR.apply () (PIR.builtin () PLC.UnMapData)
$ PIR.var () d
, PIR.tyAbs () dead (PLC.Type ())
. PIR.apply () (PIR.var () fList)
. PIR.apply () (PIR.builtin () PLC.UnListData)
$ PIR.var () d
, PIR.tyAbs () dead (PLC.Type ())
. PIR.apply () (PIR.var () fI)
. PIR.apply () (PIR.builtin () PLC.UnIData)
$ PIR.var () d
, PIR.tyAbs () dead (PLC.Type ())
. PIR.apply () (PIR.var () fB)
. PIR.apply () (PIR.builtin () PLC.UnBData)
$ PIR.var () d
]
)
$ PLC.TyVar () r
_BuiltinCasing ->
-- > /\r ->
-- > \(fConstr : integer -> list data -> r)
-- > (fMap : list (pair data data) -> r)
-- > (fList : list data -> r)
-- > (fI : integer -> r)
-- > (fB : bytestring -> r)
-- > (d : data) ->
-- > (case r d fConstr fMap fList fI fB)
fmap (const annMayInline) . runQuote $ do
r <- freshTyName "r"
fConstr <- freshName "fConstr"
fMap <- freshName "fMap"
fList <- freshName "fList"
fI <- freshName "fI"
fB <- freshName "fB"
d <- freshName "d"
let integer = PLC.mkTyBuiltin @_ @Integer ()
listData = PLC.mkTyBuiltin @_ @[PLC.Data] ()
listPairData = PLC.mkTyBuiltin @_ @[(PLC.Data, PLC.Data)] ()
bytestring = PLC.mkTyBuiltin @_ @BS.ByteString ()
return
$ PIR.tyAbs () r (PLC.Type ())
$ PIR.lamAbs
()
fConstr
(PLC.TyFun () integer . PLC.TyFun () listData $ PLC.TyVar () r)
$ PIR.lamAbs () fMap (PLC.TyFun () listPairData $ PLC.TyVar () r)
$ PIR.lamAbs () fList (PLC.TyFun () listData $ PLC.TyVar () r)
$ PIR.lamAbs () fI (PLC.TyFun () integer $ PLC.TyVar () r)
$ PIR.lamAbs () fB (PLC.TyFun () bytestring $ PLC.TyVar () r)
$ PIR.lamAbs () d (PLC.mkTyBuiltin @_ @PLC.Data ())
$ PIR.kase
()
(PLC.TyVar () r)
(PIR.var () d)
[PIR.var () fConstr, PIR.var () fMap, PIR.var () fList, PIR.var () fI, PIR.var () fB]

-- See Note [Builtin terms and values]
for_ enumerate $ \fun ->
let defineBuiltinInl impl = defineBuiltinTerm annMayInline impl $ mkBuiltin fun
Expand Down