Expose term parsing in tactics via `string_to_term`

[W95Psp]

Hello,

Here is a PR that brings term parsing to tactics, via a primitive string_to_term, that takes a string and an environement. I hope to write a sort of REPL within tactics, so that one can interactively conduct a proof, and having string_to_term is a requirement in this scenario.

Also, I wrote a few tests, and hit some existing issues (#2245, #1865, #2186) with prettyprinting.

[nikswamy]

Hi Lucas,

Thanks for this ... it looks good. But, I'm wondering what your use case is for this. E.g., why would you not write

let test : term = `(fun x -> x)

Which has the advantage of checking that the quoted term is well-scoped etc.

[W95Psp]

Hi Nik,

Yes, maybe my use case is too specific for this to be added in F*.

I'm using this in order to get a "poor man's interactive proving environment".

Basically, using launch_process I open a sort of a REPL, that reads terms as strings, parses them (using string_to_term), unquote them, and run them as tactics.

I had no much time to play with that idea, but here is a screencast of the thing:

https://user-images.githubusercontent.com/593204/112880666-044f5180-90cb-11eb-9f3f-f6275fbc272c.mp4

This would actually maybe make more sense to write such a REPL tactic directly as a native tactic rather than exposing string_to_term though.

[nikswamy]

That's cool!

And in the general spirit of exposing compiler components to meta programs, exposing this interface to the parser seems like a good idea.

We should merge this.

@aseemr @R1kM : You had some remarks about failure handling, but I forget what exactly you had in mind. Can you elaborate, please?

[aseemr]

This looks good to me as well!

[R1kM]

My concerns were about reporting errors if, for instance, you print a term inside F* with some options enabled (--ugly, --print_universes for instance) and try to parse it again using string_to_term. That is, ensuring that string_to_term and term_to_string are inverses seems impossible.

In the proposed approach, I don't think this is a problem, a wrong term would be caught by the F* parser anyway. Following Monday's discussion, I agree that exposing this string_to_term is in the Meta-F* spirit of exposing compiler features without modifying them, and it'd be a nice addition to the current tactics library.

Also, the REPL demo looks super cool!

[W95Psp]

Hi, I totally forgot about that PR. I've reworked it so that it passes the CI. I also added a push_bv_dsenv to allow parsing and desugaring with given identifiers in scope. The helper string_to_term_with_lb ease parsing a string with additional identifiers bindings.

[nikswamy]

Thanks!