An option to print the source AST using deriving yojson, show

[nikswamy]

@raulraja et al. requested an option to print the parser AST in full detail.

This PR provides two options:

• --print_ast: Which takes a module/namespace selector for the names of the modules whose AST is to be printed

• --print_ast_format [JSON | Show | Internal ]: Which selects one of three formats in which to print the AST, with Internal an ad hoc internal format as the default. The JSON and Show formats are determined by the ppxderiving options for deriving Yojson and Show-based printers

For example, you can write fstar.exe --print_ast_format JSON --print_ast +Unit1 Unit1.Basic.fst to print the AST of all files in the Unit1 namespace.

By default, the printers produced by deriving Yojson and Show are extremely verbose. They print the entire AST, including all the metadata at each node, like the range information on terms and at every identifier.

So, the main code change in this PR is to refactor the Parser.AST and FStar.Ident.ident and lident types to make it possible to easily omit some of the fields in printing.

The general recipe here is that if you have a type

type t = { f:tf; g:tg }

and you only want to print the f:tf,
abstract the type a bit to

type t0 'a = {f:'a; g:tg}
[@@PpxDervingYoJson; PpxDerivingShow]
type t = t0 tf

and define

let t0_to_yojson f x = f x.f
let pp_t0 f fmt x = f fmt x.t

This, in a generic way, matches the signatures expected by the deriving packages for YoJson and Show and allows one to print just the fields of interest.

I used this recipe on the following types:

• FStar.Parser.AST.term, pat, binder, etc (to hide the range and level information from the printer)
• FStar.Ident.ident (to hide the range)
• FStar.Ident.lident (to only print the dot-separated string, not the other fields)

The changes to FStar.Ident are localized and make no difference in the interface.

The changes to FStar.Parser.AST do impact several frontend modules, so most of the code change is related to that. Arguably, the change is an improvement, since it factors a lot of the duplication around ranges etc. into a single type, rather than inserting them in several types in the AST (e.g., prange for patters, brange for binders etc.)

[raulraja]

Thank you so much for taking the time to implement this, @nikswamy. This has helped us a lot understanding the structure of F* programs 🙏

[W95Psp]

As we just discussed:
The OCaml library ppx_yojson_conv from Janestreet allows marking fields as opaque, but that would require translating F* attributes (or some attributes) to OCaml. (I think it's not the case currently, right? PpxDerivingYoJson and friends are special cases?)

Anyway, I think F* doesn't use ppx_yojson_conv but ppx_deriving_yojson, which indeed seems to lack a mechanism to hide some fields for serialization :(

Though, quoting the readme of ppx_deriving_yojson, it seems like ppx_yojson_conv is the recommended PPX to deal with JSON (de)serialization derivation.

Note: ppx_yojson_conv is a more recent deriving extension for Yojson that uses a more durable technical foundation and is more actively maintained. We keep maintaining ppx_deriving_yojson for our existing users, but we would recommend that new projects start from ppx_yojson_conv instead.

[R1kM]

Note, while ppx_deriving_yojson does not have this opaque feature, it should be possible to emulate it using the override of default derivations.
For instance, by annotating a field with @to_yojson Fun.const (`String "<opaque>")]