Fix formatting for set types

Also simplify the grammar so `in` is treated as a regular binary
operator, and {|1, 2, 3|} and {1, 2, 3} are treated the same

src/bin/sail.ml

@@ -332,7 +332,7 @@ let run_sail_format (config : Yojson.Basic.t option) =
     (fun (f, (comments, parse_ast)) ->
       let source = file_to_string f in
       if is_format_file f && not (is_skipped_file f) then (
-        let formatted = Formatter.format_defs f source comments parse_ast in
+        let formatted = Formatter.format_defs ~debug:true f source comments parse_ast in
         begin
           match !opt_format_backup with
           | Some suffix ->

src/lib/chunk_ast.ml

@@ -545,7 +545,6 @@ let chunk_infix_token comments chunk_primary (infix_token, _, _) =
       | Id_aux (Id "negate", _) -> Infix_prefix "-"
       | _ -> Infix_prefix (string_of_id id)
     )
-  | IT_in_set set -> Infix_op ("in {" ^ Util.string_of_list ", " Big_int.to_string set ^ "}")
   | IT_primary exp ->
       let chunks = Queue.create () in
       chunk_primary comments chunks exp;
@@ -563,10 +562,10 @@ let rec chunk_atyp comments chunks (ATyp_aux (aux, l)) =
   | ATyp_id id -> Queue.add (Atom (string_of_id id)) chunks
   | ATyp_var v -> Queue.add (Atom (string_of_var v)) chunks
   | ATyp_lit lit -> Queue.add (chunk_of_lit lit) chunks
-  | ATyp_nset (n, set) ->
-      let lhs_chunks = rec_chunk_atyp n in
-      let rhs_chunks = Queue.create () in
-      Queue.add (Atom ("{" ^ Util.string_of_list ", " Big_int.to_string set ^ "}")) rhs_chunks;
+  | ATyp_nset set -> Queue.add (Atom ("{" ^ Util.string_of_list ", " Big_int.to_string set ^ "}")) chunks
+  | ATyp_in (lhs, rhs) ->
+      let lhs_chunks = rec_chunk_atyp lhs in
+      let rhs_chunks = rec_chunk_atyp rhs in
       Queue.add (Binary (lhs_chunks, "in", rhs_chunks)) chunks
   | ATyp_infix [(IT_primary lhs, _, _); (IT_op (Id_aux (Id op, _)), _, _); (IT_primary rhs, _, _)] ->
       let lhs_chunks = rec_chunk_atyp lhs in

src/lib/infix_parser.mly

@@ -63,9 +63,8 @@ let rec desugar_rchain chain s e =
 %token <Parse_ast.id> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
 %token <Parse_ast.id> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
-%token Lt Gt LtEq GtEq Minus Star Plus ColonColon At
+%token Lt Gt LtEq GtEq Minus Star Plus ColonColon At In
 %token TwoCaret
-%token <Nat_big_num.num list> InSet
 
 %start typ_eof
 %start exp_eof
@@ -219,8 +218,7 @@ typ8r:
   | typ9 { $1 }
 
 typ9:
-  | atomic_typ InSet
-    { mk_typ (ATyp_nset ($1, $2)) $startpos $endpos }
+  | atomic_typ In atomic_typ { mk_typ (ATyp_in ($1, $3)) $startpos $endpos }
   | atomic_typ Op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ9l Op9l atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | atomic_typ Op9r typ9r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }

src/lib/initial_check.ml

