Skip to content
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

Jump to bottom

Add Delay type and use it #5910

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add Delay type and use it #5910

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
07a889e
Add Delay type and use it
michaelpj Apr 17, 2024
d1637d6
Add comments
michaelpj Apr 18, 2024
7a0fa2c
Use tilded 'data' instead of 'newtype'
effectfully Jun 19, 2024
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
203 changes: 115 additions & 88 deletions plutus-tx-plugin/test/IsData/9.6/deconstructData.pir.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ let
Nothing : Maybe a
!head : all a. list a -> a = headList
!ifThenElse : all a. bool -> a -> a -> a = ifThenElse
data Unit | Unit_match where
Unit : Unit
data (Delay :: * -> *) a | Delay_match where
Delay : (all b. a) -> Delay a
!chooseData : all a. data -> a -> a -> a -> a -> a -> a = chooseData
!fst : all a b. pair a b -> a = fstPair
!snd : all a b. pair a b -> b = sndPair
Expand Down Expand Up @@ -55,22 +55,27 @@ let
let
!bCase : bytestring -> r = bCase
in
chooseData
{Unit -> r}
d
(\(ds : Unit) ->
let
!tup : pair integer (list data)
= unsafeDataAsConstr d
in
constrCase
(fst {integer} {list data} tup)
(snd {integer} {list data} tup))
(\(ds : Unit) -> mapCase (unsafeDataAsMap d))
(\(ds : Unit) -> listCase (unsafeDataAsList d))
(\(ds : Unit) -> iCase (unsafeDataAsI d))
(\(ds : Unit) -> bCase (unsafeDataAsB d))
Unit
Delay_match
{r}
(chooseData
{Delay r}
d
(Delay
{r}
(/\b ->
let
!tup : pair integer (list data)
= unsafeDataAsConstr d
in
constrCase
(fst {integer} {list data} tup)
(snd {integer} {list data} tup)))
(Delay {r} (/\b -> mapCase (unsafeDataAsMap d)))
(Delay {r} (/\b -> listCase (unsafeDataAsList d)))
(Delay {r} (/\b -> iCase (unsafeDataAsI d)))
(Delay {r} (/\b -> bCase (unsafeDataAsB d))))
{r}
(\(a : all b. r) -> a {unit})
!tail : all a. list a -> list a = tailList
~`$fFromDataTuple2_$cfromBuiltinData` :
all a b.
Expand Down Expand Up @@ -101,80 +106,102 @@ let
(ifThenElse {Bool} b True False)
{all dead. Maybe (Tuple2 a b)}
(/\dead ->
Maybe_match
{Tuple2 data (list data)}
Delay_match
{Maybe (Tuple2 data (list data))}
(chooseList
{data}
{Unit -> Maybe (Tuple2 data (list data))}
{Delay (Maybe (Tuple2 data (list data)))}
args
(\(ds : Unit) -> Nothing {Tuple2 data (list data)})
(\(ds : Unit) ->
let
!h : data = head {data} args
!t : list data = tail {data} args
in
Just
{Tuple2 data (list data)}
(Tuple2 {data} {list data} h t))
Unit)
{all dead. Maybe (Tuple2 a b)}
(\(ds : Tuple2 data (list data)) ->
/\dead ->
Tuple2_match
{data}
{list data}
ds
{Maybe (Tuple2 a b)}
(\(ds : data) (ds : list data) ->
let
!l : list data = ds
in
Maybe_match
{a}
(`$dFromData` ds)
{all dead. Maybe (Tuple2 a b)}
(\(arg : a) ->
/\dead ->
Maybe_match
{data}
(chooseList
{data}
{Unit -> Maybe data}
l
(\(ds : Unit) -> Nothing {data})
(\(ds : Unit) ->
let
!h : data = head {data} l
!ds : list data
= tail {data} l
in
Just {data} h)
Unit)
{all dead. Maybe (Tuple2 a b)}
(\(ds : data) ->
/\dead ->
Maybe_match
{b}
(`$dFromData` ds)
{all dead. Maybe (Tuple2 a b)}
(\(arg : b) ->
/\dead ->
Just
{Tuple2 a b}
(Tuple2
{a}
(Delay
{Maybe (Tuple2 data (list data))}
(/\b -> Nothing {Tuple2 data (list data)}))
(Delay
{Maybe (Tuple2 data (list data))}
(/\b ->
let
!h : data = head {data} args
!t : list data = tail {data} args
in
Just
{Tuple2 data (list data)}
(Tuple2 {data} {list data} h t))))
{Maybe (Tuple2 a b)}
(\(a : all b. Maybe (Tuple2 data (list data))) ->
Maybe_match
{Tuple2 data (list data)}
(a {unit})
{all dead. Maybe (Tuple2 a b)}
(\(ds : Tuple2 data (list data)) ->
/\dead ->
Tuple2_match
{data}
{list data}
ds
{Maybe (Tuple2 a b)}
(\(ds : data) (ds : list data) ->
let
!l : list data = ds
in
Maybe_match
{a}
(`$dFromData` ds)
{all dead. Maybe (Tuple2 a b)}
(\(arg : a) ->
/\dead ->
Delay_match
{Maybe data}
(chooseList
{data}
{Delay (Maybe data)}
l
(Delay
{Maybe data}
(/\b -> Nothing {data}))
(Delay
{Maybe data}
(/\b ->
let
!h : data
= head {data} l
!ds : list data
= tail {data} l
in
Just {data} h)))
{Maybe (Tuple2 a b)}
(\(a : all b. Maybe data) ->
Maybe_match
{data}
(a {unit})
{all dead.
Maybe (Tuple2 a b)}
(\(ds : data) ->
/\dead ->
Maybe_match
{b}
arg
arg))
(/\dead ->
Nothing {Tuple2 a b})
{all dead. dead})
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead})
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead}))
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead})
(`$dFromData` ds)
{all dead.
Maybe
(Tuple2 a b)}
(\(arg : b) ->
/\dead ->
Just
{Tuple2 a b}
(Tuple2
{a}
{b}
arg
arg))
(/\dead ->
Nothing
{Tuple2 a b})
{all dead. dead})
(/\dead ->
Nothing {Tuple2 a b})
{all dead. dead}))
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead}))
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead}))
(/\dead -> Nothing {Tuple2 a b})
{all dead. dead})
(\(ds : list (pair data data)) -> Nothing {Tuple2 a b})
Expand Down
2 changes: 1 addition & 1 deletion plutus-tx-plugin/test/size/fromBuiltinData.size.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
346
343
31 changes: 17 additions & 14 deletions plutus-tx/src/PlutusTx/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,14 +109,15 @@ module PlutusTx.Builtins (
) where

