Rebase pretty-printing for Rocq cert and get everything compiling

Author: jaccokrijnen

plutus-core/executables/plutus/AnyProgram/Compile.hs

@@ -79,9 +79,9 @@ compileProgram = curry $ \case
     -- pir to plc
     ----------------------------------------
     (SPir n1@SName a1, SPlc n2 SUnit) ->
-      withA @Ord a1 $ withA @Pretty a1 $ withA @AnnInline a1 $
+      withA @Ord a1 $ withA @Pretty a1 $ withA @Show a1 $ withA @AnnInline a1 $
         -- Note: PIR.compileProgram subsumes pir typechecking
-        (PLC.runQuoteT . flip runReaderT compCtx . PIR.compileProgram)
+        (PLC.runQuoteT . flip runReaderT compCtx . PIR.compileProgram (const (return ())))
         >=> plcToOutName n1 n2
         -- completely drop annotations for now
         >=> pure . void

plutus-core/plutus-core.cabal

@@ -1,7 +1,7 @@
-cabal-version:   3.0
-name:            plutus-core
-version:         1.46.0.0
-license:         Apache-2.0
+cabal-version:      3.0
+name:               plutus-core
+version:            1.46.0.0
+license:            Apache-2.0
 license-files:
   LICENSE
   NOTICE
@@ -521,6 +521,7 @@ library plutus-ir
     PlutusIR.Core.Instance.Pretty
     PlutusIR.Core.Instance.Pretty.Readable
     PlutusIR.Core.Instance.Scoping
+    PlutusIR.Core.Instance.ShowRocq
     PlutusIR.Core.Plated
     PlutusIR.Core.Type
     PlutusIR.Error
@@ -570,6 +571,7 @@ library plutus-ir
   build-depends:
     , algebraic-graphs     >=0.7
     , base                 >=4.9     && <5
+    , bytestring
     , containers
     , data-default-class
     , dlist
@@ -591,6 +593,7 @@ library plutus-ir
     , semigroups           >=0.19.1
     , text
     , transformers
+    , vector
     , witherable
 
 test-suite plutus-ir-test

plutus-core/plutus-core/src/PlutusCore/Core/Type.hs

@@ -41,6 +41,8 @@ module PlutusCore.Core.Type
     , termAnn
     , typeAnn
     , mapFun
+    , mapUniType
+    , mapUniTerm
     , tyVarDeclAnn
     , tyVarDeclName
     , tyVarDeclKind
@@ -185,15 +187,43 @@ data TyVarDecl tyname ann = TyVarDecl
     { _tyVarDeclAnn  :: ann
     , _tyVarDeclName :: tyname
     , _tyVarDeclKind :: Kind ann
-    } deriving stock (Functor, Show, Generic)
+    } deriving stock (Functor, Generic)
+
+-- | Custom instance that behaves as a derived instance of Show, but without record syntax.
+-- Used in the Rocq PIR certifier dumping format.
+instance (Show tn, Show ann) => Show (TyVarDecl tn ann) where
+  showsPrec p (TyVarDecl x y z) =
+    showParen (p >= 11) $
+      showString "TyVarDecl" .
+      showString " " .
+      showsPrec 11 x .
+      showString " " .
+      showsPrec 11 y .
+      showString " " .
+      showsPrec 11 z
+
 makeLenses ''TyVarDecl
 
 -- | A "variable declaration", i.e. a name and a type for a variable.
 data VarDecl tyname name uni ann = VarDecl
     { _varDeclAnn  :: ann
     , _varDeclName :: name
     , _varDeclType :: Type tyname uni ann
-    } deriving stock (Functor, Show, Generic)
+    } deriving stock (Functor, Generic)
+
+-- | Custom instance that behaves as a derived instance of Show, but without record syntax.
+-- Used in the Rocq PIR certifier dumping format.
+instance (Show tn, Show ann, GShow uni, Show n) => Show (VarDecl tn n uni ann) where
+  showsPrec p (VarDecl x y z) =
+    showParen (p >= 11) $
+      showString "VarDecl" .
+      showString " " .
+      showsPrec 11 x .
+      showString " " .
+      showsPrec 11 y .
+      showString " " .
+      showsPrec 11 z
+
 makeLenses ''VarDecl
 
 -- | A "type declaration", i.e. a kind for a type.
@@ -270,6 +300,43 @@ mapFun f = go where
     go (Constr ann ty i args)     = Constr ann ty i (map go args)
     go (Case ann ty arg cs)       = Case ann ty (go arg) (map go cs)
 