@@ -222,7 +222,6 @@ let parse_infix :
       (List.map
          (function
            | P.IT_primary x, s, e -> (mk_primary x, s, e)
-           | P.IT_in_set nums, s, e -> (InSet nums, s, e)
            | P.IT_prefix id, s, e -> (
                match id with
                | Id_aux (Id "pow2", _) -> (TwoCaret, s, e)
@@ -241,6 +240,7 @@ let parse_infix :
                | Id_aux (Id ">=", _) -> (GtEq, s, e)
                | Id_aux (Id "::", _) -> (ColonColon, s, e)
                | Id_aux (Id "@", _) -> (At, s, e)
+               | Id_aux (Id "in", _) -> (In, s, e)
                | _ -> (
                    match Bindings.find_opt (to_ast_id ctx id) ctx.fixities with
                    | Some (prec, level) -> (to_infix_parser_op (prec, level, id), s, e)
@@ -333,6 +333,9 @@ let rec to_ast_typ ctx atyp =
       in
       Typ_aux (Typ_fn (from_typs, to_ast_typ ctx to_typ), l)
   | P.ATyp_bidir (typ1, typ2, _) -> Typ_aux (Typ_bidir (to_ast_typ ctx typ1, to_ast_typ ctx typ2), l)
+  | P.ATyp_nset nums ->
+      let n = Kid_aux (Var "'n", gen_loc l) in
+      Typ_aux (Typ_exist ([mk_kopt ~loc:l K_int n], nc_set n nums, atom_typ (nvar n)), l)
   | P.ATyp_tuple typs -> Typ_aux (Typ_tuple (List.map (to_ast_typ ctx) typs), l)
   | P.ATyp_app (P.Id_aux (P.Id "int", il), [n]) ->
       Typ_aux (Typ_app (Id_aux (Id "atom", il), [to_ast_typ_arg ctx n K_int]), l)
@@ -474,7 +477,7 @@ and to_ast_constraint ctx atyp =
         | P.ATyp_var v -> NC_var (to_ast_var v)
         | P.ATyp_lit (P.L_aux (P.L_true, _)) -> NC_true
         | P.ATyp_lit (P.L_aux (P.L_false, _)) -> NC_false
-        | P.ATyp_nset (P.ATyp_aux (P.ATyp_var v, _), bounds) -> NC_set (to_ast_var v, bounds)
+        | P.ATyp_in (P.ATyp_aux (P.ATyp_var v, _), P.ATyp_aux (P.ATyp_nset bounds, _)) -> NC_set (to_ast_var v, bounds)
         | _ -> raise (Reporting.err_typ l "Invalid constraint")
       in
       NC_aux (aux, l)

src/lib/parse_ast.ml

@@ -125,7 +125,7 @@ type kid = Kid_aux of kid_aux * l
 
 type id = Id_aux of id_aux * l
 
-type 'a infix_token = IT_primary of 'a | IT_op of id | IT_prefix of id | IT_in_set of Big_int.num list
+type 'a infix_token = IT_primary of 'a | IT_op of id | IT_prefix of id
 
 type lit_aux =
   | (* Literal constant *)
@@ -148,7 +148,8 @@ type atyp_aux =
   | ATyp_id of id (* identifier *)
   | ATyp_var of kid (* ticked variable *)
   | ATyp_lit of lit (* literal *)
-  | ATyp_nset of atyp * Big_int.num list (* set type *)
+  | ATyp_nset of Big_int.num list (* set type *)
+  | ATyp_in of atyp * atyp (* set type *)
   | ATyp_times of atyp * atyp (* product *)
   | ATyp_sum of atyp * atyp (* sum *)
   | ATyp_minus of atyp * atyp (* subtraction *)

src/lib/parser.mly

@@ -240,6 +240,9 @@ let cast_deprecated l =
 let warn_extern_effect l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either monadic or pure"
 
+let set_syntax_deprecated l =
+  Reporting.warn ~once_from:__POS__ "Deprecated" l "Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}."
+  
 %}
 
 /*Terminals with no content*/
@@ -308,6 +311,8 @@ op_no_caret:
     { mk_id (Id "|") $startpos $endpos }
   | Star
     { mk_id (Id "*") $startpos $endpos }
+  | In
+    { mk_id (Id "in") $startpos $endpos }
 
 op:
   | OpId
@@ -320,6 +325,8 @@ op:
     { mk_id (Id "^") $startpos $endpos }
   | Star
     { mk_id (Id "*") $startpos $endpos }
+  | In
+    { mk_id (Id "in") $startpos $endpos }
 
 exp_op:
   | OpId
@@ -379,14 +386,9 @@ typ_eof:
   | Star
     { [(IT_prefix (mk_id (Id "__deref") $startpos $endpos), $startpos, $endpos)] }
 
-num_set:
-  | Lcurly; xs = num_list; Rcurly { xs } 
-
 postfix_typ:
   | t = atomic_typ
     { [(IT_primary t, $startpos, $endpos)] }
-  | t = atomic_typ; i = In; xs = num_set
-    { [(IT_primary t, $startpos(t), $endpos(t)); (IT_in_set xs, $startpos(i), $endpos)] }
 
 /* When we parse a type from a pattern, we can't parse a ^ immediately because that's used for string append patterns */
 typ_no_caret:
@@ -430,12 +432,11 @@ atomic_typ:
     { mk_typ (ATyp_parens $2) $startpos $endpos }
   | Lparen typ Comma typ_list Rparen
     { mk_typ (ATyp_tuple ($2 :: $4)) $startpos $endpos }
+  | Lcurly num_list Rcurly
+    { mk_typ (ATyp_nset $2) $startpos $endpos }
   | LcurlyBar num_list RcurlyBar
-    { let v = mk_typ (ATyp_var (mk_kid "n" $startpos $endpos)) $startpos $endpos in
-      let atom_id = mk_id (Id "atom") $startpos $endpos in
-      let atom_of_v = mk_typ (ATyp_app (atom_id, [v])) $startpos $endpos in
-      let kopt = mk_kopt (KOpt_kind (None, [mk_kid "n" $startpos $endpos], None)) $startpos $endpos in
-      mk_typ (ATyp_exist ([kopt], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+    { set_syntax_deprecated (loc $startpos $endpos);
+      mk_typ (ATyp_nset $2) $startpos $endpos }
   | Lcurly kopt_list Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, ATyp_aux (ATyp_lit (L_aux (L_true, loc $startpos $endpos)), loc $startpos $endpos), $4)) $startpos $endpos }
   | Lcurly kopt_list Comma typ Dot typ Rcurly

test/format/default/set_syntax.expect

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+val main : unit -> unit
+
+function main () = {
+    let x : {1, 2, 3} = 3
+}

test/format/set_syntax.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+val main : unit -> unit
+
+function main() = {
+    let x: {|1, 2, 3|} = 3;
+}

test/typecheck/pass/existential_ast/v1.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/existential_ast/v1.sail:17.10-20:
+17 |  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+   |          ^--------^
+   | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/existential_ast/v1.sail:46.7-21:
 46 |  Some(Ctor2(y, x, c))

test/typecheck/pass/existential_ast/v2.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/existential_ast/v2.sail:17.10-20:
+17 |  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+   |          ^--------^
+   | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/existential_ast/v2.sail:39.7-21:
 39 |  Some(Ctor2(y, x, c))

test/typecheck/pass/existential_ast/v3.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/existential_ast/v3.sail:17.10-20:
+17 |  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+   |          ^--------^
+   | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/existential_ast/v3.sail:26.7-21:
 26 |  Some(Ctor1(a, x, c))

test/typecheck/pass/global_type_var/v1.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/global_type_var/v1.sail:3.22-32:
+3 |let (size as 'size) : {|32, 64|} = 32
+  |                      ^--------^
+  | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/global_type_var/v1.sail:21.13-15:
 21 |let _ = test(32)

test/typecheck/pass/global_type_var/v2.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/global_type_var/v2.sail:3.22-32:
+3 |let (size as 'size) : {|32, 64|} = 32
+  |                      ^--------^
+  | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/global_type_var/v2.sail:21.13-15:
 21 |let _ = test(64)

test/typecheck/pass/global_type_var/v3.expect

@@ -1,3 +1,9 @@
+Warning: Deprecated pass/global_type_var/v3.sail:3.22-32:
+3 |let (size as 'size) : {|32, 64|} = 32
+  |                      ^--------^
+  | 
+Old set syntax, {|1, 2, 3|} can now be written as {1, 2, 3}.
+
 Type error:
 pass/global_type_var/v3.sail:13.23-27:
 13 |    let y : atom(64) = size in