Add a new syntax to support partial opens and includes

[W95Psp]

Hi!

This PR introduces the following syntaxes:

// brings `MyModule.some_function`, `MyModule.some_type` and `MyModule.SomeConstructor` only, nothing else is visible
open MyModule { some_function, some_type, SomeConstructor }
// `include` works the same
include MyModule { some_function, some_type, SomeConstructor }
// renaming is possible
include MyModule { some_function as f, SomeConstructor as X }

I call { ... } a restriction that we impose on the open or include, maybe there's a better naming there.

This PR:

• tags auto generated records (when type foo = | Foo {...}) with a new attribute desugar_of_variant_record (this is important, so that open Module {foo} is able to look for that attribute and bring foo__Foo__payload in scope too);
• add a type restriction;
• change the parser to allow the new restriction syntax;
• tweaks DsEnv accordingly;
• adds a module _ = Foo syntax (that desugars to open Foo {})

What do you think about this new feature?

@mtzguido, I haven't hacked on F* for a while, and I have to say having typeclasses (and tactics, seems like! 👀) within the compiler sources is fantastic! Especially something as "stupid" as showable simplifies makes debugging much much nicer!

---

More example in tests/restricted_includes, but here is a preview:

Given the following module:

module Definitions

type a_type = 
  | AType1: a1:int -> a2:nat -> a_type
  | AType2 of string
  | AType3 { a_type_C_field1: int
           ; a_type_C_field2: b_type }
and b_type =
  | BType1
  | BType2 of a_type
  | BType3 { b_type_F_field1: int
           ; a_type_F_field2: a_type }

type a_record = { a_record_field1: a_type; a_record_field2: int }

let fn_example x y = x + y

You can:

module Consumer

(**** Opening a type *)
// Importing an inductive `a_type` will implicitely import each data
// constructors and each associated desugared record types (here,
// `a_type` as a constructor `Type3` with a record payload: the
// implicit corresponding record type will be imported).
open Definitions {a_type}

// `a_type` and its constructors are available
let _ = a_type
let _ = AType1 0 1
let _ = AType2 "hi"
let _ = AType3 { a_type_C_field1 = 3
               ; a_type_C_field2 = Definitions.BType1 (* BType1 is not in scope *) }

// The automatically generated type `a_type__AType3__payload` is available as well
let _ = a_type__AType3__payload
let _ = Mka_type__AType3__payload
let _ = { a_type_C_field1 = 3
        ; a_type_C_field2 = Definitions.BType1 (* BType1 is not in scope *) }

// Fields projectors are imported
let _ = (AType1?.a1, AType2?._0, AType3?._0)

// The constructors of `a_type` are imported:
let _ = (AType1, AType2, AType3)

// Fields names are imported correctly
let _ = fun x -> x.a_type_C_field1

// Other definitions are not visible:
[@@expect_failure [72]] let _ = a_record
[@@expect_failure [72]] let _ = fn_example
[@@expect_failure [72]] let _ = b_type
[@@expect_failure [72]] let _ = BType1
[@@expect_failure [72]] let _ = BType2
[@@expect_failure [72]] let _ = BType3

(**** Include works as well *)
// Exactly the same syntax and expressivity works for `include` as
// well.
include Definitions {a_type}

(**** Renaming *)
include Definitions {AType2 as AnotherNicerName}
include Definitions {BType1 as RenamedBType1}
include Definitions {BType2}
include Definitions {fn_example as fn_renamed}

let _: a_type = AnotherNicerName "hello"

(**** Missing names or redundant names *)
// If a include or open exposes missing redundant names, this is an error.
[@@expect_failure [47]] open Definitions {AType2 as AType1, AType1}
[@@expect_failure [47]] open Definitions {AType1, AType1}
[@@expect_failure [47]] open Definitions {a_type, AType1}

(**** Opening a module anonymously *)
// Let's first bring in scope the method `to_int` of the typeclass `to_int_tc`:
open TypeclassDefinition {to_int}

// The module `TypeclassInstance` defines an instance of `to_int_tc`
// for `int`. I can open it without exposing any name into my scope:
open TypeclassInstance {}

// Now, I can use `to_int` on int:
let _ = to_int 3

[mtzguido]

Hi Lucas, this looks great and it's very useful! Thank you!

I left some tiny comments, but other than that I'd be really happy merging this.

[W95Psp]

Thanks for the fast review Guido! I addressed your comments, tell me if there's anything else I can do :)
Otherwise I'd be quite happy to see that merged :D

[mtzguido]

Thanks Lucas! This is great.