Implicit PrettyPrinter and CommandLineState arguments

[roboguy13]

Most of the commands that take a PrettyPrinter argument actually take that argument implicitly (that is, this argument is not provided by the end-user). For example, the type of ruleToLemma :: PrettyPrinter -> RuleName -> Transform LCore Doc indicates that it takes a PrettyPrinter, but if we look at the HERMIT help:

rule-to-lemma :: RuleName -> TransformLCoreDocH                             []
  Create a lemma from a GHC RULE.

I believe the only exception to this is dump-lemma (which does take a PrettyPrinter from the user). We should remove these PrettyPrinter arguments on the client-side and figure out how to correctly handle them on the server-side.

It looks like CommandLineState is the same way. possible-rewrites is an example of that. I'm not sure any other commands use CommandLineState, actually.

[ecaustin]

So this relates to the conversation we were having the other day about using HERMIT pretty-printers to debug things.

Remember the liftPrettyH function I pointed out to you? Its abbreviated type is Transform PrettyC HermitM a b -> Transform HermitC HermitM a b, meaning it lifts a transformation that uses a pretty-printer context to be a transformation that uses a HERMIT context.

In order to do this, liftPrettyH needs access to a PrettyOptions value, either using the Default value (which is what I did to debug things) or a value extracted from a pretty-printer using the pOptions field accessor. This is why ruleToLemma needs access to a PrettyPrinter value.

Now the reason we don't actually have to provide one is because the current PrettyPrinter is carried by the shell state. The method provideState from the interpreter should automatically handle things for us as long as the externals we define have PrettyPrinter as the first argument. i.e. they must be of type PrettyPrinter -> a.

The same thing goes for commands that rely on the CommandLineState.

I'm going to go ahead and close this issue for now, but feel free to reopen it if things are not acting as they should.

[ecaustin]

On second thought, I'm going to reopen the issue until we actually test to make sure these commands work.

@andygill, how does the new shell interact with provideState? Will it provide a value for a PrettyPrinter from its state before it tries to retrieve arguments from the transmitted JSON values, or does it do things the other way around?

[ecaustin]

After some limited testing and code review, I think I've concluded that our shell lacks an analogue to the provideState function.

I'm not sure what the best way to solve this problem is. If I understand things correctly, the shell state, including the current pretty-printer, is stored server-side so that it can be modified by effects such as setPP. I assume that means we want to retrieve the pretty-printer value after transmitting the ruleToLemma command.

How do we do this? Do we want to make a new version of ruleToLemma that is a monadic shell effect instead of a transformation?

[roboguy13]

One thing about this that confuses me a bit is whether or not we should expose PrettyPrinter at all (even opaquely) on the client-side. I could have sworn I saw something that takes an actual, explicit PrettyPrinter argument, but now can't find it... Maybe I was just seeing things. @andygill I think that you said you had a particular plan about how you want this aspect of the system to work. What do you think?

Maybe the command I saw was just set-pp, although that takes a String that is interpreted as the name of a pretty printer (which is not really how we should do it in hermit-shell).

[xich]

Evan's summary of PrettyPrinter/CommandLineState arguments above is accurate. When they are the first argument, they get treated specially by the interpreter, and the current pretty printer or state is provided implicitly. This allows rewrites to have access to state without altering the "pure" type signature of the external, meaning they can be composed with other rewrites/etc.

However, when they are not the first argument, then they must be supplied. The only example I can think of are the dump commands, though set-pp should also work that way. It still takes a String because that allowed me to give a better error message, if I remember correctly. The idea of exposing the pretty printers themselves as externals occurred to me fairly recently, so it hasn't been propagated through all the various externals it could probably apply to.

For your purposes, I would assume that the client side would have some command fooC :: a -> Rewrite b that would correspond to either fooS :: PrettyPrinter -> a -> Rewrite b or fooS2 :: MonadReader PrettyPrinter m => a -> m (Rewrite b) on the server. Thus the client only has to provide and serialize a, and the PrettyPrinter would be supplied by the server.

An (untried thus far) alternative might be to give reader access to the shell/pp state in the HermitM monad. To do this without inducing a dependency on the shell would require an extra type parameter to HermitM and likely Kernel, which would be pretty pervasive (and is why I didn't try it).

[ecaustin]

So after a bit more talking with Andy, I think we're going to use this as a motivating example for binding return values from the server in the client. I think a fairly minor change to ShellEffect to give it kind * -> * will allow us add a constructor like CLSGet :: FromJSON a => CLT IO a -> ShellEffect a.

This will let us retrieve the server's PrettyPrinter on the client side and is a good first step towards the more general notion of the Return constructor we will likely eventually want.

I have yet to see if this will have a major impact anywhere beyond the performShellEffect method, so if anyone has any insights on that I'm all ears.

[ecaustin]

I've added a getPP command to hermit-shell which will retrieve the PrettyPrinter value from the server.

Eventually we will want to move PrettyPrinter information client-side, but for now this is a decent enough work around to close this ticket.