Add flag to dump PIR ASTs for certifier

[basetunnel]

Context

For my certifier in Coq, I need to get my hands on all intermediate PIR ASTs. I've added a plugin flag dump-cert-trace, that dumps all PIR ASTs to a single text file during a compilation.

Dumping to file

To prevent keeping all intermediate ASTs in memory, I'm dumping ASTs directly after a pass has run (rather than collecting a pure list of ASTs and dumping them at the end of the pipeline). To that end, I've added a parameter dumpCert :: Text -> m () to runPass (in the pass abstraction), which can be used to append text to the dump file. It needs to be of type Text -> m () rather than Text -> IO (), since the monad stack m does not necessarily have IO in it (the pass abstraction does not require it). The concrete monad stack in Compiler.hs does have IO, so it can be lifted into m.

As a consequence, this new argument also shows up in functions like PIR.compileProgram, PIR.compileToReadable, PIR.compileReadableToPlc. This feels very clumsy, but I couldn't find a nice way to do it. Here are two ideas:

• The dump function could go in CompilationCtx as a Text -> IO (), but that requires a MonadIO constraint in Compiling type and the runPass function in order to actually run it. I'm not sure if that is desired.
• Similar to how logging works (which uses traceM), use unsafePerformIO and add a "pure" function Monad m => Text -> m () in the CompilationCtx

Any other suggestions?

Pretty printing ASTs

The dumping format is textual, and easily parseable in the proof assistant. It's almost Show, but without record syntax and uses Text instead of String for performance. I've added a new typeclass SimpleShow in module Text.SimpleShow, which has some basic instances and the possibility for deriving using GHC generics. I've also written/derived instances for all PIR AST types.

I've added the SimpleShow constraints to the Compiling type/constraint synonym, this required me turning on the following extensions in some places:

• QuantifiedConstraints (because of the constraint forall t. SimpleShow (uni t))
• ImpredicativeTypes, to add the constraint forall t. SimpleShow (uni t) to the Compiling type synonym.

Pretty printing pass information

In addition to ASTs I'm also dumping information about which pass was run. Here I've added the PassId type, which is used as an additional field for every basic Pass constructor.

[basetunnel]

Thanks @effectfully , I think it's a good idea and I've tried it out. Types that needed a custom Show instances are : Unique, Name, TyName, VarDecl and TyVarDecl.

A different problem I'm running into is that the Show instance for Text is not exactly suitable for my purposes in Coq, which parses string literals in a different way (e.g. \ is not treated in a special way). So I'd prefer to produce a custom format that basically prints the UTF-8 byte sequence. For other parts of the AST I'd just reuse Show instances. Do you have any recommendations on how to do this?

[effectfully]

A different problem I'm running into is that the Show instance for Text is not exactly suitable for my purposes in Coq, which parses string literals in a different way (e.g. \ is not treated in a special way). So I'd prefer to produce a custom format that basically prints the UTF-8 byte sequence. For other parts of the AST I'd just reuse Show instances. Do you have any recommendations on how to do this?

Well, that does sound like custom pretty-printing then, given that we can't change the Show instance of Text. So given that you wouldn't really benefit from prettyprinter-configurable, you can do something like this:

newtype AsCoq a = AsCoq a
newtype AsCoq1 f a = AsCoq1 (f a)

deriving newtype instance Show (AsCoq Integer)
instance Show (AsCoq Text) where <...>

instance Show (AsCoq (Term Name DefaultUni DefaultFun ann)) where
    showsPrec pr (AsCoq term) = showsPrec (coerce term :: Term Name (AsCoq1 DefaultUni) DefaultFun ann)

deriving anyclass instance Pretty (AsCoq (Term Name DefaultUni DefaultFun ann)) 

Hm, except propagating AsCoq1 in there looks complicated... OK, I'll take a look.

[effectfully]

You can take the code from #6815 or fix the Show instances at the bottom of UntypedPlutusCore.Core.Instance.CoqShow and we'll merge my PR first and then yours.

It's pretty horrible, but you don't need to understand it, just fix the straightforward instances at the bottom.

An example using the custom Text instance:

example :: Term Name DefaultUni DefaultFun ()
example = Constant () (Some (ValueOf DefaultUniString (Text.pack "abc\n")))

-- >>> showAsCoq example
-- "Constant () (Some (ValueOf DefaultUniString abc\n))"

vs

-- >>> show example
-- "Constant () (Some (ValueOf DefaultUniString \"abc\\n\"))"

[effectfully]

Damn I implemented UPLC instead of PIR. Anyway, adding support for PIR should be a matter of adding a few straightforward instances. I'll do it tomorrow.

[basetunnel]

Thanks, that's quite an interesting technique! It's the first time I see how the flexibility of Term's type parameters can be useful. I'll use the code and adapt it to PIR and what I need for Text.

[effectfully]

It's the first time I see how the flexibility of Term's type parameters can be useful.

The fun parameter is very useful for tests and costing calibrations and I believe it was totally worth introducing it, but arguably the uni parameter doesn't have a high utility-to-cost ratio.

I'll use the code and adapt it to PIR

You can just move the CoqShow module it to PIR without keeping it on the UPLC side, since I assume we aren't exporting UPLC into Coq quite yet. Please do keep the mapUni functions in UPLC and TPLC though, these can be useful for others things.

[bezirg]

Any other suggestions?

Maybe you can reuse the MonadWriter CoverageIndex, changing it to MonadWriter (CertTrace,CoverageIndex)?

Another possibility is to pass around the dumpCert function as an ImplicitParam.