[Experiment] Let/Bind

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Definitions.hs

@@ -16,6 +16,7 @@ import PlutusCore.Name.Unique (HasUnique, TermUnique (TermUnique), Unique (Uniqu
 import Control.Lens (forMOf_)
 import Control.Monad.State (MonadState, execStateT)
 import Control.Monad.Writer (MonadWriter, WriterT (runWriterT))
+import Data.Foldable (traverse_)
 
 -- | Given a UPLC term, add all of its term definitions and usages, including its subterms,
 -- to a global map.
@@ -40,6 +41,8 @@ handleTerm = \case
         addUsage n ann TermScope
     LamAbs ann n _ ->
         addDef n ann TermScope
+    Let ann ns _ ->
+        traverse_ (\n -> addDef n ann TermScope) ns
     _               -> pure ()
 
 runTermDefs

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Flat.hs

@@ -65,7 +65,7 @@ tags and their used/available encoding possibilities.
 | Data type        | Function          | Bit Width | Total | Used | Remaining |
 |------------------|-------------------|-----------|-------|------|-----------|
 | default builtins | encodeBuiltin     | 7         | 128   | 54   | 74        |
-| Terms            | encodeTerm        | 4         | 16    | 10   | 6         |
+| Terms            | encodeTerm        | 4         | 16    | 10   | 4         |
 
 For format stability we are manually assigning the tag values to the
 constructors (and we do not use a generic algorithm that may change this order).
@@ -114,16 +114,18 @@ encodeTerm
     => Term name uni fun ann
     -> Encoding
 encodeTerm = \case
-    Var      ann n      -> encodeTermTag 0 <> encode ann <> encode n
-    Delay    ann t      -> encodeTermTag 1 <> encode ann <> encodeTerm t
-    LamAbs   ann n t    -> encodeTermTag 2 <> encode ann <> encode (Binder n) <> encodeTerm t
-    Apply    ann t t'   -> encodeTermTag 3 <> encode ann <> encodeTerm t <> encodeTerm t'
-    Constant ann c      -> encodeTermTag 4 <> encode ann <> encode c
-    Force    ann t      -> encodeTermTag 5 <> encode ann <> encodeTerm t
-    Error    ann        -> encodeTermTag 6 <> encode ann
-    Builtin  ann bn     -> encodeTermTag 7 <> encode ann <> encode bn
-    Constr   ann i es   -> encodeTermTag 8 <> encode ann <> encode i <> encodeListWith encodeTerm es
-    Case     ann arg cs -> encodeTermTag 9 <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm (V.toList cs)
+    Var      ann n      -> encodeTermTag 0  <> encode ann <> encode n
+    Delay    ann t      -> encodeTermTag 1  <> encode ann <> encodeTerm t
+    LamAbs   ann n t    -> encodeTermTag 2  <> encode ann <> encode (Binder n) <> encodeTerm t
+    Apply    ann t t'   -> encodeTermTag 3  <> encode ann <> encodeTerm t <> encodeTerm t'
+    Constant ann c      -> encodeTermTag 4  <> encode ann <> encode c
+    Force    ann t      -> encodeTermTag 5  <> encode ann <> encodeTerm t
+    Error    ann        -> encodeTermTag 6  <> encode ann
+    Builtin  ann bn     -> encodeTermTag 7  <> encode ann <> encode bn
+    Constr   ann i es   -> encodeTermTag 8  <> encode ann <> encode i <> encodeListWith encodeTerm es
+    Case     ann arg cs -> encodeTermTag 9  <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm (V.toList cs)
+    Let      ann ns t   -> encodeTermTag 10 <> encode ann <> encode ns <> encodeTerm t
+    Bind     ann t bs   -> encodeTermTag 11 <> encode ann <> encodeTerm t <> encodeListWith encodeTerm bs
 
 decodeTerm
     :: forall name uni fun ann
@@ -161,6 +163,12 @@ decodeTerm version builtinPred = go
         handleTerm 9 = do
             unless (version >= PLC.plcVersion110) $ fail $ "'case' is not allowed before version 1.1.0, this program has version: " ++ (show $ pretty version)
             Case     <$> decode <*> go <*> (V.fromList <$> decodeListWith go)
+        handleTerm 10 = do
+            -- TODO: fail when version is low
+            Let <$> decode <*> decode <*> go
+        handleTerm 11 = do
+            -- TODO: fail when version is low
+            Bind <$> decode <*> go <*> decodeListWith go
         handleTerm t = fail $ "Unknown term constructor tag: " ++ show t
 
 sizeTerm
@@ -189,6 +197,8 @@ sizeTerm tm sz =
     Builtin  ann bn     -> size ann $ size bn sz'
     Constr   ann i es   -> size ann $ size i $ sizeListWith sizeTerm es sz'
     Case     ann arg cs -> size ann $ sizeTerm arg $ sizeListWith sizeTerm (V.toList cs) sz'
+    Let      ann ns t   -> size ann $ size ns $ sizeTerm t sz'
+    Bind     ann t bs   -> size ann $ sizeTerm t $ sizeListWith sizeTerm bs sz'
 
 -- | An encoder for programs.
 --

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Classic.hs

@@ -50,6 +50,14 @@ instance (PrettyClassicBy configName name, PrettyUni uni, Pretty fun, Pretty ann
         Case ann arg cs ->
             sexp "case" (consAnnIf config ann
                 (prettyBy config arg : fmap (prettyBy config) (toList cs)))
+        Let ann names body ->
+          sexp "let" (consAnnIf config ann
+              [ parens' (sep $ prettyBy config <$> names)
+              , prettyBy config body
+              ])
+        Bind ann t binds ->
+          sexp "bind" (consAnnIf config ann
+              (prettyBy config t : (prettyBy config <$> binds)))
       where
         prettyTypeOf :: Some (ValueOf uni) -> Doc dann
         prettyTypeOf (Some (ValueOf uni _ )) = prettyBy juxtRenderContext $ SomeTypeIn uni

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Readable.hs

@@ -12,6 +12,7 @@ module UntypedPlutusCore.Core.Instance.Pretty.Readable () where
 import PlutusCore.Pretty.PrettyConst
 import PlutusCore.Pretty.Readable
 import PlutusPrelude
+import Prettyprinter.Custom (parens')
 import UntypedPlutusCore.Core.Type
 
 import Prettyprinter
@@ -53,6 +54,10 @@ instance
     Constr _ i es -> iterAppDocM $ \_ prettyArg ->
       ("constr" <+> prettyArg i) :| [prettyArg es]
     Case _ arg cs -> iterAppDocM $ \_ prettyArg -> "case" :| [prettyArg arg, prettyArg (toList cs)]
+    Let _ ns t -> iterAppDocM $ \_ prettyArg ->
+      "let" :| [parens' (sep $ prettyArg <$> ns), prettyArg t]
+    Bind _ t bs -> iterAppDocM $ \_ prettyArg ->
+      "bind" :| [prettyArg t, prettyArg bs]
 
 instance
   (PrettyReadableBy configName (Term name uni fun a)) =>

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs

@@ -50,6 +50,10 @@ instance name ~ Name => EstablishScoping (Term name uni fun) where
         -- that none of the transformations leak variables outside of the branch they're bound in.
         pure . referenceOutOfScope branchBounds $
             Case NotAName aScoped . Vector.fromList $ map referenceInBranch esScopedPoked
+    establishScoping (Let _ _ns _t) = error "no"
+    establishScoping (Bind _ _t _bs) = error "no"
+    -- TODO: Current scope checking uses `NameAnn` which only allows a single name to be annotated.
+    -- It's hard to support `Let` and `Bind` which binds multiple names at once
 
 instance name ~ Name => EstablishScoping (Program name uni fun) where
     establishScoping (Program _ ver term) = Program NotAName ver <$> establishScoping term
@@ -65,6 +69,8 @@ instance name ~ Name => CollectScopeInfo (Term name uni fun) where
     collectScopeInfo (Builtin _ _)          = mempty
     collectScopeInfo (Constr _ _ es)        = foldMap collectScopeInfo es
     collectScopeInfo (Case _ arg cs)        = collectScopeInfo arg <> foldMap collectScopeInfo cs
+    collectScopeInfo (Let _ _ns _t)         = error "no"
+    collectScopeInfo (Bind _ _t _bs)        = error "no"
 
 instance name ~ Name => CollectScopeInfo (Program name uni fun) where
     collectScopeInfo (Program _ _ term) = collectScopeInfo term

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs

@@ -32,6 +32,8 @@ termConstants f term0 = case term0 of
     Builtin{}        -> pure term0
     Constr{}         -> pure term0
     Case{}           -> pure term0
+    Let{}            -> pure term0
+    Bind{}           -> pure term0
 
 -- | Get all the direct child 'name a's of the given 'Term' from 'LamAbs'es.
 termBinds :: Traversal' (Term name uni fun ann) name
@@ -55,16 +57,18 @@ termUniques f = \case
 -- | Get all the direct child 'Term's of the given 'Term'.
 termSubterms :: Traversal' (Term name uni fun ann) (Term name uni fun ann)
 termSubterms f = \case
-    LamAbs ann n t    -> LamAbs ann n <$> f t
-    Apply ann t1 t2   -> Apply ann <$> f t1 <*> f t2
-    Delay ann t       -> Delay ann <$> f t
-    Force ann t       -> Force ann <$> f t
-    Constr ann i args -> Constr ann i <$> traverse f args
-    Case ann arg cs   -> Case ann <$> f arg <*> traverse f cs
-    e@Error {}        -> pure e
-    v@Var {}          -> pure v
-    c@Constant {}     -> pure c
-    b@Builtin {}      -> pure b
+    LamAbs ann n t     -> LamAbs ann n <$> f t
+    Apply ann t1 t2    -> Apply ann <$> f t1 <*> f t2
+    Delay ann t        -> Delay ann <$> f t
+    Force ann t        -> Force ann <$> f t
+    Constr ann i args  -> Constr ann i <$> traverse f args
+    Case ann arg cs    -> Case ann <$> f arg <*> traverse f cs
+    Let ann names body -> Let ann names <$> f body
+    Bind ann t binds   -> Bind ann <$> f t <*> traverse f binds
+    e@Error {}         -> pure e
+    v@Var {}           -> pure v
+    c@Constant {}      -> pure c
+    b@Builtin {}       -> pure b
 {-# INLINE termSubterms #-}
 
 -- | Get all the transitive child 'Constant's of the given 'Term'.

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs

@@ -101,6 +101,8 @@ data Term name uni fun ann
     | Constr !ann !Word64 ![Term name uni fun ann]
     -- See Note [Supported case-expressions].
     | Case !ann !(Term name uni fun ann) !(Vector (Term name uni fun ann))
+    | Let !ann ![name] !(Term name uni fun ann)
+    | Bind !ann !(Term name uni fun ann) ![Term name uni fun ann]
     deriving stock (Functor, Generic)
 
 deriving stock instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -168,6 +170,8 @@ termAnn (Force ann _)    = ann
 termAnn (Error ann)      = ann
 termAnn (Constr ann _ _) = ann
 termAnn (Case ann _ _)   = ann
+termAnn (Let ann _ _)    = ann
+termAnn (Bind ann _ _)   = ann
 
 bindFunM
     :: Monad m
@@ -185,6 +189,8 @@ bindFunM f = go where
     go (Error ann)            = pure $ Error ann
     go (Constr ann i args)    = Constr ann i <$> traverse go args
     go (Case ann arg cs)      = Case ann <$> go arg <*> traverse go cs
+    go (Let ann name body)    = Let ann name <$> go body
+    go (Bind ann fun arg)     = Bind ann <$> go fun <*> traverse go arg
 
 bindFun
     :: (ann -> fun -> Term name uni fun' ann)

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs

@@ -93,6 +93,15 @@ deBruijnTermWithM h = go
        Constant ann con -> pure $ Constant ann con
        Builtin ann bn -> pure $ Builtin ann bn
        Error ann -> pure $ Error ann
+       Let ann names body -> do
+         let
+           goNames acc [] = Let ann (acc []) <$> go body
+           goNames acc (n:ns) = declareUnique n $ do
+             n' <- nameToDeBruijn h n
+             withScope $ do
+               goNames (acc . (n':)) ns
+         goNames id names
+       Bind ann t binds -> Bind ann <$> go t <*> traverse go binds
 
 -- | Takes a "handler" function to execute when encountering free variables.
 unDeBruijnTermWithM
@@ -121,3 +130,12 @@ unDeBruijnTermWithM h = go
         Constant ann con -> pure $ Constant ann con
         Builtin ann bn -> pure $ Builtin ann bn
         Error ann -> pure $ Error ann
+        Let ann names body -> do
+          let
+            goNames acc [] = Let ann (acc []) <$> go body
+            goNames acc (n:ns) = declareBinder $ do
+              n' <- deBruijnToName h $ set index deBruijnInitIndex n
+              withScope $ do
+                goNames (acc . (n':)) ns
+          goNames id names
+        Bind ann t binds -> Bind ann <$> go t <*> traverse go binds

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

@@ -308,6 +308,7 @@ data CekValue uni fun ann =
       -- Check the docs of 'BuiltinRuntime' for details.
     -- | A constructor value, including fully computed arguments and the tag.
   | VConstr {-# UNPACK #-} !Word64 !(EmptyOrMultiStack uni fun ann)
+  | VLet ![NamedDeBruijn] !(NTerm uni fun ann) !(CekValEnv uni fun ann)
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
     => Show (CekValue uni fun ann)
@@ -639,6 +640,11 @@ dischargeCekValue value0     = DischargeNonConstant $ goValue value0 where
         -- @term@ is fully discharged, so we can return it directly without any further discharging.
         VBuiltin _ term _ -> term
         VConstr ind args -> Constr () ind . map goValue $ argStackToList args
+        VLet names body env ->
+          Let
+            ()
+            ((\(NamedDeBruijn n _ix) -> NamedDeBruijn n deBruijnInitIndex) <$> names)
+            (goValEnv env 1 body)
 
     -- Instantiate all the free variables of a term by looking them up in an environment.
     -- Mutually recursive with @goValue@.
@@ -669,6 +675,8 @@ dischargeCekValue value0     = DischargeNonConstant $ goValue value0 where
           Error _            -> Error ()
           Constr _ ind args  -> Constr () ind $ map (go shift) args
           Case _ scrut alts  -> Case () (go shift scrut) $ fmap (go shift) alts
+          Let _ names body   -> Let () names (go (shift + fromIntegral (length names)) body)
+          Bind _ t bs        -> Bind () (go shift t) (fmap (go shift) bs)
 
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
     prettyBy cfg = prettyBy cfg . dischargeResultToTerm . dischargeCekValue
@@ -705,6 +713,8 @@ data Context uni fun ann
     -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
     | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
     -- ^ @(case _ C0 .. Cn)@
+    | FrameAwaitLetBinds !(CekValEnv uni fun ann) !(NTerm uni fun ann) ![NTerm uni fun ann] ![CekValue uni fun ann] !(Context uni fun ann)
+    | FrameMine ![CekValue uni fun ann] !(Context uni fun ann)
     | NoFrame
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -718,6 +728,7 @@ instance (Closed uni, uni `Everywhere` ExMemoryUsage) => ExMemoryUsage (CekValue
         VLamAbs {}  -> singletonRose 1
         VBuiltin {} -> singletonRose 1
         VConstr {}  -> singletonRose 1
+        VLet {}  -> singletonRose 1
     {-# INLINE memoryUsage #-}
 
 {- Note [ArgStack vs Spine]
@@ -832,6 +843,16 @@ enterComputeCek = computeCek
     -- s ; ρ ▻ error  ↦  <> A
     computeCek !_ !_ (Error _) =
         throwErrorWithCause (OperationalError CekEvaluationFailure) (Error ())
+    -- ???
+    computeCek !ctx !env (Let _ names body) = do
+        stepAndMaybeSpend BLamAbs
+        returnCek ctx (VLet names body env)
+    computeCek !ctx !env (Bind _ body bs) = do
+        --stepAndMaybeSpend BApply
+        -- computeCek (FrameAwaitLetBinds env t bs ctx) env t
+        case bs of
+          (t : rest) -> computeCek (FrameAwaitLetBinds env body rest [] ctx) env t
+          []         -> computeCek ctx env body
 
     {- | The returning phase of the CEK machine.
     Returns 'EvaluationSuccess' in case the context is empty, otherwise pops up one frame
@@ -871,6 +892,12 @@ enterComputeCek = computeCek
         SpineLast arg      -> applyEvaluate ctx fun (VCon arg)
         SpineCons arg rest -> applyEvaluate (FrameAwaitFunConN rest ctx) fun (VCon arg)
     -- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
+    returnCek (FrameMine args ctx) l =
+      case l of
+        VLet names body env
+          | length names == length args -> computeCek ctx (foldr Env.cons env args) body
+        _               -> error "no"
+
     returnCek (FrameAwaitFunValueN args ctx) fun =
         case args of
           LastStackNonEmpty arg ->
@@ -905,6 +932,14 @@ enterComputeCek = computeCek
             Right (HeadOnly fX) -> computeCek ctx env fX
             Right (HeadSpine f xs) -> computeCek (FrameAwaitFunConN xs ctx) env f
         _ -> throwErrorDischarged (StructuralError NonConstrScrutinizedMachineError) e
+    -- returnCek (FrameAwaitLetTerm env bs ctx) e =
+    --   case bs of
+    --     (next : todo) -> computeCek (FrameAwaitLetBinds env e todo [] ctx) env next
+        -- [] -> returnCek ctx e -- no bindings
+    returnCek (FrameAwaitLetBinds env l todo done ctx) e =
+      case todo of
+        (next : todo') -> computeCek (FrameAwaitLetBinds env l todo' (e : done) ctx) env next
+        []             -> computeCek (FrameMine (e : done) ctx) env l
 
     -- | @force@ a term and proceed.
     -- If v is a delay then compute the body of v;

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Parser.hs

@@ -90,6 +90,20 @@ caseTerm = withSpan $ \sp ->
       whenVersion (\v -> v < plcVersion110) $ fail "'case' is not allowed before version 1.1.0"
       pure res
 
+letTerm :: Parser PTerm
+letTerm = withSpan $ \sp ->
+  inParens $ symbol "let" *> do
+    res <- UPLC.Let sp <$> (inParens $ many (leadingWhitespace name)) <*> term
+    -- TODO: version check
+    pure res
+
+bindTerm :: Parser PTerm
+bindTerm = withSpan $ \sp ->
+  inParens $ symbol "bind" *> do
+    res <- UPLC.Bind sp <$> term <*> (many term)
+    -- TODO: version check
+    pure res
+
 -- | Parser for all UPLC terms.
 term :: Parser PTerm
 term = leadingWhitespace go
@@ -106,6 +120,8 @@ term = leadingWhitespace go
             , errorTerm
             , constrTerm
             , caseTerm
+            , letTerm
+            , bindTerm
             ]
 
 -- | Parser for UPLC programs.

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs

@@ -35,6 +35,12 @@ renameTermM (Constr ann i es)          = Constr ann i <$> traverse renameTermM e
 renameTermM (Case ann arg cs)          = Case ann <$> renameTermM arg <*> traverse renameTermM cs
 renameTermM con@Constant{}             = pure con
 renameTermM bi@Builtin{}               = pure bi
+renameTermM (Let ann names body)       =
+  let
+    goNames acc []     = Let ann (acc []) <$> renameTermM body
+    goNames acc (n:ns) = withFreshenedName n $ \n' -> goNames (acc . (n':)) ns
+  in goNames id names
+renameTermM (Bind ann t binds) = Bind ann <$> renameTermM t <*> traverse renameTermM binds
 
 -- | Rename a 'Program' in the 'RenameM' monad.
 renameProgramM

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Subst.hs

@@ -72,6 +72,8 @@ termMapNames f = go
             Force ann t          -> Force ann (go t)
             Constr ann i es      -> Constr ann i (fmap go es)
             Case ann arg cs      -> Case ann (go arg) (fmap go cs)
+            Let ann ns t         -> Let ann (fmap f ns) (go t)
+            Bind ann t bs        -> Bind ann (go t) (fmap go bs)
 
             Constant ann c       -> Constant ann c
             Builtin ann b        -> Builtin ann b