diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 10bb891b5..5d212de7b 100644 --- a/src/bin/sail.ml +++ b/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 -> diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 4ad44db23..6c0771958 100644 --- a/src/lib/chunk_ast.ml +++ b/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 diff --git a/src/lib/infix_parser.mly b/src/lib/infix_parser.mly index 2586fb1d8..a58cacf1a 100644 --- a/src/lib/infix_parser.mly +++ b/src/lib/infix_parser.mly @@ -63,9 +63,8 @@ let rec desugar_rchain chain s e = %token Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l %token 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 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 } diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index 1f51015f2..3a8744181 100644 --- a/src/lib/initial_check.ml +++ b/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) diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index dff6d5d2d..9f9e90935 100644 --- a/src/lib/parse_ast.ml +++ b/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 *) diff --git a/src/lib/parser.mly b/src/lib/parser.mly index e72b0e604..5b05b4c66 100644 --- a/src/lib/parser.mly +++ b/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 diff --git a/test/format/default/set_syntax.expect b/test/format/default/set_syntax.expect new file mode 100644 index 000000000..1511e4a7c --- /dev/null +++ b/test/format/default/set_syntax.expect @@ -0,0 +1,9 @@ +default Order dec + +$include + +val main : unit -> unit + +function main () = { + let x : {1, 2, 3} = 3 +} diff --git a/test/format/set_syntax.sail b/test/format/set_syntax.sail new file mode 100644 index 000000000..4c53f43e5 --- /dev/null +++ b/test/format/set_syntax.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + +val main : unit -> unit + +function main() = { + let x: {|1, 2, 3|} = 3; +} diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect index cca7a8560..681838656 100644 --- a/test/typecheck/pass/existential_ast/v1.expect +++ b/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)) diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect index 3b5651eb5..03ca7656d 100644 --- a/test/typecheck/pass/existential_ast/v2.expect +++ b/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)) diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index b823b8d4d..fa841208c 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/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)) diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index 85f3c4962..50cc6186d 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/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) diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 7e4f1781b..1971afdaf 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/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) diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect index c37ec784b..9326e71e3 100644 --- a/test/typecheck/pass/global_type_var/v3.expect +++ b/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