Lower precedence of "in" for set constraints

(e.g., for `'n * 8 in {8, 16, 32}`)
rems-project · Jun 7, 2024 · 3d66ddd · 3d66ddd
1 parent 92150fa
commit 3d66ddd
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/src/lib/infix_parser.mly b/src/lib/infix_parser.mly
@@ -150,6 +150,7 @@ typ4r:
   | typ5 { $1 }
 
 typ5:
+  | typ6 In typ6 { mk_typ (ATyp_in ($1, $3)) $startpos $endpos }
   | typ6 Op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ5l Op5l typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ6 Op5r typ5r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
@@ -218,7 +219,6 @@ typ8r:
   | typ9 { $1 }
 
 typ9:
-  | 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/test/typecheck/pass/set_constraint.sail b/test/typecheck/pass/set_constraint.sail
@@ -0,0 +1,10 @@
+default Order dec
+$include <prelude.sail>
+
+val f : forall 'n. int('n) -> int
+
+function f(n) = {
+  assert(constraint('n * 8 in {8, 16, 32}));
+  n
+}
+