Desugar constraints from atyp rather than n_constraint

Previously the valid constraints had to be carefully restricted to
avoid parser ambiguities between n_constraint and atyp. With the
initial check refactored, we can now parse constraints into atyp using
ATyp_app for the operators, and changing ATyp_constant into a more
general ATyp_lit for true and false. Logically this new structure is
more uniform, as atyp is now the parse representation for all
Bool-kinded things (constraints), Type-kinded things (regular types),
and Int-kinded things (n-expressions), and initial_check.ml now splits
all three into n_constraint, typ, and nexp respectively, rather than
how it was before with initial_check splitting types and nexps, but
constraints already being separate in the parser.

5 files changed, 90 insertions, 156 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 926e993a..b57e6b17 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -171,7 +171,7 @@ and to_ast_nexp ctx (P.ATyp_aux (aux, l)) =
   let aux = match aux with
     | P.ATyp_id id -> Nexp_id (to_ast_id id)
     | P.ATyp_var v -> Nexp_var (to_ast_var v)
-    | P.ATyp_constant c -> Nexp_constant c
+    | P.ATyp_lit (P.L_aux (P.L_num c, _)) -> Nexp_constant c
     | P.ATyp_sum (t1, t2) -> Nexp_sum (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
     | P.ATyp_exp t1 -> Nexp_exp (to_ast_nexp ctx t1)
     | P.ATyp_neg t1 -> Nexp_neg (to_ast_nexp ctx t1)
@@ -189,26 +189,26 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
   | ATyp_dec -> Ord_aux (Ord_dec, l)
   | _ -> raise (Reporting.err_typ l "Invalid order in type")
 
-and to_ast_constraint ctx (P.NC_aux (nc, l)) =
-  let nc = match nc with
-    | P.NC_equal (t1, t2) ->
-       NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
-    | P.NC_not_equal (t1, t2) ->
-       NC_not_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
-    | P.NC_bounded_ge (t1,t2) ->
-       NC_bounded_ge (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
-    | P.NC_bounded_le(t1,t2) ->
-       NC_bounded_le (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
-    | P.NC_set(id,bounds) ->
-       NC_set(to_ast_var id, bounds)
-    | P.NC_or (nc1, nc2) ->
-       NC_or (to_ast_constraint ctx nc1, to_ast_constraint ctx nc2)
-    | P.NC_and (nc1, nc2) ->
-       NC_and (to_ast_constraint ctx nc1, to_ast_constraint ctx nc2)
-    | P.NC_true -> NC_true
-    | P.NC_false -> NC_false
+and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
+  let aux = match aux with
+    | P.ATyp_app (Id_aux (DeIid op, _), [t1; t2]) ->
+       begin match op with
+       | "==" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
+       | "!=" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
+       | ">=" -> NC_bounded_ge (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
+       | "<=" -> NC_bounded_le (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
+       | ">" -> NC_bounded_ge (to_ast_nexp ctx t1, nsum (to_ast_nexp ctx t2) (nint 1))
+       | "<" -> NC_bounded_le (nsum (to_ast_nexp ctx t1) (nint 1), to_ast_nexp ctx t2)
+       | "&" -> NC_and (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
+       | "|" -> NC_or (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
+       | _ -> raise (Reporting.err_typ l ("Invalid operator in constraint"))
+       end
+    | 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 (id, bounds) -> NC_set (to_ast_var id, bounds)
+    | _ -> raise (Reporting.err_typ l "Invalid constraint")
   in
-  NC_aux (nc, l)
+  NC_aux (aux, l)
 
 let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
   match aux with
diff --git a/src/lexer.mll b/src/lexer.mll
index a1f3ace2..f5a982eb 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -217,7 +217,6 @@ rule token = parse
   | "@"                                 { (At "@") }
   | "2" ws "^"                          { TwoCaret }
   | "^"					{ (Caret(r"^")) }
-  | "::<"                               { ColonColonLt }
   | "::"                                { ColonColon(r "::") }
   (* | "^^"                                { CaretCaret(r "^^") } *)
   | "~~"                                { TildeTilde(r "~~") }
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 79d90635..204389f9 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -122,13 +122,32 @@ kid =
 
 type 
 id = 
-   Id_aux of id_aux * l
+  Id_aux of id_aux * l
+
+type
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of Big_int.num (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* undefined value *)
+ | L_string of string (* string constant *)
+ | L_real of string
+
+type
+lit =
+   L_aux of lit_aux * l
 
 type
 atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
    ATyp_id of id (* identifier *)
  | ATyp_var of kid (* ticked variable *)
- | ATyp_constant of Big_int.num (* constant *)
+ | ATyp_lit of lit (* literal *)
+ | ATyp_nset of kid * (Big_int.num) list (* set type *)
  | ATyp_times of atyp * atyp (* product *)
  | ATyp_sum of atyp * atyp (* sum *)
  | ATyp_minus of atyp * atyp (* subtraction *)
@@ -143,8 +162,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_wild
  | ATyp_tup of (atyp) list (* Tuple type *)
  | ATyp_app of id * (atyp) list (* type constructor application *)
- | ATyp_exist of kid list * n_constraint * atyp
- | ATyp_with of atyp * n_constraint
+ | ATyp_exist of kid list * atyp * atyp
 
 and atyp = 
    ATyp_aux of atyp_aux * l
@@ -155,23 +173,6 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
    KOpt_none of kid (* identifier *)
  | KOpt_kind of kind * kid (* kind-annotated variable *)
 
-
-and 
-n_constraint_aux =  (* constraint over kind $_$ *)
-   NC_equal of atyp * atyp
- | NC_bounded_ge of atyp * atyp
- | NC_bounded_le of atyp * atyp
- | NC_not_equal of atyp * atyp
- | NC_set of kid * (Big_int.num) list
- | NC_or of n_constraint * n_constraint
- | NC_and of n_constraint * n_constraint
- | NC_true
- | NC_false
-
-and
-n_constraint = 
-   NC_aux of n_constraint_aux * l
-
 type 
 kinded_id = 
    KOpt_aux of kinded_id_aux * l
@@ -179,7 +180,7 @@ kinded_id =
 type
 quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
    QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of n_constraint (* A constraint for this type *)
+ | QI_const of atyp (* A constraint for this type *)
 
 
 type 
@@ -197,32 +198,12 @@ type
 typquant = 
    TypQ_aux of typquant_aux * l
 
-
-type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of Big_int.num (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* undefined value *)
- | L_string of string (* string constant *)
- | L_real of string
-
-type 
+type
 typschm_aux =  (* type scheme *)
    TypSchm_ts of typquant * atyp
 
 
 type 
-lit = 
-   L_aux of lit_aux * l
-
-
-type 
 typschm = 
    TypSchm_aux of typschm_aux * l
 
@@ -285,7 +266,7 @@ exp_aux =  (* Expression *)
  | E_let of letbind * exp (* let expression *)
  | E_assign of exp * exp (* imperative assignment *)
  | E_sizeof of atyp
- | E_constraint of n_constraint
+ | E_constraint of atyp
  | E_exit of exp
  | E_throw of exp
  | E_try of exp * pexp list
@@ -302,12 +283,6 @@ and fexp_aux =  (* Field-expression *)
 and fexp = 
    FE_aux of fexp_aux * l
 
-and fexps_aux =  (* Field-expression list *)
-   FES_Fexps of (fexp) list * bool
-
-and fexps = 
-   FES_aux of fexps_aux * l
-
 and opt_default_aux =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
    Def_val_empty
  | Def_val_dec of exp
diff --git a/src/parser.mly b/src/parser.mly
index 73259210..bb5aa5f1 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -103,7 +103,6 @@ let mk_typschm_opt ts n m = TypSchm_opt_aux (
 
 let mk_typschm_opt_none = TypSchm_opt_aux (TypSchm_opt_none, Unknown)
 
-let mk_nc nc n m = NC_aux (nc, loc n m)
 let mk_sd s n m = SD_aux (s, loc n m)
 let mk_sd_doc s str n m = SD_aux (s, Documented (str, loc n m))
 let mk_ir r n m = BF_aux (r, loc n m)
@@ -140,18 +139,18 @@ type lchain =
 | LC_lteq
 | LC_nexp of atyp
 
+let tyop op t1 t2 s e = mk_typ (ATyp_app (Id_aux (DeIid op, loc s e), [t1; t2])) s e
+
 let rec desugar_lchain chain s e =
   match chain with
-  | [LC_nexp n1; LC_lteq; LC_nexp n2] ->
-    mk_nc (NC_bounded_le (n1, n2)) s e
-  | [LC_nexp n1; LC_lt; LC_nexp n2] ->
-    mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e
+  | [LC_nexp n1; LC_lteq; LC_nexp n2] -> tyop "<=" n1 n2 s e
+  | [LC_nexp n1; LC_lt; LC_nexp n2] -> tyop "<" n1 n2 s e
   | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) ->
-    let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in
-    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+     let nc1 = tyop "<=" n1 n2 s e in
+     tyop "&" nc1 (desugar_lchain (LC_nexp n2 :: chain) s e) s e
   | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) ->
-    let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e, n2)) s e in
-    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+     let nc1 = tyop "<" n1 n2 s e in
+     tyop "&" nc1 (desugar_lchain (LC_nexp n2 :: chain) s e) s e
   | _ -> assert false
 
 type rchain =
@@ -161,20 +160,16 @@ type rchain =
 
 let rec desugar_rchain chain s e =
   match chain with
-  | [RC_nexp n1; RC_gteq; RC_nexp n2] ->
-    mk_nc (NC_bounded_ge (n1, n2)) s e
-  | [RC_nexp n1; RC_gt; RC_nexp n2] ->
-    mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e
+  | [RC_nexp n1; RC_gteq; RC_nexp n2] -> tyop ">=" n1 n2 s e
+  | [RC_nexp n1; RC_gt; RC_nexp n2] -> tyop ">" n1 n2 s e
   | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) ->
-    let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in
-    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+     let nc1 = tyop ">=" n1 n2 s e in
+     tyop "&" nc1 (desugar_rchain (RC_nexp n2 :: chain) s e) s e
   | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) ->
-    let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant (Big_int.of_int 1)) s e)) s e)) s e in
-    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+     let nc1 = tyop ">" n1 n2 s e in
+     tyop "&" nc1 (desugar_rchain (RC_nexp n2 :: chain) s e) s e
   | _ -> assert false
 
