Support mutually recursive let bindings in sigelt_view

[antoniolocascio]

Context

The module FStar.Reflection.Data defines the data type sigelt_view, which is used for inspecting the signature of a declaration. As of right now, its definition is:

type sigelt_view =
    | Sg_Let of bool * fv * list<univ_name> * typ * term
    | Sg_Inductive of name * list<univ_name> * list<binder> * typ * list<ctor> 
    | Sg_Val of name * list<univ_name> * typ
    | Unk

The problem is that there’s no way of inspecting mutually recursive let bindings, as the first constructor can only represent a single standalone let. In contrast, the sigelt datatype's Sig_let constructor has a list of let bindings to accommodate mutually recursive lets.

Implemented solution

In this PR I provide a workaround to this, which involves adding a new constructor to sigelt_view to represent mutually recursive lets:

  | Sg_MLet of list<lb_view>

where lb_view is a type that packs the same information as in Sg_Let, and is defined as:

type lb_view = {
    lb_r : bool;
    lb_fv : fv;
    lb_us : list<univ_name>;
    lb_typ : typ;
    lb_def : term;
}

I chose to add a new constructor to make sure this worked without having to fix every use of Sg_Let, but I believe the two could well be unified. This is something I need in the project I'm currently working on, so I would be happy to hear you opinion on this issue and make any changes to its solution.

[antoniolocascio]

Following a discussion with @aseemr and @nikswamy, I've changed the implementation of this PR to generalize Sg_Let. Now, this constructor is defined as:

  | Sg_MLet of bool * list<letbinding>

Where the boolean value flags whether the binding is recursive, and letbinding is the record type defined in Syntax.Syntax.

I also defined the lb_view type, an abstraction that hides the internal representation of let bindings, together with inspection and packing functions.

[antoniolocascio]

Fixed the errors caused by this PR in HACL* in hacl-star#471

[aseemr]

Is this code fixing the unembedding of Sg_val? Was it a bug in the previous code? (Asking only because doesn't seem directly related to the change that this PR is doing.)

[antoniolocascio]

Yes, it's fixing the Sg_Val case. I really can’t remember now, but I'm almost positive it was a bug.

[aseemr]

Do we need to remove these? I am guessing these functions are not used currently but still any harm in keeping them?

[antoniolocascio]

These aren’t removed, they're moved a little earlier in the module (l.625).

[aseemr]

Thanks Antonio! Looks good to me, left a couple of comments.

Since this is a breaking change, can you add an entry to CHANGES.md, summarizing the change, and pointing to a representative example of how to fix the code that breaks? You can see other entries in CHANGES.md for examples.

Thanks again, this is a nice enhancement to the reflection API that would definitely be useful for others too.

[antoniolocascio]

Hi @aseemr, thank you so much for the review. I've updated the CHANGES.md file.