import Data.Maybe
import PlutusTx.Base (const, uncurry)
import PlutusTx.Base (uncurry)
import PlutusTx.Bool (Bool (..))
import PlutusTx.Builtins.Class
import PlutusTx.Builtins.Internal (BuiltinBLS12_381_G1_Element (..),
BuiltinBLS12_381_G2_Element (..), BuiltinBLS12_381_MlResult (..),
BuiltinByteString (..), BuiltinData, BuiltinString)
import PlutusTx.Builtins.Internal qualified as BI
import PlutusTx.Integer (Integer)
import PlutusTx.Utils

import GHC.ByteOrder (ByteOrder (BigEndian, LittleEndian))

Expand Down Expand Up @@ -385,7 +386,7 @@ encodeUtf8 = BI.encodeUtf8

{-# INLINABLE matchList #-}
matchList :: forall a r . BI.BuiltinList a -> r -> (a -> BI.BuiltinList a -> r) -> r
matchList l nilCase consCase = BI.chooseList l (const nilCase) (\_ -> consCase (BI.head l) (BI.tail l)) ()
matchList l nilCase consCase = force (BI.chooseList l (Delay nilCase) (Delay (consCase (BI.head l) (BI.tail l))))

{-# INLINE headMaybe #-}
headMaybe :: BI.BuiltinList a -> Maybe a
Expand Down Expand Up @@ -484,14 +485,15 @@ matchData
-> (BuiltinByteString -> r)
-> r
matchData d constrCase mapCase listCase iCase bCase =
force (
chooseData
d
(\_ -> uncurry constrCase (unsafeDataAsConstr d))
(\_ -> mapCase (unsafeDataAsMap d))
(\_ -> listCase (unsafeDataAsList d))
(\_ -> iCase (unsafeDataAsI d))
(\_ -> bCase (unsafeDataAsB d))
()
(Delay (uncurry constrCase (unsafeDataAsConstr d)))
(Delay (mapCase (unsafeDataAsMap d)))
(Delay (listCase (unsafeDataAsList d)))
(Delay (iCase (unsafeDataAsI d)))
(Delay (bCase (unsafeDataAsB d)))
)

{-# INLINABLE matchData' #-}
-- | Given a 'BuiltinData' value and matching functions for the five constructors,
Expand All @@ -505,14 +507,15 @@ matchData'
-> (BuiltinByteString -> r)
-> r
matchData' d constrCase mapCase listCase iCase bCase =
force (
chooseData
d
(\_ -> let tup = BI.unsafeDataAsConstr d in constrCase (BI.fst tup) (BI.snd tup))
(\_ -> mapCase (BI.unsafeDataAsMap d))
(\_ -> listCase (BI.unsafeDataAsList d))
(\_ -> iCase (unsafeDataAsI d))
(\_ -> bCase (unsafeDataAsB d))
()
(Delay (let tup = BI.unsafeDataAsConstr d in constrCase (BI.fst tup) (BI.snd tup)))
(Delay (mapCase (BI.unsafeDataAsMap d)))
(Delay (listCase (BI.unsafeDataAsList d)))
(Delay (iCase (unsafeDataAsI d)))
(Delay (bCase (unsafeDataAsB d)))
)

-- G1 --
{-# INLINABLE bls12_381_G1_equals #-}
Expand Down
30 changes: 30 additions & 0 deletions plutus-tx/src/PlutusTx/Utils.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,40 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unused-foralls #-}
module PlutusTx.Utils where

-- We do not use qualified import because the whole module contains off-chain code
import PlutusTx.Builtins.Internal qualified as BI
import Prelude as Haskell

mustBeReplaced :: String -> a
mustBeReplaced placeholder =
error $
"The " <> show placeholder <> " placeholder must have been replaced by the \
\core-to-plc plugin during compilation."

-- | Delay evalaution of the expression inside the 'Delay' constructor.
data Delay a = Delay ~(forall b. a)

-- | Force the evaluation of the expression delayed by the 'Delay'.
force :: Delay a -> a
-- We can use any type here, but the type instantiation will keep the
-- type alive, so best to use a builtin type to avoid keeping other stuff
-- needlessly live.
force (Delay a) = a @BI.BuiltinUnit
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess the BuiltinUnit is necessary in order for it to be compiled into delay and force?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mysteriously it compiles without it, but I think it's better to be explicit about doing the type instantiation.


{- Note [The Delay type]
Occasionally we need to explicitly delay evaluation of an expression, since PLC
is strict. Ideally, this would eventually translate into the underlying 'delay'
and 'force' constructors of UPLC, as this is the fastest way to do it.

Our typed intermediate languages do not have 'delay' and 'force', however.
What they do have is type abstractions and type instantiations, which get
compiled into 'delay' and 'force', respectively. So what we want is something
which will create a (needless) type abstraction/type instantiation.

This is what 'Delay' does: the constructor accepts a 'forall' type, so the
expression inside the constructor application should be a type abstraction;
and 'force' just instantiates this to an arbitrary type, in this case
'BuiltinUnit'.
-}