-let future_syntax l = Util.warn (Reporting.loc_to_string l ^ "\n\nThis syntax is currently experimental")
-
 %}
 
 /*Terminals with no content*/
@@ -189,7 +184,7 @@ let future_syntax l = Util.warn (Reporting.loc_to_string l ^ "\n\nThis syntax is
 %nonassoc Then
 %nonassoc Else
 
-%token Bar Comma Dot Eof Minus Semi Under DotDot ColonColonLt
+%token Bar Comma Dot Eof Minus Semi Under DotDot
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar
 %token MinusGt Bidir LtMinus
 
@@ -324,69 +319,35 @@ kid_list:
   | kid kid_list
     { $1 :: $2 }
 
-nc:
-  | nc Bar nc_and
-    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
-  | nc_and
-    { $1 }
-
-nc_and:
-  | nc_and Amp atomic_nc
-    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
-  | atomic_nc
-    { $1 }
-
-atomic_nc:
-  | True
-    { mk_nc NC_true $startpos $endpos }
-  | False
-    { mk_nc NC_false $startpos $endpos }
-  | typ0 EqEq typ0
-    { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
-  | typ0 ExclEq typ0
-    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
-  | nc_lchain
-    { desugar_lchain $1 $startpos $endpos }
-  | nc_rchain
-    { desugar_rchain $1 $startpos $endpos }
-  | Lparen nc Rparen
-    { $2 }
-  | kid In Lcurly num_list Rcurly
-    { mk_nc (NC_set ($1, $4)) $startpos $endpos }
-
 num_list:
   | Num
     { [$1] }
   | Num Comma num_list
     { $1 :: $3 }
 
-nc_lchain:
-  | typ0 LtEq typ0
+lchain:
+  | typ5 LtEq typ5
     { [LC_nexp $1; LC_lteq; LC_nexp $3] }
-  | typ0 Lt typ0
+  | typ5 Lt typ5
     { [LC_nexp $1; LC_lt; LC_nexp $3] }
-  | typ0 LtEq nc_lchain
+  | typ5 LtEq lchain
     { LC_nexp $1 :: LC_lteq :: $3 }
-  | typ0 Lt nc_lchain
+  | typ5 Lt lchain
     { LC_nexp $1 :: LC_lt :: $3 }
 
-nc_rchain:
-  | typ0 GtEq typ0
+rchain:
+  | typ5 GtEq typ5
     { [RC_nexp $1; RC_gteq; RC_nexp $3] }
-  | typ0 Gt typ0
+  | typ5 Gt typ5
     { [RC_nexp $1; RC_gt; RC_nexp $3] }
-  | typ0 GtEq nc_rchain
+  | typ5 GtEq rchain
     { RC_nexp $1 :: RC_gteq :: $3 }
-  | typ0 Gt nc_rchain
+  | typ5 Gt rchain
     { RC_nexp $1 :: RC_gt :: $3 }
 
 tyarg:
-  | ColonColonLt typ_list Gt
-    { future_syntax (loc $startpos($1) $endpos($3)); $2, [] }
   | Lparen typ_list Rparen
     { [], $2 }
-  | ColonColonLt typ_list Gt Lparen typ_list Rparen
-    { future_syntax (loc $startpos($1) $endpos($3)); $2, $5 }
 
 typ:
   | typ0
@@ -427,6 +388,7 @@ typ2:
   | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ3 Bar typ2r { mk_typ (ATyp_app (deinfix (mk_id (Id "|") $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
   | typ3 { $1 }
 typ2l:
   | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
@@ -435,12 +397,14 @@ typ2l:
 typ2r:
   | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ3 op2r typ2r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ3 Bar typ2r { mk_typ (ATyp_app (deinfix (mk_id (Id "|") $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
   | typ3 { $1 }
 
 typ3:
   | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ4 Amp typ3r { mk_typ (ATyp_app (deinfix (mk_id (Id "&") $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
   | typ4 { $1 }
 typ3l:
   | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
@@ -449,12 +413,17 @@ typ3l:
 typ3r:
   | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ4 op3r typ3r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ4 Amp typ3r { mk_typ (ATyp_app (deinfix (mk_id (Id "&") $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
   | typ4 { $1 }
 
 typ4:
   | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | lchain { desugar_lchain $1 $startpos $endpos }
+  | rchain { desugar_rchain $1 $startpos $endpos }
+  | typ5 EqEq typ5 { mk_typ (ATyp_app (deinfix (mk_id (Id $2) $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
+  | typ5 ExclEq typ5 { mk_typ (ATyp_app (deinfix (mk_id (Id $2) $startpos($2) $endpos($2)), [$1; $3])) $startpos $endpos }
   | typ5 { $1 }
 typ4l:
   | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
@@ -534,6 +503,8 @@ typ8r:
   | typ9 { $1 }
 
 typ9:
+  | kid In Lcurly num_list Rcurly
+    { mk_typ (ATyp_nset ($1, $4)) $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 }
@@ -554,8 +525,8 @@ atomic_typ:
     { mk_typ ATyp_wild $startpos $endpos }
   | kid
     { mk_typ (ATyp_var $1) $startpos $endpos }
-  | Num
-    { mk_typ (ATyp_constant $1) $startpos $endpos }
+  | lit
+    { mk_typ (ATyp_lit $1) $startpos $endpos }
   | Dec
     { mk_typ ATyp_dec $startpos $endpos }
   | Inc
@@ -573,10 +544,10 @@ atomic_typ:
     { let v = mk_kid "n" $startpos $endpos in
       let atom_id = mk_id (Id "atom") $startpos $endpos in
       let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
-      mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+      mk_typ (ATyp_exist ([v], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
   | Lcurly kid_list Dot typ Rcurly
-    { mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
-  | Lcurly kid_list Comma nc 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 kid_list Comma typ Dot typ Rcurly
     { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
 
 typ_list:
@@ -606,7 +577,7 @@ kopt_list:
     { $1 :: $2 }
 
 typquant:
-  | kopt_list Comma nc
+  | kopt_list Comma typ
     { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in
       TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) }
   | kopt_list
@@ -1055,7 +1026,7 @@ atomic_exp:
     { mk_exp (E_exit $3) $startpos $endpos }
   | Sizeof Lparen typ Rparen
     { mk_exp (E_sizeof $3) $startpos $endpos }
-  | Constraint Lparen nc Rparen
+  | Constraint Lparen typ Rparen
     { mk_exp (E_constraint $3) $startpos $endpos }
   | Assert Lparen exp Rparen
     { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos }
@@ -1175,17 +1146,7 @@ param_kopt_list:
     { $1 :: $3 }
 
 typaram:
-  | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen Comma nc
-    { future_syntax (loc $startpos($1) $endpos($3));
-      let qi_nc = QI_aux (QI_const $8, loc $startpos($8) $endpos($8)) in
-      mk_typq ($5 @ $2) [qi_nc] $startpos $endpos }
-  | ColonColonLt param_kopt_list Gt Lparen param_kopt_list Rparen
-    { future_syntax (loc $startpos($1) $endpos($3));
-      mk_typq ($5 @ $2) [] $startpos $endpos }
-  | ColonColonLt param_kopt_list Gt
-    { future_syntax (loc $startpos($1) $endpos($3));
-      mk_typq $2 [] $startpos $endpos }
-  | Lparen param_kopt_list Rparen Comma nc
+  | Lparen param_kopt_list Rparen Comma typ
     { let qi_nc = QI_aux (QI_const $5, loc $startpos($5) $endpos($5)) in
       mk_typq $2 [qi_nc] $startpos $endpos }
   | Lparen param_kopt_list Rparen
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f9908c71..5201744b 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -146,9 +146,8 @@ let doc_nc nc =
        end
     | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs)
   and nc1 (NC_aux (nc_aux, _) as nc) =
-    match nc_aux with
-    | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
-    | _ -> atomic_nc nc
+    let conjs = constraint_conj nc in
+    separate_map (space ^^ string "&" ^^ space) atomic_nc conjs
   in
   atomic_nc (constraint_simp nc)