FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Resugaring for dependent tuples #3316

Closed mtzguido closed 2 weeks ago

mtzguido commented 3 weeks ago

This PR introduces resugaring for dependent tuples (we had none, except for printing out dtupleN explicitly) and fixes some other problems with resugaring of tuples. See this snippet:

(* Basic dtuple3 *)
let _ = (a:int & b:int & z:int{z == a+b})

(* tuple3 and nested tuple2: all printed the same *)
let _ = int & int & int
let _ = ((int & int) & int)
let _ = (int & (int & int))

(* printed as int * bool *)
let _ = tuple4 int bool

Before (output with --dump_module):

Exports: [
private
let _ =
  FStar.Pervasives.dtuple3 Prims.int (fun _ -> Prims.int) (fun a b -> z: Prims.int{z == a + b})
private
let _ = Prims.int * Prims.int * Prims.int
private
let _ = Prims.int * Prims.int * Prims.int
private
let _ = Prims.int * Prims.int * Prims.int
private
let _ = Prims.int * Prims.bool
]

After:

Exports: [
private
let _ = a: Prims.int & b: Prims.int & z: Prims.int{z == a + b}
private
let _ = Prims.int & Prims.int & Prims.int
private
let _ = (Prims.int & Prims.int) & Prims.int
private
let _ = Prims.int & (Prims.int & Prims.int)
private
let _ = FStar.Pervasives.Native.tuple4 Prims.int Prims.bool
]

Also: Fixes #2245

mtzguido commented 3 weeks ago

This PR will also print out tuples using & instead of *. I propose we switch to & for all tuples consistently.