Allow :searching partially-applied SAW context types

[samcowger]

As in, allow a user to write :search ProofScript at the SAW REPL, rather than requiring them to write :search (ProofScript _) - though the latter is still allowed.

[sauclovian-g]

There are, I'm afraid, some holes in this as it stands; e.g. :search {a} ProofScript a generates a parse error, although :search {a} (ProofScript a) still works. Also, the idea of the list of BaseType in SchemaPattern is that you can do :search Int String, and with these changes, while you can still do :search (ProofScript _) Int String, both :search ProofScript Int String and :search Int String ProofScript fail.

I think the right thing to do is fold Context into BaseType; there's no reason to distinguish them in the parser, and there doesn't seem to be any problem with having sequences of BaseType in AppliedType. This allows one to write uninhabitable types like Int Int but these days the typechecker should cope.

(also, while you're touching this file, could you delete the CryptolSetup keyword on line 67? it is not used and generates a warning)

[sauclovian-g]

Also it might be a good idea to replace the note in the docs about needing (ProofScript _) with one about how :search ProofScript Int will be interpreted as multiple search terms rather than a type application, and to use :search (ProofScript Int) if you want the type application.

[sauclovian-g]

And a third thing (sorry, should have thought of these all at once and sent fewer emails), can you add a CHANGES entry?

[sauclovian-g]

And a fourth: thanks for attending to this, I'd been figuring it was going to require burning out Context from the downstream AST to fix it. That should still get done of course but it's a lot more involved...

[samcowger]

There are, I'm afraid, some holes in this as it stands; e.g. :search {a} ProofScript a generates a parse error, although :search {a} (ProofScript a) still works. Also, the idea of the list of BaseType in SchemaPattern is that you can do :search Int String, and with these changes, while you can still do :search (ProofScript _) Int String, both :search ProofScript Int String and :search Int String ProofScript fail.

I think the right thing to do is fold Context into BaseType; there's no reason to distinguish them in the parser, and there doesn't seem to be any problem with having sequences of BaseType in AppliedType. This allows one to write uninhabitable types like Int Int but these days the typechecker should cope.

I'm pleasantly surprised to see that the parser doesn't complain about that change, so I've made it in d4c37a4. I also added tests in that commit for those now-no-longer-failing cases you discovered - thanks for discovering them!

(also, while you're touching this file, could you delete the CryptolSetup keyword on line 67? it is not used and generates a warning)

Ah, thanks for the reminder, I noticed that as well. I've removed that, as well as one other non-user-facing occurrence of CryptolSetup, in 99412c3.

Also it might be a good idea to replace the note in the docs about needing (ProofScript _) with one about how :search ProofScript Int will be interpreted as multiple search terms rather than a type application, and to use :search (ProofScript Int) if you want the type application.

Good idea, done in 4948104.

And a third thing (sorry, should have thought of these all at once and sent fewer emails), can you add a CHANGES entry?

No problem, done in cc7272d.

[sauclovian-g]

Otherwise LGTM