WIP

plutus-benchmark/validation/Main.hs

@@ -29,7 +29,7 @@ import           Text.Printf                              (printf)
   source code, along with README files explaining which scripts were involved in
   each validation during the tests.  --}
 
-type Term a    = UPLC.Term (UPLC.GName PLC.Name) PLC.DefaultUni PLC.DefaultFun a
+type Term a    = UPLC.Term PLC.Name PLC.DefaultUni PLC.DefaultFun a
 type Program a = UPLC.Program PLC.Name PLC.DefaultUni PLC.DefaultFun a
 type PlcParserError = PLC.Error PLC.DefaultUni PLC.DefaultFun PLC.AlexPosn
 

plutus-core/common/PlcTestUtils.hs

@@ -84,7 +84,7 @@ runTPlc values = do
 runUPlc
     :: ToUPlc a DefaultUni TPLC.DefaultFun
     => [a]
-    -> ExceptT SomeException IO (UPLC.EvaluationResult (UPLC.Term (UPLC.GName TPLC.Name) DefaultUni TPLC.DefaultFun ()))
+    -> ExceptT SomeException IO (UPLC.EvaluationResult (UPLC.Term TPLC.Name DefaultUni TPLC.DefaultFun ()))
 runUPlc values = do
     ps <- traverse toUPlc values
     let (UPLC.Program _ _ t) = foldl1 UPLC.applyProgram ps

plutus-core/generators/PlutusCore/Generators/NEAT/Spec.hs

@@ -115,7 +115,7 @@ handleError ty e = case U._ewcError e of
 handleUError ::
           U.ErrorWithCause (U.EvaluationError user internal) term
        -> Either (U.ErrorWithCause (U.EvaluationError user internal) term)
-                 (U.Term (U.GName Name) DefaultUni DefaultFun ())
+                 (U.Term Name DefaultUni DefaultFun ())
 handleUError e = case U._ewcError e of
   U.UserEvaluationError     _ -> return (U.Error ())
   U.InternalEvaluationError _ -> throwError e
@@ -158,11 +158,11 @@ prop_agree_termEval tyG tmG = do
     evaluateCkNoEmit defaultBuiltinsRuntime tm `catchError` handleError ty
 
   -- erase CK output
-  let tmUCk = U.globalifyTerm $ U.erase tmCk
+  let tmUCk = U.erase tmCk
 
   -- run untyped CEK on erased input
   tmUCek <- withExceptT UCekP $ liftEither $
-    U.evaluateCekNoEmit defaultCekParameters (U.globalifyTerm $ U.erase tm) `catchError` handleUError
+    U.evaluateCekNoEmit defaultCekParameters (U.erase tm) `catchError` handleUError
 
   -- check if typed CK and untyped CEK give the same output modulo erasure
   unless (tmUCk == tmUCek) $
@@ -307,7 +307,7 @@ data Ctrex
   | CtrexUntypedTermEvaluationMismatch
     ClosedTypeG
     ClosedTermG
-    [U.Term (U.GName Name) DefaultUni DefaultFun ()]
+    [U.Term Name DefaultUni DefaultFun ()]
 
 instance Show TestFail where
   show (TypeError e)  = show e

plutus-core/plc/Main.hs

