FStar icon indicating copy to clipboard operation
FStar copied to clipboard

`*` and `&` don't coincide

Open mtzguido opened this issue 1 year ago • 1 comments

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

  1. The pretty printer is being very misleading with nested tuples and we should definitely fix that.
  2. Looks like & only "composes" with itself and not with * to make larger tuples. Maybe that's ok.

mtzguido avatar Dec 08 '23 22:12 mtzguido

This reminds me of #2245, I don't know if it is related.

TWal avatar Dec 09 '23 09:12 TWal

I propose we start deprecating * in favor of &. See also this PR which made the switch in the printer: #3316

mtzguido avatar Jun 14 '24 23:06 mtzguido

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.

mtzguido avatar Jun 17 '24 16:06 mtzguido