FStar
FStar copied to clipboard
`*` and `&` don't coincide
module ProdAssoc
let t1 = int * int * int
let t2 = int * int & int
let t3 = int & int * int
let t4 = int & int & int
--dump_module shows...
Module after type checking:
module ProdAssoc
Declarations: [
let t1 = Prims.int * Prims.int * Prims.int
let t2 = Prims.int * Prims.int * Prims.int
let t3 = Prims.int * Prims.int * Prims.int
let t4 = Prims.int * Prims.int * Prims.int
]
Exports: [
let t1 = Prims.int * Prims.int * Prims.int
let t2 = Prims.int * Prims.int * Prims.int
let t3 = Prims.int * Prims.int * Prims.int
let t4 = Prims.int * Prims.int * Prims.int
]
but! with --ugly we see
Module after type checking:
module ProdAssoc
Declarations: [
[@ ]
visible let t1 : Type = (tuple3 int int int)
[@ ]
visible let t2 : Type = (tuple2 (tuple2 int int) int)
[@ ]
visible let t3 : Type = (tuple2 int (tuple2 int int))
[@ ]
visible let t4 : Type = (tuple3 int int int)
]
Exports: [
[@ ]
visible let t1 : Type = (tuple3 int int int)
[@ ]
visible let t2 : Type = (tuple2 (tuple2 int int) int)
[@ ]
visible let t3 : Type = (tuple2 int (tuple2 int int))
[@ ]
visible let t4 : Type = (tuple3 int int int)
]
Verified module: ProdAssoc
All verification conditions discharged successfully
So
- The pretty printer is being very misleading with nested tuples and we should definitely fix that.
- Looks like
&only "composes" with itself and not with*to make larger tuples. Maybe that's ok.
This reminds me of #2245, I don't know if it is related.
I propose we start deprecating * in favor of &. See also this PR which made the switch in the printer: #3316
The resugaring confusion is now fixed by the PR above. As for & and * having different precedence levels, I think that is fine as-is. Regardless we should move to using & uniformly for tuples (more PRs incoming).
Closing.