@@ -853,7 +853,7 @@ runEval (EvalOptions language inp ifmt evalMode printMode budgetMode timingMode
             CK  -> errorWithoutStackTrace "There is no CK machine for Untyped Plutus Core"
             CEK -> do
                   UntypedProgram prog <- getProgram UntypedPLC ifmt inp
-                  let term = void . UPLC.globalifyTerm $ UPLC.toTerm $ prog
+                  let term = UPLC.globalifyTerm $ void $ UPLC.toTerm $ prog
                       !_ = rnf term
                       cekparams = case cekModel of
                                 Default -> PLC.defaultCekParameters  -- AST nodes are charged according to the default cost model

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExMemory.hs

@@ -25,7 +25,7 @@ import           Data.Aeson
 import qualified Data.ByteString            as BS
 import           Data.Proxy
 import           Data.SatInt
-import qualified Data.Text                as T
+import qualified Data.Text                  as T
 import           Data.Word
 import           GHC.Generics
 import           GHC.Integer
@@ -189,7 +189,7 @@ instance ExMemoryUsage Integer where
   memoryUsage 0 = ExMemory 1  -- integerLog2# is unspecified for 0, but in practice returns -1
   memoryUsage i = ExMemory . fromIntegral $ (1 + smallInteger (integerLog2# (abs i) `quotInt#` integerToInt 64)) -- Assume 64bit size.
 
-instance ExMemoryUsage Word64 where
+instance ExMemoryUsage Word where
     memoryUsage _ = 1
 
 instance ExMemoryUsage BS.ByteString where

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

@@ -30,6 +30,8 @@ instance ( Closed uni
         Force    ann t    -> encodeConstructorTag 5 <> encode ann <> encode t
         Error    ann      -> encodeConstructorTag 6 <> encode ann
         Builtin  ann bn   -> encodeConstructorTag 7 <> encode ann <> encode bn
+        GVar      ann n   -> encodeConstructorTag 8 <> encode ann <> encode n
+        LamAbs   ann n t  -> encodeConstructorTag 9 <> encode ann <> encode n <> encode t
 
     decode = go =<< decodeConstructorTag
         where go 0 = Var      <$> decode <*> decode
@@ -40,6 +42,8 @@ instance ( Closed uni
               go 5 = Force    <$> decode <*> decode
               go 6 = Error    <$> decode
               go 7 = Builtin  <$> decode <*> decode
+              go 8 = GVar      <$> decode <*> decode
+              go 9 = GLamAbs   <$> decode <*> decode <*> decode
               go _ = fail "Failed to decode Term TyName Name ()"
 
 instance ( Closed uni

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

@@ -29,8 +29,13 @@ eqTermM (Builtin _ bi1) (Builtin _ bi2) =
     eqM bi1 bi2
 eqTermM (Var _ name1) (Var _ name2) =
     eqNameM name1 name2
+eqTermM (GVar _ name1) (GVar _ name2) =
+    eqM name1 name2
 eqTermM (LamAbs _ name1 body1) (LamAbs _ name2 body2) =
     withTwinBindings name1 name2 $ eqTermM body1 body2
+eqTermM (GLamAbs _ name1 body1) (GLamAbs _ name2 body2) = do
+    eqM name1 name2
+    eqTermM body1 body2
 eqTermM (Apply _ fun1 arg1) (Apply _ fun2 arg2) = do
     eqTermM fun1 fun2
     eqTermM arg1 arg2
@@ -42,7 +47,9 @@ eqTermM (Error _) (Error _) = pure ()
 eqTermM Constant{} _ = empty
 eqTermM Builtin{}  _ = empty
 eqTermM Var{}      _ = empty
+eqTermM GVar{}      _ = empty
 eqTermM LamAbs{}   _ = empty
+eqTermM GLamAbs{}   _ = empty
 eqTermM Apply{}    _ = empty
 eqTermM Delay{}    _ = empty
 eqTermM Force{}    _ = empty

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

@@ -94,6 +94,8 @@ instance ( Closed uni
         Force    ann t    -> encodeTerm 5 <> encode ann <> encode t
         Error    ann      -> encodeTerm 6 <> encode ann
         Builtin  ann bn   -> encodeTerm 7 <> encode ann <> encode bn
+        GVar      ann n   -> encodeTerm 8 <> encode ann <> encode n
+        GLamAbs   ann n t -> encodeTerm 9 <> encode ann <> encode n <> encode t
 
     decode = go =<< decodeTerm
         where go 0 = Var      <$> decode <*> decode
@@ -104,12 +106,16 @@ instance ( Closed uni
               go 5 = Force    <$> decode <*> decode
               go 6 = Error    <$> decode
               go 7 = Builtin  <$> decode <*> decode
+              go 8 = GVar  <$> decode <*> decode
+              go 9 = GLamAbs   <$> decode <*> decode <*> decode
               go _ = fail "Failed to decode Term Name ()"
 
     size tm sz = termTagWidth + sz + case tm of
         Var      ann n    -> getSize ann + getSize n
+        GVar      ann n   -> getSize ann + getSize n
         Delay    ann t    -> getSize ann + getSize t
         LamAbs   ann n t  -> getSize ann + getSize n + getSize t
+        GLamAbs   ann n t -> getSize ann + getSize n + getSize t
         Apply    ann t t' -> getSize ann + getSize t + getSize t'
         Constant ann c    -> getSize ann + getSize c
         Force    ann t    -> getSize ann + getSize t

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

@@ -27,14 +27,16 @@ instance
         , GShow uni, Closed uni, uni `Everywhere` PrettyConst, Pretty fun
         ) => PrettyBy (PrettyConfigClassic configName) (Term name uni fun a) where
     prettyBy config = go where
-        go (Constant _ val)     = parens' $ "con" </> prettyTypeOf val </> pretty val  -- NB: actually calls prettyConst
-        go (Builtin _ bi)       = parens' $ "builtin" </> pretty bi
-        go (Var _ name)         = prettyName name
-        go (LamAbs _ name body) = parens' $ "lam" </> vsep' [prettyName name, go body]
-        go (Apply _ fun arg)    = brackets' $ vsep' [go fun, go arg]
-        go (Delay _ term)       = parens' ("delay" </> go term)
-        go (Force _ term)       = parens' ("force" </> go term)
-        go (Error _)            = parens' "error"
+        go (Constant _ val)      = parens' $ "con" </> prettyTypeOf val </> pretty val  -- NB: actually calls prettyConst
+        go (Builtin _ bi)        = parens' $ "builtin" </> pretty bi
+        go (Var _ name)          = prettyName name
+        go (GVar _ name)         = pretty name
+        go (LamAbs _ name body)  = parens' $ "lam" </> vsep' [prettyName name, go body]
+        go (GLamAbs _ name body) = parens' $ "glam" </> vsep' [prettyName name, go body]
+        go (Apply _ fun arg)     = brackets' $ vsep' [go fun, go arg]
+        go (Delay _ term)        = parens' ("delay" </> go term)
+        go (Force _ term)        = parens' ("force" </> go term)
+        go (Error _)             = parens' "error"
 
         prettyName :: PrettyClassicBy configName n => n -> Doc ann
         prettyName = prettyBy config

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

@@ -29,10 +29,15 @@ instance
         Constant _ val -> unitDocM $ pretty val
         Builtin _ bi -> unitDocM $ pretty bi
         Var _ name -> prettyM name
+        GVar _ name -> prettyM name
         LamAbs _ name body ->
             compoundDocM binderFixity $ \prettyIn ->
                 let prettyBot x = prettyIn ToTheRight botFixity x
                 in "\\" <> prettyBot name <+> "->" <+> prettyBot body
+        GLamAbs _ name body ->
+            compoundDocM binderFixity $ \prettyIn ->
+                let prettyBot x = prettyIn ToTheRight botFixity x
+                in "\\g" <> prettyBot name <+> "->" <+> prettyBot body
         Apply _ fun arg -> fun `juxtPrettyM` arg
         Delay _ term ->
             sequenceDocM ToTheRight juxtFixity $ \prettyEl ->

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

@@ -40,11 +40,13 @@ termUniques f = \case
 termSubterms :: Traversal' (Term name uni fun ann) (Term name uni fun ann)
 termSubterms f = \case
     LamAbs ann n t  -> LamAbs ann n <$> f t
+    GLamAbs ann n t -> GLamAbs 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
     e@Error {}      -> pure e
     v@Var {}        -> pure v
+    v@GVar {}       -> pure v
     c@Constant {}   -> pure c
     b@Builtin {}    -> pure b
 

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

@@ -12,7 +12,6 @@ module UntypedPlutusCore.Core.Type
     , TPLC.Version (..)
     , Term (..)
     , Program (..)
-    , GName (..)
     , toTerm
     , bindFunM
     , bindFun
@@ -23,10 +22,8 @@ module UntypedPlutusCore.Core.Type
     ) where
 
 import           Data.Functor.Identity
-import           Data.Text.Prettyprint.Doc
 import           PlutusPrelude
 
-import           Data.Word
 import qualified PlutusCore.Constant                    as TPLC
 import qualified PlutusCore.Core                        as TPLC
 import           PlutusCore.Evaluation.Machine.ExBudget
@@ -35,31 +32,6 @@ import           PlutusCore.MkPlc
 import qualified PlutusCore.Name                        as TPLC
 import           Universe
 
--- | A global name ('GName') or an underlying name.
-data GName name = GName {-# UNPACK #-} !Word64 | NName !name
-    deriving stock (Show, Eq, Ord, Generic)
-    deriving anyclass (NFData)
-
-instance Pretty name => Pretty (GName name) where
-    pretty (GName w) = "global" <+> pretty w
-    pretty (NName n) = pretty n
-
-instance PrettyBy config name => PrettyBy config (GName name) where
-    prettyBy _ (GName w)      = "global" <+> pretty w
-    prettyBy config (NName n) = prettyBy config n
-
--- HACK: this instance should not exist, I just did it so 'termSubstFreeNames' would be happy,
--- even though it only really needs a prism.
-instance TPLC.HasUnique name TPLC.TermUnique => TPLC.HasUnique (GName name) TPLC.TermUnique where
-     unique = lens g s
-         where
-             g :: GName name -> TPLC.TermUnique
-             g (NName n) = view TPLC.unique n
-             g (GName _) = coerce (TPLC.Unique 0)
-             s :: GName name -> TPLC.TermUnique -> GName name
-             s (NName n) u   = NName (set TPLC.unique u n)
-             s n@(GName{}) _ = n
-
 {-| The type of Untyped Plutus Core terms. Mirrors the type of Typed Plutus Core terms except
 
 1. all types are removed
@@ -79,7 +51,9 @@ data Term name uni fun ann
     = Constant !ann !(Some (ValueOf uni))
     | Builtin !ann !fun
     | Var !ann !name
+    | GVar !ann !Word
     | LamAbs !ann !name !(Term name uni fun ann)
+    | GLamAbs !ann !Word !(Term name uni fun ann)
     | Apply !ann !(Term name uni fun ann) !(Term name uni fun ann)
     | Delay !ann !(Term name uni fun ann)
     | Force !ann !(Term name uni fun ann)
@@ -132,29 +106,33 @@ toTerm (Program _ _ term) = term
 
 -- | Return the outermost annotation of a 'Term'.
 termAnn :: Term name uni fun ann -> ann
-termAnn (Constant ann _) = ann
-termAnn (Builtin ann _)  = ann
-termAnn (Var ann _)      = ann
-termAnn (LamAbs ann _ _) = ann
-termAnn (Apply ann _ _)  = ann
-termAnn (Delay ann _)    = ann
-termAnn (Force ann _)    = ann
-termAnn (Error ann)      = ann
+termAnn (Constant ann _)  = ann
+termAnn (Builtin ann _)   = ann
+termAnn (Var ann _)       = ann
+termAnn (GVar ann _)      = ann
+termAnn (LamAbs ann _ _)  = ann
+termAnn (GLamAbs ann _ _) = ann
+termAnn (Apply ann _ _)   = ann
+termAnn (Delay ann _)     = ann
+termAnn (Force ann _)     = ann
+termAnn (Error ann)       = ann
 
 bindFunM
     :: Monad m
     => (ann -> fun -> m (Term name uni fun' ann))
     -> Term name uni fun ann
     -> m (Term name uni fun' ann)
 bindFunM f = go where
-    go (Constant ann val)     = pure $ Constant ann val
-    go (Builtin ann fun)      = f ann fun
-    go (Var ann name)         = pure $ Var ann name
-    go (LamAbs ann name body) = LamAbs ann name <$> go body
-    go (Apply ann fun arg)    = Apply ann <$> go fun <*> go arg
-    go (Delay ann term)       = Delay ann <$> go term
-    go (Force ann term)       = Force ann <$> go term
-    go (Error ann)            = pure $ Error ann
+    go (Constant ann val)      = pure $ Constant ann val
+    go (Builtin ann fun)       = f ann fun
+    go (Var ann name)          = pure $ Var ann name
+    go (GVar ann name)         = pure $ GVar ann name
+    go (LamAbs ann name body)  = LamAbs ann name <$> go body
+    go (GLamAbs ann name body) = GLamAbs ann name <$> go body
+    go (Apply ann fun arg)     = Apply ann <$> go fun <*> go arg
+    go (Delay ann term)        = Delay ann <$> go term
+    go (Force ann term)        = Force ann <$> go term
+    go (Error ann)             = pure $ Error ann
 
 bindFun
     :: (ann -> fun -> Term name uni fun' ann)

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

@@ -72,8 +72,8 @@ runCekNoEmit
     :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
     => MachineParameters CekMachineCosts CekValue uni fun
     -> ExBudgetMode cost uni fun
-    -> Term (GName Name) uni fun ()
-    -> (Either (CekEvaluationException uni fun) (Term (GName Name) uni fun ()), cost)
+    -> Term Name uni fun ()
+    -> (Either (CekEvaluationException uni fun) (Term Name uni fun ()), cost)
 runCekNoEmit params mode term =
     case runCek params mode False term of
         (errOrRes, cost', _) -> (errOrRes, cost')
@@ -87,17 +87,17 @@ unsafeRunCekNoEmit
        )
     => MachineParameters CekMachineCosts CekValue uni fun
     -> ExBudgetMode cost uni fun
-    -> Term (GName Name) uni fun ()
-    -> (EvaluationResult (Term (GName Name) uni fun ()), cost)
+    -> Term Name uni fun ()
+    -> (EvaluationResult (Term Name uni fun ()), cost)
 unsafeRunCekNoEmit params mode =
     first unsafeExtractEvaluationResult . runCekNoEmit params mode
 
 -- | Evaluate a term using the CEK machine with logging enabled.
 evaluateCek
     :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
     => MachineParameters CekMachineCosts CekValue uni fun
-    -> Term (GName Name) uni fun ()
-    -> (Either (CekEvaluationException uni fun) (Term (GName Name) uni fun ()), [String])
+    -> Term Name uni fun ()
+    -> (Either (CekEvaluationException uni fun) (Term Name uni fun ()), [String])
 evaluateCek params term =
     case runCek params restrictingEnormous True term of
         (errOrRes, _, logs) -> (errOrRes, logs)
@@ -106,8 +106,8 @@ evaluateCek params term =
 evaluateCekNoEmit
     :: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
     => MachineParameters CekMachineCosts CekValue uni fun
-    -> Term (GName Name) uni fun ()
-    -> Either (CekEvaluationException uni fun) (Term (GName Name) uni fun ())
+    -> Term Name uni fun ()
+    -> Either (CekEvaluationException uni fun) (Term Name uni fun ())
 evaluateCekNoEmit params = fst . runCekNoEmit params restrictingEnormous
 
 -- | Evaluate a term using the CEK machine with logging enabled. May throw a 'CekMachineException'.
@@ -117,8 +117,8 @@ unsafeEvaluateCek
        , Ix fun, Pretty fun, Typeable fun
        )
     => MachineParameters CekMachineCosts CekValue uni fun
-    -> Term (GName Name) uni fun ()
-    -> (EvaluationResult (Term (GName Name) uni fun ()), [String])
+    -> Term Name uni fun ()
+    -> (EvaluationResult (Term Name uni fun ()), [String])
 unsafeEvaluateCek params = first unsafeExtractEvaluationResult . evaluateCek params
 
 -- | Evaluate a term using the CEK machine with logging disabled. May throw a 'CekMachineException'.
@@ -128,17 +128,17 @@ unsafeEvaluateCekNoEmit
        , Ix fun, Pretty fun, Typeable fun
        )
     => MachineParameters CekMachineCosts CekValue uni fun
-    -> Term (GName Name) uni fun ()
-    -> EvaluationResult (Term (GName Name) uni fun ())
+    -> Term Name uni fun ()
+    -> EvaluationResult (Term Name uni fun ())
 unsafeEvaluateCekNoEmit params = unsafeExtractEvaluationResult . evaluateCekNoEmit params
 
 -- | Unlift a value using the CEK machine.
 readKnownCek
     :: ( uni `Everywhere` ExMemoryUsage
-       , KnownType (Term (GName Name) uni fun ()) a
+       , KnownType (Term Name uni fun ()) a
        , Ix fun, PrettyUni uni fun
        )
     => MachineParameters CekMachineCosts CekValue uni fun
-    -> Term (GName Name) uni fun ()
+    -> Term Name uni fun ()
     -> Either (CekEvaluationException uni fun) a
 readKnownCek params = evaluateCekNoEmit params >=> readKnown