+mapUniType
+    :: forall uni uni' tyname ann.
+       (SomeTypeIn uni -> SomeTypeIn uni')
+    -> Type tyname uni ann
+    -> Type tyname uni' ann
+mapUniType f = go where
+    go :: Type tyname uni ann -> Type tyname uni' ann
+    go (TyVar ann name)        = TyVar ann name
+    go (TyFun ann ty1 ty2)     = TyFun ann (go ty1) (go ty2)
+    go (TyIFix ann ty1 ty2)    = TyIFix ann (go ty1) (go ty2)
+    go (TyForall ann name k t) = TyForall ann name k (go t)
+    go (TyBuiltin ann con)     = TyBuiltin ann (f con)
+    go (TyLam ann name k t)    = TyLam ann name k (go t)
+    go (TyApp ann t1 t2)       = TyApp ann (go t1) (go t2)
+    go (TySOP ann tys)         = TySOP ann (map (map go) tys)
+
+mapUniTerm
+    :: forall uni uni' tyname name fun ann.
+       (SomeTypeIn uni -> SomeTypeIn uni')
+    -> (Some (ValueOf uni) -> Some (ValueOf uni'))
+    -> Term tyname name uni fun ann
+    -> Term tyname name uni' fun ann
+mapUniTerm fTy fCon = go where
+    go :: Term tyname name uni fun ann -> Term tyname name uni' fun ann
+    go (LamAbs ann name ty body)  = LamAbs ann name (mapUniType fTy ty) (go body)
+    go (TyAbs ann name kind body) = TyAbs ann name kind (go body)
+    go (IWrap ann pat arg term)   = IWrap ann (mapUniType fTy pat) (mapUniType fTy arg) (go term)
+    go (Apply ann fun arg)        = Apply ann (go fun) (go arg)
+    go (Unwrap ann term)          = Unwrap ann (go term)
+    go (Error ann ty)             = Error ann (mapUniType fTy ty)
+    go (TyInst ann term ty)       = TyInst ann (go term) (mapUniType fTy ty)
+    go (Var ann name)             = Var ann name
+    go (Constant ann con)         = Constant ann (fCon con)
+    go (Builtin ann fun)          = Builtin ann fun
+    go (Constr ann ty i args)     = Constr ann (mapUniType fTy ty) i (map go args)
+    go (Case ann ty arg cs)       = Case ann (mapUniType fTy ty) (go arg) (map go cs)
+
 -- | This is a wrapper to mark the place where the binder is introduced (i.e. LamAbs/TyAbs)
 -- and not where it is actually used (TyVar/Var..).
 -- This marking allows us to skip the (de)serialization of binders at LamAbs/TyAbs positions

plutus-core/plutus-core/src/PlutusCore/Name/Unique.hs

@@ -60,7 +60,7 @@ data Name = Name
   , _nameUnique :: Unique
   -- ^ A 'Unique' assigned to the name, allowing for cheap comparisons in the compiler.
   }
-  deriving stock (Show, Generic, Lift)
+  deriving stock (Generic, Lift, Show)
   deriving anyclass (NFData)
 
 -- | Allowed characters in the starting position of a non-quoted identifier.
@@ -93,7 +93,7 @@ toPrintedName txt = if isValidUnquotedName txt then txt else "`" <> txt <> "`"
 those used for terms.
 -}
 newtype TyName = TyName {unTyName :: Name}
-  deriving stock (Show, Generic, Lift)
+  deriving stock (Generic, Lift, Show)
   deriving newtype (Eq, Ord, NFData, Hashable, PrettyBy config)
 
 instance Wrapped TyName
@@ -123,7 +123,7 @@ instance Hashable Name where
 
 -- | A unique identifier
 newtype Unique = Unique {unUnique :: Int}
-  deriving stock (Eq, Show, Ord, Lift)
+  deriving stock (Eq, Ord, Lift, Generic, Show)
   deriving newtype (Enum, NFData, Pretty, Hashable)
 
 -- | The unique of a type-level name.

plutus-core/plutus-ir/src/PlutusIR/Compiler.hs

@@ -61,6 +61,7 @@ import Control.Monad.Except
 import Control.Monad.Extra (orM, whenM)
 import Data.Monoid
 import Data.Monoid.Extra (mwhen)
+import Data.Text (Text)
 import Debug.Trace (traceM)
 import PlutusCore qualified as PLC
 import PlutusCore.Error (throwingEither)
@@ -89,6 +90,8 @@ import PlutusIR.Transform.ThunkRecursions qualified as ThunkRec
 import PlutusIR.Transform.Unwrap qualified as Unwrap
 import PlutusPrelude
 
+import PlutusIR.Core.Instance.ShowRocq
+
 isVerbose :: Compiling m e uni fun a => m Bool
 isVerbose = view $ ccOpts . coVerbose
 
@@ -101,11 +104,18 @@ logVerbose = whenM (orM [isVerbose, isDebug]) . traceM
 logDebug :: Compiling m e uni fun a => String -> m ()
 logDebug = whenM isDebug . traceM
 
-runCompilerPass :: (Compiling m e uni fun a, b ~ Provenance a) => m (P.Pass m tyname name uni fun b) -> Term tyname name uni fun b -> m (Term tyname name uni fun b)
-runCompilerPass mpasses t = do
+runCompilerPass
+  :: ( Compiling m e uni fun a, b ~ Provenance a
+     , ShowRocq tyname name uni fun a
+     )
+  => (Text -> m ())
+  -> m (P.Pass m tyname name uni fun b)
+  -> Term tyname name uni fun b
+  -> m (Term tyname name uni fun b)
+runCompilerPass dumpCert mpasses t = do
   passes <- mpasses
   pedantic <- view (ccOpts . coPedantic)
-  res <- runExceptT $ P.runPass logVerbose pedantic passes t
+  res <- runExceptT $ P.runPass logVerbose dumpCert pedantic passes t
   throwingEither _Error res
 
 floatOutPasses :: Compiling m e uni fun a => m (P.Pass m TyName Name uni fun (Provenance a))
@@ -181,20 +191,34 @@ dce = do
 -- to dump a "readable" version of pir (i.e. floated).
 compileToReadable
   :: forall m e uni fun a b
-  . (Compiling m e uni fun a, b ~ Provenance a)
-  => Program TyName Name uni fun b
+  . (Compiling m e uni fun a, b ~ Provenance a
+  , PLC.Everywhere uni (ComposeC Show AsRocq)
+  , PLC.GShow (AsRocqUni uni)
+  , Show fun
+  )
+  => (Text -> m ())
+  -> Program TyName Name uni fun b
   -> m (Program TyName Name uni fun b)
-compileToReadable (Program a v t) = do
+compileToReadable dumpCert (Program a v t) = do
   validateOpts v
   let pipeline :: m (P.Pass m TyName Name uni fun b)
       pipeline = ala Ap foldMap [typeCheckTerm, dce, simplifier, floatOutPasses]
-  Program a v <$> runCompilerPass pipeline t
+  Program a v <$> runCompilerPass dumpCert pipeline t
 
 -- | The 2nd half of the PIR compiler pipeline.
 -- Compiles a 'Term' into a PLC Term, by removing/translating step-by-step the PIR's language constructs to PLC.
 -- Note: the result *does* have globally unique names.
-compileReadableToPlc :: forall m e uni fun a b . (Compiling m e uni fun a, b ~ Provenance a) => Program TyName Name uni fun b -> m (PLCProgram uni fun a)
-compileReadableToPlc (Program a v t) = do
+compileReadableToPlc
+  :: forall m e uni fun a b
+  . (Compiling m e uni fun a, b ~ Provenance a
+     , PLC.Everywhere uni (ComposeC Show AsRocq)
+     , PLC.GShow (AsRocqUni uni)
+     , Show fun
+  )
+  => (Text -> m ())
+  -> Program TyName Name uni fun b
+  -> m (PLCProgram uni fun a)
+compileReadableToPlc dumpCert (Program a v t) = do
 
   let
     pipeline :: m (P.Pass m TyName Name uni fun b)
@@ -216,18 +240,23 @@ compileReadableToPlc (Program a v t) = do
         ]
 
     go =
-        runCompilerPass pipeline
+        runCompilerPass dumpCert pipeline
         >=> (<$ logVerbose "  !!! lowerTerm")
         >=> lowerTerm
 
   PLC.Program a v <$> go t
 
 --- | Compile a 'Program' into a PLC Program. Note: the result *does* have globally unique names.
-compileProgram :: Compiling m e uni fun a
-            => Program TyName Name uni fun a -> m (PLCProgram uni fun a)
-compileProgram =
+compileProgram :: ( Compiling m e uni fun a
+  , PLC.Everywhere uni (ComposeC Show AsRocq)
+  , PLC.GShow (AsRocqUni uni)
+  , Show fun
+  )
+            => (Text -> m ()) ->
+            Program TyName Name uni fun a -> m (PLCProgram uni fun a)
+compileProgram dumpCert =
   (pure . original)
   >=> (<$ logDebug "!!! compileToReadable")
-  >=> compileToReadable
+  >=> (compileToReadable dumpCert)
   >=> (<$ logDebug "!!! compileReadableToPlc")
-  >=> compileReadableToPlc
+  >=> (compileReadableToPlc dumpCert)

plutus-core/plutus-ir/src/PlutusIR/Compiler/Let.hs

@@ -41,6 +41,13 @@ Also we should pull out more stuff (e.g. see 'NonStrict' which uses unit).
 data LetKind = RecTerms | NonRecTerms | Types | DataTypes
   deriving stock (Show, Eq, Ord)
 
+kindToPass :: LetKind -> PassId
+kindToPass k = case k of
+  RecTerms    -> PassCompileLetRec
+  NonRecTerms -> PassCompileLetNonRec
+  Types       -> PassCompileLetType
+  DataTypes   -> PassCompileLetData
+
 compileLetsPassSC
   :: Compiling m e uni fun a
   => TC.PirTCConfig uni fun
@@ -57,6 +64,7 @@ compileLetsPass
 compileLetsPass tcconfig letKind =
   NamedPass "compile lets" $
     Pass
+      (kindToPass letKind)
       (compileLets letKind)
       [Typechecks tcconfig, GloballyUniqueNames]
       [ConstCondition (Typechecks tcconfig)]