Skip to content

Commit b4892d0

Browse files
SeungheonOhSeungheonOh
committed
wip
1 parent 7e4257b commit b4892d0

File tree

12 files changed

+144
-25
lines changed

12 files changed

+144
-25
lines changed

‎plutus-core/plutus-core.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,6 +240,7 @@ library
240240
PlutusCore.Builtin.KnownKind
241241
PlutusCore.Builtin.KnownType
242242
PlutusCore.Builtin.KnownTypeAst
243+
PlutusCore.Builtin.Let
243244
PlutusCore.Builtin.Meaning
244245
PlutusCore.Builtin.Polymorphism
245246
PlutusCore.Builtin.Result

‎plutus-core/plutus-core/src/PlutusCore/Builtin.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import PlutusCore.Builtin.HasConstant as Export
99
import PlutusCore.Builtin.KnownKind as Export
1010
import PlutusCore.Builtin.KnownType as Export
1111
import PlutusCore.Builtin.KnownTypeAst as Export
12+
import PlutusCore.Builtin.Let as Export
1213
import PlutusCore.Builtin.Meaning as Export
1314
import PlutusCore.Builtin.Polymorphism as Export
1415
import PlutusCore.Builtin.Result as Export

‎plutus-core/plutus-core/src/PlutusCore/Builtin/Let.hs‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE OverloadedStrings #-}
3+
{-# LANGUAGE RankNTypes #-}
4+
{-# LANGUAGE TypeOperators #-}
5+
6+
module PlutusCore.Builtin.Let where
7+
8+
import PlutusCore.Builtin.KnownType (Spine)
9+
import PlutusCore.Core.Type (Type, UniOf)
10+
import PlutusCore.Name.Unique (TyName)
11+
12+
import Control.DeepSeq (NFData (..), rwhnf)
13+
import Data.Default.Class (Default (..))
14+
import Data.Text (Text)
15+
import Data.Vector (Vector)
16+
import NoThunks.Class
17+
import Text.PrettyBy (display)
18+
import Universe
19+
20+
21+
class LetBuiltin uni where
22+
-- | Given a constant with its type tag and a vector of branches, choose the appropriate branch
23+
-- or fail if the constant doesn't correspond to any of the branches (or casing on constants of
24+
-- this type isn't supported at all).
25+
letBuiltin
26+
:: Some (ValueOf uni)
27+
-> Either Text [Some (ValueOf uni)]
28+
29+
data LeterBuiltin uni = LeterBuiltin
30+
{ unLeterBuiltin :: !(Some (ValueOf uni) -> Either Text [Some (ValueOf uni)])
31+
}
32+
33+
instance NFData (LeterBuiltin uni) where
34+
rnf = rwhnf
35+
36+
deriving via OnlyCheckWhnfNamed "PlutusCore.Builtin.Case.LeterBuiltin" (LeterBuiltin uni)
37+
instance NoThunks (LeterBuiltin uni)
38+
39+
instance LetBuiltin uni => Default (LeterBuiltin uni) where
40+
def = LeterBuiltin letBuiltin
41+
42+
unavailableLeterBuiltin :: Int -> LeterBuiltin uni
43+
unavailableLeterBuiltin ver =
44+
LeterBuiltin $ \_ -> Left $
45+
"'let' TODO " <> display ver

‎plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs‎

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ import PlutusCore.Core.Type (Type (..))
5050
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
5151
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
5252
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
53-
import PlutusCore.Data (Data)
53+
import PlutusCore.Data (Data (Constr))
5454
import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
5555
NumBytesCostedAsNumWords (..))
5656
import PlutusCore.Pretty.Extra (juxtRenderContext)
@@ -651,11 +651,28 @@ instance CaseBuiltin DefaultUni where
651651
case x of
652652
(l, r) -> Right $ headSpine (branches Vector.! 0) [someValueOf tyL l, someValueOf tyR r]
653653
| otherwise -> Left $ outOfBoundsErr someVal branches
654+
DefaultUniData ->
655+
case x of
656+
Constr ix ds
657+
| 0 <= ix && ix < toInteger len ->
658+
Right $
659+
headSpine
660+
(branches Vector.! (fromIntegral ix))
661+
(someValueOf DefaultUniData <$> ds)
662+
| otherwise -> Left $ outOfBoundsErr someVal branches
663+
_ -> Left "Only 'Constr' constructor can be cased"
654664
_ -> Left $ display uni <> " isn't supported in 'case'"
655665
where
656666
!len = Vector.length branches
657667
{-# INLINE caseBuiltin #-}
658668

669+
instance LetBuiltin DefaultUni where
670+
letBuiltin _someVal@(Some (ValueOf uni x)) =
671+
case uni of
672+
DefaultUniList ty -> Right $ someValueOf ty <$> x
673+
DefaultUniPair tyL tyR -> Right [someValueOf tyL $ fst x, someValueOf tyR $ snd x]
674+
_ -> Left $ display uni <> "no"
675+
659676
{- Note [Stable encoding of tags]
660677
'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
661678
universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'

‎plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -149,19 +149,19 @@ faster than the used in production. Also see Note [noinline for saving on
149149
ticks]. -}
150150
defaultCekParametersA :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
151151
defaultCekParametersA =
152-
MachineParameters def $
152+
MachineParameters def def $
153153
noinline mkMachineVariantParameters DefaultFunSemanticsVariantA cekCostModelVariantA
154154

155155
-- See Note [No inlining for MachineParameters]
156156
defaultCekParametersB :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
157157
defaultCekParametersB =
158-
MachineParameters def $
158+
MachineParameters def def $
159159
noinline mkMachineVariantParameters DefaultFunSemanticsVariantB cekCostModelVariantB
160160

161161
-- See Note [No inlining for MachineParameters]
162162
defaultCekParametersC :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
163163
defaultCekParametersC =
164-
MachineParameters def $
164+
MachineParameters def def $
165165
noinline mkMachineVariantParameters DefaultFunSemanticsVariantC cekCostModelVariantC
166166

167167
{- Note [noinline for saving on ticks]
@@ -360,6 +360,6 @@ unitCostBuiltinCostModel = BuiltinCostModelBase
360360
unitCekParameters :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
361361
unitCekParameters =
362362
-- See Note [noinline for saving on ticks].
363-
MachineParameters def $
363+
MachineParameters def def $
364364
noinline mkMachineVariantParameters def $
365365
CostModel unitCekMachineCosts unitCostBuiltinCostModel

‎plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ The @val@ type will be 'CekValue' when we're using this with the CEK machine.
5555
data MachineParameters machineCosts fun val =
5656
MachineParameters {
5757
machineCaserBuiltin :: CaserBuiltin (UniOf val)
58+
, machineLeterBuiltin :: LeterBuiltin (UniOf val)
5859
, machineVariantParameters :: MachineVariantParameters machineCosts fun val
5960
}
6061
deriving stock Generic
@@ -67,8 +68,8 @@ instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineVari
6768
allNoThunks [ noThunks ctx costs, noThunks ctx runtime ]
6869

6970
instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineParameters machinecosts fun val) where
70-
wNoThunks ctx (MachineParameters caser varPars) =
71-
allNoThunks [ noThunks ctx caser, noThunks ctx varPars ]
71+
wNoThunks ctx (MachineParameters caser leter varPars) =
72+
allNoThunks [ noThunks ctx caser, noThunks ctx leter, noThunks ctx varPars ]
7273

7374
{- Note [The CostingPart constraint in mkMachineVariantParameters]
7475
Discharging the @CostingPart uni fun ~ builtincosts@ constraint in 'mkMachineParameters' causes GHC

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Eq.hs‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,18 @@ eqTermM (Case ann1 a1 cs1) (Case ann2 a2 cs2) = do
108108
case zipExact (toList cs1) (toList cs2) of
109109
Just ps -> for_ ps $ \(t1, t2) -> eqTermM t1 t2
110110
Nothing -> empty
111+
eqTermM (Let ann1 names1 body1) (Let ann2 names2 body2) = do
112+
eqM ann1 ann2
113+
case zipExact names1 names2 of
114+
Just ps -> for_ ps $ \(t1, t2) -> eqNameM t1 t2
115+
Nothing -> empty
116+
eqTermM body1 body2
117+
eqTermM (Bind ann1 body1 binds1) (Bind ann2 body2 binds2) = do
118+
eqM ann1 ann2
119+
eqTermM body1 body2
120+
case zipExact binds1 binds2 of
121+
Just ps -> for_ ps $ \(t1, t2) -> eqTermM t1 t2
122+
Nothing -> empty
111123
eqTermM Constant{} _ = empty
112124
eqTermM Builtin{} _ = empty
113125
eqTermM Var{} _ = empty
@@ -118,3 +130,5 @@ eqTermM Force{} _ = empty
118130
eqTermM Error{} _ = empty
119131
eqTermM Constr{} _ = empty
120132
eqTermM Case{} _ = empty
133+
eqTermM Let{} _ = empty
134+
eqTermM Bind{} _ = empty

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs‎

Lines changed: 38 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -459,6 +459,7 @@ they don't actually take the context as an argument even at the source level.
459459
-- | Implicit parameter for the builtin runtime.
460460
type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun ann))
461461
type GivenCekCaserBuiltin uni = (?cekCaserBuiltin :: CaserBuiltin uni)
462+
type GivenCekLeterBuiltin uni = (?cekLeterBuiltin :: LeterBuiltin uni)
462463
-- | Implicit parameter for the log emitter reference.
463464
type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
464465
-- | Implicit parameter for budget spender.
@@ -471,6 +472,7 @@ type GivenCekCosts = (?cekCosts :: CekMachineCosts)
471472
type GivenCekReqs uni fun ann s =
472473
( GivenCekRuntime uni fun ann
473474
, GivenCekCaserBuiltin uni
475+
, GivenCekLeterBuiltin uni
474476
, GivenCekEmitter uni fun s
475477
, GivenCekSpender uni fun s
476478
, GivenCekSlippage
@@ -713,8 +715,8 @@ data Context uni fun ann
713715
-- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
714716
| FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
715717
-- ^ @(case _ C0 .. Cn)@
716-
| FrameAwaitLetBinds !(CekValEnv uni fun ann) !(NTerm uni fun ann) ![NTerm uni fun ann] ![CekValue uni fun ann] !(Context uni fun ann)
717-
| FrameAwaitLet ![CekValue uni fun ann] !(Context uni fun ann)
718+
| FrameAwaitLetBinds !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 !(NTerm uni fun ann) ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
719+
| FrameAwaitLet {-# UNPACK #-} !Word64 !(ArgStack uni fun ann) !(Context uni fun ann)
718720
| NoFrame
719721

720722
deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -754,7 +756,7 @@ runCekM
754756
-> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun))
755757
-> CekReport cost NamedDeBruijn uni fun
756758
runCekM
757-
(MachineParameters caser (MachineVariantParameters costs runtime))
759+
(MachineParameters caser leter (MachineVariantParameters costs runtime))
758760
(ExBudgetMode getExBudgetInfo)
759761
(EmitterMode getEmitterMode)
760762
a = runST $ do
@@ -763,6 +765,7 @@ runCekM
763765
ctr <- newCounter (Proxy @CounterSize)
764766
let ?cekRuntime = runtime
765767
?cekCaserBuiltin = caser
768+
?cekLeterBuiltin = leter
766769
?cekEmitter = _cekEmitterInfoEmit
767770
?cekBudgetSpender = _exBudgetModeSpender
768771
?cekCosts = costs
@@ -851,7 +854,7 @@ enterComputeCek = computeCek
851854
--stepAndMaybeSpend BApply
852855
-- computeCek (FrameAwaitLetBinds env t bs ctx) env t
853856
case bs of
854-
(t : rest) -> computeCek (FrameAwaitLetBinds env body rest [] ctx) env t
857+
(t : rest) -> computeCek (FrameAwaitLetBinds env 0 body rest NilStack ctx) env t
855858
[] -> computeCek ctx env body
856859

857860
{- | The returning phase of the CEK machine.
@@ -892,11 +895,16 @@ enterComputeCek = computeCek
892895
SpineLast arg -> applyEvaluate ctx fun (VCon arg)
893896
SpineCons arg rest -> applyEvaluate (FrameAwaitFunConN rest ctx) fun (VCon arg)
894897
-- s , [_ V1 .. Vn] ◅ lam x (M,ρ) ↦ s , [_ V2 .. Vn]; ρ [ x ↦ V1 ] ▻ M
895-
returnCek (FrameAwaitLet args ctx) l =
896-
case l of
897-
VLet names body env
898-
| length names == length args -> computeCek ctx (foldr Env.cons env args) body
899-
_ -> error "no"
898+
returnCek (FrameAwaitLet cnt args ctx) l =
899+
let
900+
-- this can probably be done in FrameAwaitLetBinds for better performance.
901+
go acc NilStack = acc
902+
go acc (ConsStack x xs) = Env.cons x (go acc xs)
903+
in case l of
904+
VLet names body env
905+
| length names == fromIntegral cnt -> computeCek ctx (go env args) body
906+
| otherwise -> error $ show (length names) <> " " <> show cnt
907+
_ -> error "no"
900908

901909
returnCek (FrameAwaitFunValueN args ctx) fun =
902910
case args of
@@ -930,16 +938,20 @@ enterComputeCek = computeCek
930938
VCon val -> case unCaserBuiltin ?cekCaserBuiltin val cs of
931939
Left err -> throwErrorDischarged (OperationalError $ CekCaseBuiltinError err) e
932940
Right (HeadOnly fX) -> computeCek ctx env fX
933-
Right (HeadSpine f xs) -> computeCek (FrameAwaitFunConN xs ctx) env f
941+
Right (HeadSpine f xs) ->
942+
let
943+
-- we reverse and reverse again, this is bad, just POC
944+
go acc (SpineLast x) = (ConsStack (VCon x) acc, 1)
945+
go acc (SpineCons x rest) = (+1) <$> go (ConsStack (VCon x) acc) rest
946+
947+
(xs', cnt) = go NilStack xs
948+
in computeCek (FrameAwaitLet cnt xs' ctx) env f
934949
_ -> throwErrorDischarged (StructuralError NonConstrScrutinizedMachineError) e
935-
-- returnCek (FrameAwaitLetTerm env bs ctx) e =
936-
-- case bs of
937-
-- (next : todo) -> computeCek (FrameAwaitLetBinds env e todo [] ctx) env next
938-
-- [] -> returnCek ctx e -- no bindings
939-
returnCek (FrameAwaitLetBinds env l todo done ctx) e =
950+
returnCek (FrameAwaitLetBinds env cnt l todo done ctx) e =
940951
case todo of
941-
(next : todo') -> computeCek (FrameAwaitLetBinds env l todo' (e : done) ctx) env next
942-
[] -> computeCek (FrameAwaitLet (e : done) ctx) env l
952+
(next : todo') ->
953+
computeCek (FrameAwaitLetBinds env (cnt + 1) l todo' (ConsStack e done) ctx) env next
954+
[] -> computeCek (FrameAwaitLet (cnt + 1) (ConsStack e done) ctx) env l
943955

944956
-- | @force@ a term and proceed.
945957
-- If v is a delay then compute the body of v;
@@ -996,6 +1008,15 @@ enterComputeCek = computeCek
9961008
evalBuiltinApp ctx fun term' $ f arg
9971009
_ ->
9981010
throwErrorWithCause (StructuralError UnexpectedBuiltinTermArgumentMachineError) term'
1011+
applyEvaluate !ctx (VLet names body env) (VCon v) =
1012+
case unLeterBuiltin ?cekLeterBuiltin v of
1013+
Right binds
1014+
| length binds == length names ->
1015+
computeCek ctx (foldl (flip (Env.cons . VCon)) env binds) body
1016+
| otherwise -> error "aa"
1017+
Left e -> error $ show e
1018+
1019+
-- computeCek (FrameAwaitLet cnt xs' ctx) env body
9991020
applyEvaluate !_ val _ =
10001021
throwErrorDischarged (StructuralError NonFunctionalApplicationMachineError) val
10011022

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -347,7 +347,7 @@ mkCekTrans
347347
-> Slippage
348348
-> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
349349
mkCekTrans
350-
(MachineParameters caser (MachineVariantParameters costs runtime))
350+
(MachineParameters caser leter (MachineVariantParameters costs runtime))
351351
(ExBudgetMode getExBudgetInfo)
352352
(EmitterMode getEmitterMode)
353353
slippage = do
@@ -356,6 +356,7 @@ mkCekTrans
356356
ctr <- newCounter (Proxy @CounterSize)
357357
let ?cekRuntime = runtime
358358
?cekCaserBuiltin = caser
359+
?cekLeterBuiltin = leter
359360
?cekEmitter = _cekEmitterInfoEmit
360361
?cekBudgetSpender = _exBudgetModeSpender
361362
?cekCosts = costs

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Purity.hs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -214,6 +214,16 @@ termEvaluationOrder builtinSemanticsVariant = goTerm
214214
<> evalThis (EvalTerm Pure MaybeWork t)
215215
-- then we go to an unknown scrutinee
216216
<> evalThis Unknown
217+
t@(Bind _ body binds) ->
218+
-- first binds
219+
foldMap goTerm binds
220+
-- then the body
221+
<> goTerm body
222+
-- then do the whole term
223+
<> evalThis (EvalTerm Pure MaybeWork t)
224+
<> case body of -- TODO: make sure this is correct
225+
Let _ _ body' -> goTerm body'
226+
_ -> evalThis Unknown
217227
-- Leaf terms
218228
t@Var{} ->
219229
evalThis (EvalTerm Pure WorkFree t)
@@ -228,6 +238,8 @@ termEvaluationOrder builtinSemanticsVariant = goTerm
228238
evalThis (EvalTerm Pure WorkFree t)
229239
t@LamAbs{} ->
230240
evalThis (EvalTerm Pure WorkFree t)
241+
t@Let{} ->
242+
evalThis (EvalTerm Pure WorkFree t)
231243
t@Constant{} ->
232244
evalThis (EvalTerm Pure WorkFree t)
233245

0 commit comments

Comments
 (0)