diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml
index 98c4ebaab..f309c0b04 100644
--- a/src/lib/chunk_ast.ml
+++ b/src/lib/chunk_ast.ml
@@ -92,7 +92,9 @@ let binder_keyword = function Var_binder -> "var" | Let_binder -> "let" | Intern
 
 let comment_type_delimiters = function Lexer.Comment_line -> ("//", "") | Lexer.Comment_block -> ("/*", "*/")
 
-type chunk =
+type infix_chunk = Infix_prefix of string | Infix_op of string | Infix_chunks of chunks
+
+and chunk =
   | Comment of Lexer.comment_type * int * int * string
   | Spacer of bool * int
   | Function of {
@@ -118,6 +120,7 @@ type chunk =
   | Unary of string * chunks
   | Binary of chunks * string * chunks
   | Ternary of chunks * string * chunks * string * chunks
+  | Infix_sequence of infix_chunk list
   | Index of chunks * chunks
   | Delim of string
   | Opt_delim of string
@@ -326,6 +329,17 @@ let rec prerr_chunk indent = function
           Queue.iter (prerr_chunk (indent ^ "    ")) arg
         )
         [("x", x); ("y", y); ("z", z)]
+  | Infix_sequence infix_chunks ->
+      Printf.eprintf "%sInfix:\n" indent;
+      List.iter
+        (function
+          | Infix_prefix op -> Printf.eprintf "%s  Prefix:%s\n" indent op
+          | Infix_op op -> Printf.eprintf "%s  Op:%s\n" indent op
+          | Infix_chunks chunks ->
+              Printf.eprintf "%s  Chunks:\n" indent;
+              Queue.iter (prerr_chunk (indent ^ "    ")) chunks
+          )
+        infix_chunks
   | Delim str -> Printf.eprintf "%sDelim:%s\n" indent str
   | Opt_delim str -> Printf.eprintf "%sOpt_delim:%s\n" indent str
   | Exists ex ->
@@ -521,6 +535,23 @@ let chunk_delimit ?delim ~get_loc ~chunk comments xs =
     )
     xs
 
+let chunk_infix_token comments chunk_primary (infix_token, _, _) =
+  match infix_token with
+  | IT_op id -> Infix_op (string_of_id id)
+  | IT_prefix id -> (
+      match id with
+      | Id_aux (Id "__deref", _) -> Infix_prefix "*"
+      | Id_aux (Id "pow2", _) -> Infix_prefix "2 ^"
+      | 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;
+      Infix_chunks chunks
+
 let rec chunk_atyp comments chunks (ATyp_aux (aux, l)) =
   pop_comments comments chunks l;
   let rec_chunk_atyp atyp =
@@ -534,10 +565,17 @@ let rec chunk_atyp comments chunks (ATyp_aux (aux, l)) =
   | 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) ->
-      (* We would need more granular location information to do anything better here *)
-      Queue.add
-        (Atom (Printf.sprintf "%s in {%s}" (string_of_var n) (Util.string_of_list ", " Big_int.to_string set)))
-        chunks
+      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;
+      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
+      let rhs_chunks = rec_chunk_atyp rhs in
+      Queue.add (Binary (lhs_chunks, op, rhs_chunks)) chunks
+  | ATyp_infix infix_tokens ->
+      let infix_chunks = List.map (chunk_infix_token comments chunk_atyp) infix_tokens in
+      Queue.add (Infix_sequence infix_chunks) chunks
   | (ATyp_times (lhs, rhs) | ATyp_sum (lhs, rhs) | ATyp_minus (lhs, rhs)) as binop ->
       let op_symbol =
         match binop with
@@ -757,6 +795,13 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
   | E_exit exp ->
       let exp_chunks = rec_chunk_exp exp in
       Queue.add (App (Id_aux (Id "exit", Unknown), [exp_chunks])) chunks
+  | E_infix [(IT_primary lhs, _, _); (IT_op (Id_aux (Id op, _)), _, _); (IT_primary rhs, _, _)] ->
+      let lhs_chunks = rec_chunk_exp lhs in
+      let rhs_chunks = rec_chunk_exp rhs in
+      Queue.add (Binary (lhs_chunks, op, rhs_chunks)) chunks
+  | E_infix infix_tokens ->
+      let infix_chunks = List.map (chunk_infix_token comments chunk_exp) infix_tokens in
+      Queue.add (Infix_sequence infix_chunks) chunks
   | E_app_infix (lhs, op, rhs) ->
       let lhs_chunks = rec_chunk_exp lhs in
       let rhs_chunks = rec_chunk_exp rhs in
diff --git a/src/lib/chunk_ast.mli b/src/lib/chunk_ast.mli
index a17d07aa6..c360d2fd6 100644
--- a/src/lib/chunk_ast.mli
+++ b/src/lib/chunk_ast.mli
@@ -84,7 +84,9 @@ val match_keywords : match_kind -> string * string option
 
 val comment_type_delimiters : Lexer.comment_type -> string * string
 
-type chunk =
+type infix_chunk = Infix_prefix of string | Infix_op of string | Infix_chunks of chunks
+
+and chunk =
   | Comment of Lexer.comment_type * int * int * string
   | Spacer of bool * int
   | Function of {
@@ -110,6 +112,7 @@ type chunk =
   | Unary of string * chunks
   | Binary of chunks * string * chunks
   | Ternary of chunks * string * chunks * string * chunks
+  | Infix_sequence of infix_chunk list
   | Index of chunks * chunks
   | Delim of string
   | Opt_delim of string
diff --git a/src/lib/dune b/src/lib/dune
index 5950e74ad..b4dbd4dc4 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -97,6 +97,10 @@
 (menhir
  (modules parser))
 
+(menhir
+ (modules infix_parser)
+ (flags --table))
+
 (ocamllex lexer)
 
 (generate_sites_module
@@ -106,6 +110,6 @@
 (library
  (name libsail)
  (public_name libsail)
- (libraries lem linksem pprint dune-site yojson)
+ (libraries lem linksem pprint dune-site yojson menhirLib)
  (instrumentation
   (backend bisect_ppx)))
diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml
index 5fd967a6e..409c094a2 100644
--- a/src/lib/format_sail.ml
+++ b/src/lib/format_sail.ml
@@ -266,6 +266,8 @@ let precedence n opts = { opts with precedence = n }
 
 let atomic_parens opts doc = if opts.precedence <= 0 then parens doc else doc
 
+let subatomic_parens opts doc = if opts.precedence < 0 then parens doc else doc
+
 (* While everything in Sail is an expression, for formatting we
    recognize that some constructs will appear as either statement-like
    or expression-like depending on where they occur. For example, and
@@ -287,12 +289,22 @@ let expression_like opts = { opts with statement = false }
 let statement_like opts = { opts with statement = true }
 
 let operator_precedence = function
-  | "=" -> (10, atomic, nonatomic, 1)
+  | "=" -> (10, precedence 1, nonatomic, 1)
   | ":" -> (0, subatomic, subatomic, 1)
   | ".." -> (10, atomic, atomic, 0)
   | "@" -> (6, precedence 5, precedence 6, 1)
   | _ -> (10, subatomic, subatomic, 1)
 
+let max_precedence infix_chunks =
+    List.fold_left (fun max_prec infix_chunk ->
+      match infix_chunk with
+      | Infix_op op ->
+        let prec, _, _, _ = operator_precedence op in
+        max prec max_prec
+      | _ ->
+        max_prec
+    ) 0 infix_chunks
+
 let intersperse_operator_precedence = function "@" -> (6, precedence 5) | _ -> (10, subatomic)
 
 let ternary_operator_precedence = function
@@ -412,6 +424,18 @@ module Make (Config : CONFIG) = struct
         let outer_prec, inner_prec, spacing = unary_operator_precedence op in
         let doc = string op ^^ spacing ^^ doc_chunks (opts |> inner_prec |> expression_like) exp in
         if outer_prec > opts.precedence then parens doc else doc
+    | Infix_sequence infix_chunks ->
+        let outer_prec = max_precedence infix_chunks in
+        let doc =
+          separate_map empty
+            (function
+              | Infix_prefix op -> string op
+              | Infix_op op -> space ^^ string op ^^ space
+              | Infix_chunks chunks -> doc_chunks (opts |> atomic |> expression_like) chunks
+              )
+            infix_chunks
+        in
+        if outer_prec > opts.precedence then parens doc else doc
     | Binary (lhs, op, rhs) ->
         let outer_prec, lhs_prec, rhs_prec, spacing = operator_precedence op in
         let doc =
@@ -462,7 +486,7 @@ module Make (Config : CONFIG) = struct
     | Index (exp, ix) ->
         let exp_doc = doc_chunks (opts |> atomic |> expression_like) exp in
         let ix_doc = doc_chunks (opts |> nonatomic |> expression_like) ix in
-        exp_doc ^^ surround indent 0 (char '[') ix_doc (char ']') |> atomic_parens opts
+        exp_doc ^^ surround indent 0 (char '[') ix_doc (char ']') |> subatomic_parens opts
     | Exists ex ->
         let ex_doc =
           doc_chunks (atomic opts) ex.vars
diff --git a/src/lib/infix_parser.mly b/src/lib/infix_parser.mly
new file mode 100644
index 000000000..2586fb1d8
--- /dev/null
+++ b/src/lib/infix_parser.mly
@@ -0,0 +1,425 @@
+
+%{
+
+[@@@coverage exclude_file]
+
+module Big_int = Nat_big_num
+open Parse_ast
+
+let loc n m = Range (n, m)
+
+let mk_id id n m = Id_aux (id, loc n m)
+let mk_typ t n m = ATyp_aux (t, loc n m)
+let mk_exp e n m = E_aux (e, loc n m)
+
+let deinfix = function
+  | (Id_aux (Id v, l)) -> Id_aux (Operator v, l)
+  | (Id_aux (Operator v, l)) -> Id_aux (Id v, l)
+
+type lchain =
+  LC_lt
+| LC_lteq
+| LC_nexp of atyp
+
+let tyop op t1 t2 s e = mk_typ (ATyp_app (Id_aux (Operator 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] -> 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 = 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 = tyop "<" n1 n2 s e in
+     tyop "&" nc1 (desugar_lchain (LC_nexp n2 :: chain) s e) s e
+  | _ -> assert false
+
+type rchain =
+  RC_gt
+| RC_gteq
+| RC_nexp of atyp
+
+let rec desugar_rchain chain s e =
+  match chain with
+  | [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 = 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 = tyop ">" n1 n2 s e in
+     tyop "&" nc1 (desugar_rchain (RC_nexp n2 :: chain) s e) s e
+  | _ -> assert false
+
+%}
+
+%token Eof
+
+%token <Parse_ast.exp> Exp
+%token <Parse_ast.atyp> Typ
+
+%token <Parse_ast.id> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
+%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 TwoCaret
+%token <Nat_big_num.num list> InSet
+
+%start typ_eof
+%start exp_eof
+%type <Parse_ast.atyp> typ_eof
+%type <Parse_ast.exp> exp_eof
+
+%%
+
+typ_eof:
+  | t = typ0; Eof
+    { t }
+
+typ0:
+  | typ1 Op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ0l Op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 Op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 { $1 }
+typ0l:
+  | typ1 Op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ0l Op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 { $1 }
+typ0r:
+  | typ1 Op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 Op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 { $1 }
+
+typ1:
+  | typ2 Op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1l Op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 Op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 { $1 }
+typ1l:
+  | typ2 Op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1l Op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 { $1 }
+typ1r:
+  | typ2 Op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 Op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 { $1 }
+
+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 { $1 }
+typ2l:
+  | 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 { $1 }
+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 { $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 { $1 }
+typ3l:
+  | 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 { $1 }
+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 { $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 { $1 }
+typ4l:
+  | 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 { $1 }
+typ4r:
+  | typ5 Op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ5 Op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ5 { $1 }
+
+typ5:
+  | 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 }
+  | typ6 { $1 }
+typ5l:
+  | 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 { $1 }
+typ5r:
+  | typ6 Op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6 Op5r typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6 { $1 }
+
+typ6:
+  | typ7 Op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6l Op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7 Op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
+  | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos }
+  | typ7 { $1 }
+typ6l:
+  | typ7 Op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6l Op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
+  | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos }
+  | typ7 { $1 }
+typ6r:
+  | typ7 Op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7 Op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7 { $1 }
+
+typ7:
+  | typ8 Op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7l Op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8 Op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos }
+  | typ8 { $1 }
+typ7l:
+  | typ8 Op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7l Op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos }
+  | typ8 { $1 }
+typ7r:
+  | typ8 Op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8 Op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8 { $1 }
+
+typ8:
+  | typ9 Op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8l Op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ9 Op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
+  | typ9 { $1 }
+typ8l:
+  | typ9 Op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8l Op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
+  | typ9 { $1 }
+typ8r:
+  | typ9 Op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ9 Op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
+  | typ9 { $1 }
+
+typ9:
+  | atomic_typ InSet
+    { mk_typ (ATyp_nset ($1, $2)) $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 }
+  | atomic_typ { $1 }
+typ9l:
+  | 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 { $1 }
+typ9r:
+  | atomic_typ Op9 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 }
+  | atomic_typ { $1 }
+
+lchain:
+  | typ5 LtEq typ5
+    { [LC_nexp $1; LC_lteq; LC_nexp $3] }
+  | typ5 Lt typ5
+    { [LC_nexp $1; LC_lt; LC_nexp $3] }
+  | typ5 LtEq lchain
+    { LC_nexp $1 :: LC_lteq :: $3 }
+  | typ5 Lt lchain
+    { LC_nexp $1 :: LC_lt :: $3 }
+
+rchain:
+  | typ5 GtEq typ5
+    { [RC_nexp $1; RC_gteq; RC_nexp $3] }
+  | typ5 Gt typ5
+    { [RC_nexp $1; RC_gt; RC_nexp $3] }
+  | typ5 GtEq rchain
+    { RC_nexp $1 :: RC_gteq :: $3 }
+  | typ5 Gt rchain
+    { RC_nexp $1 :: RC_gt :: $3 }
+
+atomic_typ:
+  | Typ
+    { $1 }
+
+exp_eof:
+  | exp0 Eof
+    { $1 }
+
+exp0:
+  | exp1 Op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp0l Op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 Op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 { $1 }
+exp0l:
+  | exp1 Op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp0l Op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 { $1 }
+exp0r:
+  | exp1 Op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 Op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1 { $1 }
+
+exp1:
+  | exp2 Op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1l Op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 Op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 { $1 }
+exp1l:
+  | exp2 Op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp1l Op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 { $1 }
+exp1r:
+  | exp2 Op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 Op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2 { $1 }
+
+exp2:
+  | exp3 Op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2l Op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 { $1 }
+exp2l:
+  | exp3 Op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp2l Op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 { $1 }
+exp2r:
+  | exp3 Op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 { $1 }
+
+exp3:
+  | exp4 Op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3l Op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 { $1 }
+exp3l:
+  | exp4 Op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3l Op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 { $1 }
+exp3r:
+  | exp4 Op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 { $1 }
+
+exp4:
+  | exp5 Op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp4l Op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 Op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 { $1 }
+exp4l:
+  | exp5 Op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4l Op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 { $1 }
+exp4r:
+  | exp5 Op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 Op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 { $1 }
+
+exp5:
+  | exp6 Op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5l Op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 Op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
+  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
+  | exp6 { $1 }
+exp5l:
+  | exp6 Op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5l Op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 { $1 }
+exp5r:
+  | exp6 Op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 Op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
+  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
+  | exp6 { $1 }
+
+exp6:
+  | exp7 Op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6l Op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7 Op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp7 { $1 }
+exp6l:
+  | exp7 Op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6l Op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp7 { $1 }
+exp6r:
+  | exp7 Op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7 Op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7 { $1 }
+
+exp7:
+  | exp8 Op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7l Op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp8 Op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp8 { $1 }
+exp7l:
+  | exp8 Op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7l Op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp8 { $1 }
+exp7r:
+  | exp8 Op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp8 Op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp8 { $1 }
+
+exp8:
+  | exp9 Op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp8l Op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp9 Op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
+  | exp9 { $1 }
+exp8l:
+  | exp9 Op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp8l Op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
+  | exp9 { $1 }
+exp8r:
+  | exp9 Op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp9 Op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
+  | exp9 { $1 }
+
+exp9:
+  | atomic_exp Op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp9l Op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp Op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp { $1 }
+exp9l:
+  | atomic_exp Op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp9l Op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp { $1 }
+exp9r:
+  | atomic_exp Op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp Op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | atomic_exp { $1 }
+
+atomic_exp:
+  | Star atomic_exp { mk_exp (E_deref $2) $startpos $endpos }
+  | Exp
+    { $1 }
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
index 8a21ddcb3..7bd99120c 100644
--- a/src/lib/initial_check.ml
+++ b/src/lib/initial_check.ml
@@ -93,6 +93,7 @@ type ctx = {
   kinds : kind_aux KBindings.t;
   type_constructors : type_constructor Bindings.t;
   scattereds : ctx Bindings.t;
+  fixities : (prec * int) Bindings.t;
   internal_files : StringSet.t;
   target_sets : string list StringMap.t;
 }
@@ -101,6 +102,7 @@ let rec equal_ctx ctx1 ctx2 =
   KBindings.equal ( = ) ctx1.kinds ctx2.kinds
   && Bindings.equal ( = ) ctx1.type_constructors ctx2.type_constructors
   && Bindings.equal equal_ctx ctx1.scattereds ctx2.scattereds
+  && Bindings.equal ( = ) ctx1.fixities ctx2.fixities
   && StringSet.equal ctx1.internal_files ctx2.internal_files
   && StringMap.equal ( = ) ctx1.target_sets ctx2.target_sets
 
@@ -125,6 +127,10 @@ let merge_ctx l ctx1 ctx2 =
       Bindings.merge
         (compatible equal_ctx (fun id -> "Scattered definition " ^ string_of_id id ^ " found with mismatching context"))
         ctx1.scattereds ctx2.scattereds;
+    fixities =
+      Bindings.merge
+        (compatible ( = ) (fun id -> "Operator " ^ string_of_id id ^ " declared with multiple fixities"))
+        ctx1.fixities ctx2.fixities;
     internal_files = StringSet.union ctx1.internal_files ctx2.internal_files;
     target_sets =
       StringMap.merge
@@ -161,6 +167,121 @@ let to_ast_id ctx (P.Id_aux (id, l)) =
   end
   else to_ast_id' id
 
+let to_infix_parser_op =
+  let open Infix_parser in
+  function
+  | Infix, 0, x -> Op0 x
+  | InfixL, 0, x -> Op0l x
+  | InfixR, 0, x -> Op0r x
+  | Infix, 1, x -> Op1 x
+  | InfixL, 1, x -> Op1l x
+  | InfixR, 1, x -> Op1r x
+  | Infix, 2, x -> Op2 x
+  | InfixL, 2, x -> Op2l x
+  | InfixR, 2, x -> Op2r x
+  | Infix, 3, x -> Op3 x
+  | InfixL, 3, x -> Op3l x
+  | InfixR, 3, x -> Op3r x
+  | Infix, 4, x -> Op4 x
+  | InfixL, 4, x -> Op4l x
+  | InfixR, 4, x -> Op4r x
+  | Infix, 5, x -> Op5 x
+  | InfixL, 5, x -> Op5l x
+  | InfixR, 5, x -> Op5r x
+  | Infix, 6, x -> Op6 x
+  | InfixL, 6, x -> Op6l x
+  | InfixR, 6, x -> Op6r x
+  | Infix, 7, x -> Op7 x
+  | InfixL, 7, x -> Op7l x
+  | InfixR, 7, x -> Op7r x
+  | Infix, 8, x -> Op8 x
+  | InfixL, 8, x -> Op8l x
+  | InfixR, 8, x -> Op8r x
+  | Infix, 9, x -> Op9 x
+  | InfixL, 9, x -> Op9l x
+  | InfixR, 9, x -> Op9r x
+  | _ -> Reporting.unreachable P.Unknown __POS__ "Invalid fixity"
+
+let parse_infix :
+      'a 'b.
+      P.l ->
+      ctx ->
+      ('a P.infix_token * Lexing.position * Lexing.position) list ->
+      ('a -> Infix_parser.token) ->
+      'b Infix_parser.MenhirInterpreter.checkpoint ->
+      'b =
+ fun l ctx infix_tokens mk_primary checkpoint ->
+  let open Infix_parser in
+  let tokens =
+    ref
+      (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)
+               | Id_aux (Id "negate", _) -> (Minus, s, e)
+               | Id_aux (Id "__deref", _) -> (Star, s, e)
+               | _ -> raise (Reporting.err_general (P.Range (s, e)) "Unknown prefix operator")
+             )
+           | P.IT_op id, s, e -> (
+               match id with
+               | Id_aux (Id "+", _) -> (Plus, s, e)
+               | Id_aux (Id "-", _) -> (Minus, s, e)
+               | Id_aux (Id "*", _) -> (Star, s, e)
+               | Id_aux (Id "<", _) -> (Lt, s, e)
+               | Id_aux (Id ">", _) -> (Gt, s, e)
+               | Id_aux (Id "<=", _) -> (LtEq, s, e)
+               | Id_aux (Id ">=", _) -> (GtEq, s, e)
+               | Id_aux (Id "::", _) -> (ColonColon, s, e)
+               | Id_aux (Id "@", _) -> (At, 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)
+                   | None ->
+                       raise
+                         (Reporting.err_general
+                            (P.Range (s, e))
+                            ("Undeclared fixity for operator " ^ string_of_parse_id id)
+                         )
+                 )
+             )
+           )
+         infix_tokens
+      )
+  in
+  let supplier () : token * Lexing.position * Lexing.position =
+    match !tokens with
+    | [((_, _, e) as token)] ->
+        tokens := [(Infix_parser.Eof, e, e)];
+        token
+    | token :: rest ->
+        tokens := rest;
+        token
+    | [] -> assert false
+  in
+  try MenhirInterpreter.loop supplier checkpoint
+  with Infix_parser.Error -> raise (Reporting.err_syntax_loc l "Failed to parse infix expression")
+
+let parse_infix_exp ctx = function
+  | P.E_aux (P.E_infix infix_tokens, l) -> (
+      match infix_tokens with
+      | (_, s, _) :: _ ->
+          parse_infix l ctx infix_tokens (fun exp -> Infix_parser.Exp exp) (Infix_parser.Incremental.exp_eof s)
+      | [] -> Reporting.unreachable l __POS__ "Found empty infix expression"
+    )
+  | exp -> exp
+
+let parse_infix_atyp ctx = function
+  | P.ATyp_aux (P.ATyp_infix infix_tokens, l) -> (
+      match infix_tokens with
+      | (_, s, _) :: _ ->
+          parse_infix l ctx infix_tokens (fun typ -> Infix_parser.Typ typ) (Infix_parser.Incremental.typ_eof s)
+      | [] -> Reporting.unreachable l __POS__ "Found empty infix type"
+    )
+  | atyp -> atyp
+
 let to_ast_var (P.Kid_aux (P.Var v, l)) = Kid_aux (Var v, l)
 
 (* Used for error messages involving lists of kinds *)
@@ -194,7 +315,8 @@ let to_ast_kopts ctx (P.KOpt_aux (aux, l)) =
         attr
       )
 
-let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
+let rec to_ast_typ ctx atyp =
+  let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in
   match aux with
   | P.ATyp_id id -> Typ_aux (Typ_id (to_ast_id ctx id), l)
   | P.ATyp_var v -> Typ_aux (Typ_var (to_ast_var v), l)
@@ -255,7 +377,8 @@ and to_ast_typ_arg ctx (ATyp_aux (_, l) as atyp) = function
   | K_int -> A_aux (A_nexp (to_ast_nexp ctx atyp), l)
   | K_bool -> A_aux (A_bool (to_ast_constraint ctx atyp), l)
 
-and to_ast_nexp ctx (P.ATyp_aux (aux, l)) =
+and to_ast_nexp ctx atyp =
+  let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in
   match aux with
   | P.ATyp_id id -> Nexp_aux (Nexp_id (to_ast_id ctx id), l)
   | P.ATyp_var v -> Nexp_aux (Nexp_var (to_ast_var v), l)
@@ -269,7 +392,8 @@ and to_ast_nexp ctx (P.ATyp_aux (aux, l)) =
   | P.ATyp_parens atyp -> to_ast_nexp ctx atyp
   | _ -> raise (Reporting.err_typ l "Invalid numeric expression in type")
 
-and to_ast_bitfield_index_nexp ctx (P.ATyp_aux (aux, l)) =
+and to_ast_bitfield_index_nexp ctx atyp =
+  let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in
   match aux with
   | P.ATyp_id id -> Nexp_aux (Nexp_id (to_ast_id ctx id), l)
   | P.ATyp_lit (P.L_aux (P.L_num c, _)) -> Nexp_aux (Nexp_constant c, l)
@@ -291,7 +415,8 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
   | P.ATyp_parens atyp -> to_ast_order ctx atyp
   | _ -> raise (Reporting.err_typ l "Invalid order in type")
 
-and to_ast_constraint ctx (P.ATyp_aux (aux, l)) =
+and to_ast_constraint ctx atyp =
+  let (P.ATyp_aux (aux, l)) = parse_infix_atyp ctx atyp in
   match aux with
   | P.ATyp_parens atyp -> to_ast_constraint ctx atyp
   | _ ->
@@ -344,7 +469,7 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l)) =
         | 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 (id, bounds) -> NC_set (to_ast_var id, bounds)
+        | P.ATyp_nset (P.ATyp_aux (P.ATyp_var v, _), bounds) -> NC_set (to_ast_var v, bounds)
         | _ -> raise (Reporting.err_typ l "Invalid constraint")
       in
       NC_aux (aux, l)
@@ -480,7 +605,8 @@ and to_ast_fpat ctx (P.FP_aux (aux, l)) =
 let rec to_ast_letbind ctx (P.LB_aux (lb, l) : P.letbind) : uannot letbind =
   LB_aux ((match lb with P.LB_val (pat, exp) -> LB_val (to_ast_pat ctx pat, to_ast_exp ctx exp)), (l, empty_uannot))
 
-and to_ast_exp ctx (P.E_aux (exp, l) : P.exp) =
+and to_ast_exp ctx exp =
+  let (P.E_aux (exp, l)) = parse_infix_exp ctx exp in
   match exp with
   | P.E_attribute (attr, arg, exp) ->
       let (E_aux (exp, (exp_l, annot))) = to_ast_exp ctx exp in
@@ -490,7 +616,7 @@ and to_ast_exp ctx (P.E_aux (exp, l) : P.exp) =
   | _ ->
       let aux =
         match exp with
-        | P.E_attribute _ -> assert false
+        | P.E_attribute _ | P.E_infix _ -> assert false
         | P.E_block exps -> (
             match to_ast_fexps false ctx exps with
             | Some fexps -> E_struct fexps
@@ -589,7 +715,8 @@ and to_ast_measure ctx (P.Measure_aux (m, l)) : uannot internal_loop_measure =
   in
   Measure_aux (m, l)
 
-and to_ast_lexp ctx (P.E_aux (exp, l) : P.exp) : uannot lexp =
+and to_ast_lexp ctx exp =
+  let (P.E_aux (exp, l)) = parse_infix_exp ctx exp in
   let lexp =
     match exp with
     | P.E_id id -> LE_id (to_ast_id ctx id)
@@ -1058,7 +1185,12 @@ let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out
       | None -> to_ast_def (Some doc_comment) attrs ctx def
     end
   | P.DEF_overload (id, ids) -> ([DEF_aux (DEF_overload (to_ast_id ctx id, List.map (to_ast_id ctx) ids), annot)], ctx)
-  | P.DEF_fixity (prec, n, op) -> ([DEF_aux (DEF_fixity (to_ast_prec prec, n, to_ast_id ctx op), annot)], ctx)
+  | P.DEF_fixity (prec, n, op) ->
+      let op = to_ast_id ctx op in
+      let prec = to_ast_prec prec in
+      ( [DEF_aux (DEF_fixity (prec, n, op), annot)],
+        { ctx with fixities = Bindings.add op (prec, Big_int.to_int n) ctx.fixities }
+      )
   | P.DEF_type t_def -> to_ast_typedef ctx annot t_def
   | P.DEF_fundef f_def ->
       let fd = to_ast_fundef ctx f_def in
@@ -1188,6 +1320,19 @@ let initial_ctx =
         ];
     kinds = KBindings.empty;
     scattereds = Bindings.empty;
+    fixities =
+      List.fold_left
+        (fun m (k, prec, level) -> Bindings.add (mk_id k) (prec, level) m)
+        Bindings.empty
+        [
+          ("^", InfixR, 8);
+          ("|", InfixR, 2);
+          ("&", InfixR, 3);
+          ("==", Infix, 4);
+          ("!=", Infix, 4);
+          ("/", InfixL, 7);
+          ("%", InfixL, 7);
+        ];
     internal_files = StringSet.empty;
     target_sets = StringMap.empty;
   }
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
index 18ec186ba..82131731d 100644
--- a/src/lib/lexer.mll
+++ b/src/lib/lexer.mll
@@ -71,52 +71,9 @@ module Big_int = Nat_big_num
 open Parse_ast
 module M = Map.Make(String)
 
-let r = fun s -> s (* Ulib.Text.of_latin1 *)
 (* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
 let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
 
-let mk_operator prec n op =
-  match prec, n with
-  | Infix, 0 -> Op0 op
-  | Infix, 1 -> Op1 op
-  | Infix, 2 -> Op2 op
-  | Infix, 3 -> Op3 op
-  | Infix, 4 -> Op4 op
-  | Infix, 5 -> Op5 op
-  | Infix, 6 -> Op6 op
-  | Infix, 7 -> Op7 op
-  | Infix, 8 -> Op8 op
-  | Infix, 9 -> Op9 op
-  | InfixL, 0 -> Op0l op
-  | InfixL, 1 -> Op1l op
-  | InfixL, 2 -> Op2l op
-  | InfixL, 3 -> Op3l op
-  | InfixL, 4 -> Op4l op
-  | InfixL, 5 -> Op5l op
-  | InfixL, 6 -> Op6l op
-  | InfixL, 7 -> Op7l op
-  | InfixL, 8 -> Op8l op
-  | InfixL, 9 -> Op9l op
-  | InfixR, 0 -> Op0r op
-  | InfixR, 1 -> Op1r op
-  | InfixR, 2 -> Op2r op
-  | InfixR, 3 -> Op3r op
-  | InfixR, 4 -> Op4r op
-  | InfixR, 5 -> Op5r op
-  | InfixR, 6 -> Op6r op
-  | InfixR, 7 -> Op7r op
-  | InfixR, 8 -> Op8r op
-  | InfixR, 9 -> Op9r op
-  | _, _ -> assert false
-
-let operators = ref
-  (List.fold_left
-     (fun r (x, y) -> M.add x y r)
-     M.empty
-     [ ("/", mk_operator InfixL 7 "/");
-       ("%", mk_operator InfixL 7 "%");
-     ])
-
 let kw_table =
   List.fold_left
     (fun r (x,y) -> M.add x y r)
@@ -247,23 +204,17 @@ rule token = parse
   | "\r\n"
     { Lexing.new_line lexbuf;
       token lexbuf }
-  | "&"					{ (Amp(r"&")) }
-  | "@"                                 { (At "@") }
+  | "@"                                 { At }
   | "2" ws "^"                          { TwoCaret }
-  | "^"					{ (Caret(r"^")) }
-  | "::"                                { ColonColon(r "::") }
-  | ":"                                 { Colon(r ":") }
+  | "^"					{ Caret }
+  | "::"                                { ColonColon }
+  | ":"                                 { Colon ":" }
   | ","                                 { Comma }
   | ".."                                { DotDot }
   | "."                                 { Dot }
-  | "=="                                { EqEq(r"==") }
-  | "="                                 { (Eq(r"=")) }
-  | ">"					{ (Gt(r">")) }
-  | "-"					{ Minus }
-  | "<"					{ (Lt(r"<")) }
-  | "+"					{ (Plus(r"+")) }
+  | "="                                 { Eq "=" }
   | ";"                                 { Semi }
-  | "*"                                 { (Star(r"*")) }
+  | "*"                                 { Star }
   | "_"                                 { Under }
   | "[|"                                { LsquareBar }
   | "|]"                                { RsquareBar }
@@ -272,17 +223,15 @@ rule token = parse
   | "|"                                 { Bar }
   | "{"                                 { Lcurly }
   | "}"                                 { Rcurly }
-  | "()"                                { Unit(r"()") }
+  | "()"                                { Unit "()" }
   | "("                                 { Lparen }
   | ")"                                 { Rparen }
   | "["                                 { Lsquare }
   | "]"                                 { Rsquare }
-  | "!="				{ (ExclEq(r"!=")) }
-  | ">="				{ (GtEq(r">=")) }
   | "->"                                { MinusGt }
+  | "-"                                 { Minus }
   | "<->"                               { Bidir }
-  | "=>"                                { EqGt(r "=>") }
-  | "<="				{ (LtEq(r"<=")) }
+  | "=>"                                { EqGt "=>" }
   | "/*!" wsc*  { Doc (doc_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 false lexbuf) }
   | "//"        { line_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf; token lexbuf }
   | "/*"        { comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf; token lexbuf }
@@ -292,17 +241,12 @@ rule token = parse
   | "$" (ident+ as i)
     { let p = pragma (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in Pragma(i, String.trim p) }
   | "infix" ws (digit as p) ws (operator as op)
-    { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
-      Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
+    { Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
   | "infixl" ws (digit as p) ws (operator as op)
-    { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators;
-      Fixity (InfixL, Big_int.of_string (Char.escaped p), op) }
+    { Fixity (InfixL, Big_int.of_string (Char.escaped p), op) }
   | "infixr" ws (digit as p) ws (operator as op)
-    { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators;
-      Fixity (InfixR, Big_int.of_string (Char.escaped p), op) }
-  | operator as op
-    { try M.find op !operators
-      with Not_found -> raise (Reporting.err_lex (Lexing.lexeme_start_p lexbuf) ("Operator fixity undeclared " ^ op)) }
+    { Fixity (InfixR, Big_int.of_string (Char.escaped p), op) }
+  | operator as op                        { OpId op }
   | tyvar_start startident ident* as i    { TyVar i }
   | "~"                                   { Id "~" }
   | startident ident* as i                { if M.mem i kw_table then
diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml
index 61832914e..e43e4e66a 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -125,6 +125,8 @@ 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 lit_aux =
   | (* Literal constant *)
     L_unit (* $() : _$ *)
@@ -146,12 +148,13 @@ type atyp_aux =
   | ATyp_id of id (* identifier *)
   | ATyp_var of kid (* ticked variable *)
   | ATyp_lit of lit (* literal *)
-  | ATyp_nset of kid * Big_int.num list (* set type *)
+  | ATyp_nset of atyp * Big_int.num list (* set type *)
   | ATyp_times of atyp * atyp (* product *)
   | ATyp_sum of atyp * atyp (* sum *)
   | ATyp_minus of atyp * atyp (* subtraction *)
   | ATyp_exp of atyp (* exponential *)
   | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *)
+  | ATyp_infix of (atyp infix_token * Lexing.position * Lexing.position) list
   | ATyp_inc (* increasing *)
   | ATyp_dec (* decreasing *)
   | ATyp_set of base_effect list (* effect set *)
@@ -234,6 +237,7 @@ and exp_aux =
   | E_typ of atyp * exp (* cast *)
   | E_app of id * exp list (* function application *)
   | E_app_infix of exp * id * exp (* infix function application *)
+  | E_infix of (exp infix_token * Lexing.position * Lexing.position) list
   | E_tuple of exp list (* tuple *)
   | E_if of exp * exp * exp * if_loc (* conditional *)
   | E_loop of loop * measure * exp * exp
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index 6dcf773f7..20896b5fd 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -68,12 +68,20 @@
 %{
 
 [@@@coverage exclude_file]
-  
+
 module Big_int = Nat_big_num
 open Parse_ast
 
 let loc n m = Range (n, m)
 
+let first_pat_range other = function
+  | P_aux (_, Range (pos, _)) -> pos
+  | _ -> other
+
+let first_mpat_range other = function
+  | MP_aux (_, Range (pos, _)) -> pos
+  | _ -> other
+
 let default_opt x = function
   | None -> x
   | Some y -> y
@@ -94,9 +102,25 @@ let mk_kopt k n m = KOpt_aux (k, loc n m)
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
-let deinfix = function
-  | (Id_aux (Id v, l)) -> Id_aux (Operator v, l)
-  | (Id_aux (Operator v, l)) -> Id_aux (Id v, l)
+let simp_infix = function
+  | E_aux (E_infix [(IT_primary exp, _, _)], _) -> exp
+  | exp -> exp
+
+let simp_infix_typ = function
+  | ATyp_aux (ATyp_infix [(IT_primary typ, _, _)], _) -> typ
+  | typ -> typ
+
+let rec same_pat_ops (Id_aux (_, l) as op) = function
+  | ((Id_aux (_, l') as op'), _) :: ops ->
+     if string_of_id op = string_of_id op' then
+       same_pat_ops op ops
+     else
+       raise (Reporting.err_syntax_loc
+                (Parse_ast.Hint (string_of_id op ^ " here", l, l'))
+                (Printf.sprintf "Use parenthesis to group operators in pattern. Operators %s and %s found at same level."
+                                (string_of_id op)
+                                (string_of_id op')))
+  | [] -> ()
 
 let mk_effect e n m = BE_aux (e, loc n m)
 let mk_typ t n m = ATyp_aux (t, loc n m)
@@ -129,7 +153,7 @@ let mk_reg_dec d n m = DEC_aux (d, loc n m)
 let mk_default d n m = DT_aux (d, loc n m)
 let mk_outcome ev n m = OV_aux (ev, loc n m)
 let mk_subst ev n m = IS_aux (ev, loc n m)
- 
+
 let mk_mpexp mpexp n m = MPat_aux (mpexp, loc n m)
 let mk_mpat mpat n m = MP_aux (mpat, loc n m)
 let mk_bidir_mapcl mpexp1 mpexp2 n m = MCL_aux (MCL_bidir (mpexp1, mpexp2), loc n m)
@@ -215,7 +239,7 @@ 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"
- 
+
 %}
 
 /*Terminals with no content*/
@@ -232,7 +256,7 @@ let warn_extern_effect l =
 %nonassoc Then
 %nonassoc Else
 
-%token Bar Comma Dot Eof Minus Semi Under DotDot
+%token Bar Comma Dot Eof Minus Semi Under DotDot At ColonColon Caret Star
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar
 %token MinusGt Bidir
 
@@ -242,17 +266,11 @@ let warn_extern_effect l =
 %token <Nat_big_num.num> Num
 %token <string> String Bin Hex Real
 
-%token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
-%token <string> Colon ColonColon ExclEq
-%token <string> EqEq
-%token <string> GtEq
-%token <string> LtEq
+%token <string> Eq EqGt Unit Colon
 
 %token <string> Doc
 
-%token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
-%token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
-%token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
+%token <string> OpId
 
 %token <string * string> Pragma
 %token <string * string> Attribute
@@ -275,84 +293,57 @@ let warn_extern_effect l =
 id:
   | Id { mk_id (Id $1) $startpos $endpos }
 
-  | Op Op0 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op1 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op2 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op3 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op4 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op5 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op6 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op7 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op8 { mk_id (Operator $2) $startpos $endpos }
-  | Op Op9 { mk_id (Operator $2) $startpos $endpos }
-
-  | Op Op0l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op1l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op2l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op3l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op4l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op5l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op6l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op7l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op8l { mk_id (Operator $2) $startpos $endpos }
-  | Op Op9l { mk_id (Operator $2) $startpos $endpos }
-
-  | Op Op0r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op1r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op2r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op3r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op4r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op5r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op6r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op7r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op8r { mk_id (Operator $2) $startpos $endpos }
-  | Op Op9r { mk_id (Operator $2) $startpos $endpos }
-
-  | Op Plus   { mk_id (Operator "+")  $startpos $endpos }
-  | Op Minus  { mk_id (Operator "-")  $startpos $endpos }
-  | Op Star   { mk_id (Operator "*")  $startpos $endpos }
-  | Op EqEq   { mk_id (Operator "==") $startpos $endpos }
-  | Op ExclEq { mk_id (Operator "!=") $startpos $endpos }
-  | Op Lt     { mk_id (Operator "<")  $startpos $endpos }
-  | Op Gt     { mk_id (Operator ">")  $startpos $endpos }
-  | Op LtEq   { mk_id (Operator "<=") $startpos $endpos }
-  | Op GtEq   { mk_id (Operator ">=") $startpos $endpos }
-  | Op Amp    { mk_id (Operator "&")  $startpos $endpos }
-  | Op Bar    { mk_id (Operator "|")  $startpos $endpos }
-  | Op Caret  { mk_id (Operator "^")  $startpos $endpos }
-
-op0: Op0 { mk_id (Id $1) $startpos $endpos }
-op1: Op1 { mk_id (Id $1) $startpos $endpos }
-op2: Op2 { mk_id (Id $1) $startpos $endpos }
-op3: Op3 { mk_id (Id $1) $startpos $endpos }
-op4: Op4 { mk_id (Id $1) $startpos $endpos }
-op5: Op5 { mk_id (Id $1) $startpos $endpos }
-op6: Op6 { mk_id (Id $1) $startpos $endpos }
-op7: Op7 { mk_id (Id $1) $startpos $endpos }
-op8: Op8 { mk_id (Id $1) $startpos $endpos }
-op9: Op9 { mk_id (Id $1) $startpos $endpos }
-
-op0l: Op0l { mk_id (Id $1) $startpos $endpos }
-op1l: Op1l { mk_id (Id $1) $startpos $endpos }
-op2l: Op2l { mk_id (Id $1) $startpos $endpos }
-op3l: Op3l { mk_id (Id $1) $startpos $endpos }
-op4l: Op4l { mk_id (Id $1) $startpos $endpos }
-op5l: Op5l { mk_id (Id $1) $startpos $endpos }
-op6l: Op6l { mk_id (Id $1) $startpos $endpos }
-op7l: Op7l { mk_id (Id $1) $startpos $endpos }
-op8l: Op8l { mk_id (Id $1) $startpos $endpos }
-op9l: Op9l { mk_id (Id $1) $startpos $endpos }
-
-op0r: Op0r { mk_id (Id $1) $startpos $endpos }
-op1r: Op1r { mk_id (Id $1) $startpos $endpos }
-op2r: Op2r { mk_id (Id $1) $startpos $endpos }
-op3r: Op3r { mk_id (Id $1) $startpos $endpos }
-op4r: Op4r { mk_id (Id $1) $startpos $endpos }
-op5r: Op5r { mk_id (Id $1) $startpos $endpos }
-op6r: Op6r { mk_id (Id $1) $startpos $endpos }
-op7r: Op7r { mk_id (Id $1) $startpos $endpos }
-op8r: Op8r { mk_id (Id $1) $startpos $endpos }
-op9r: Op9r { mk_id (Id $1) $startpos $endpos }
+  | Op OpId { mk_id (Operator $2) $startpos $endpos }
+  | Op Minus { mk_id (Operator "-") $startpos $endpos }
+  | Op Bar { mk_id (Operator "|") $startpos $endpos }
+  | Op Caret { mk_id (Operator "^") $startpos $endpos }
+  | Op Star { mk_id (Operator "*") $startpos $endpos }
+
+op_no_caret:
+  | OpId
+    { mk_id (Id $1) $startpos $endpos }
+  | Minus
+    { mk_id (Id "-") $startpos $endpos }
+  | Bar
+    { mk_id (Id "|") $startpos $endpos }
+  | Star
+    { mk_id (Id "*") $startpos $endpos }
+
+op:
+  | OpId
+    { mk_id (Id $1) $startpos $endpos }
+  | Minus
+    { mk_id (Id "-") $startpos $endpos }
+  | Bar
+    { mk_id (Id "|") $startpos $endpos }
+  | Caret
+    { mk_id (Id "^") $startpos $endpos }
+  | Star
+    { mk_id (Id "*") $startpos $endpos }
+
+exp_op:
+  | OpId
+    { mk_id (Id $1) $startpos $endpos }
+  | Minus
+    { mk_id (Id "-") $startpos $endpos }
+  | Bar
+    { mk_id (Id "|") $startpos $endpos }
+  | At
+    { mk_id (Id "@") $startpos $endpos }
+  | ColonColon
+    { mk_id (Id "::") $startpos $endpos }
+  | Caret
+    { mk_id (Id "^") $startpos $endpos }
+  | Star
+    { mk_id (Id "*") $startpos $endpos }
+
+pat_op:
+  | At
+    { mk_id (Id "@") $startpos $endpos }
+  | ColonColon
+    { mk_id (Id "::") $startpos $endpos }
+  | Caret
+    { mk_id (Id "^") $startpos $endpos }
 
 id_list:
   | id
@@ -370,26 +361,6 @@ num_list:
   | Num Comma num_list
     { $1 :: $3 }
 
-lchain:
-  | typ5 LtEq typ5
-    { [LC_nexp $1; LC_lteq; LC_nexp $3] }
-  | typ5 Lt typ5
-    { [LC_nexp $1; LC_lt; LC_nexp $3] }
-  | typ5 LtEq lchain
-    { LC_nexp $1 :: LC_lteq :: $3 }
-  | typ5 Lt lchain
-    { LC_nexp $1 :: LC_lt :: $3 }
-
-rchain:
-  | typ5 GtEq typ5
-    { [RC_nexp $1; RC_gteq; RC_nexp $3] }
-  | typ5 Gt typ5
-    { [RC_nexp $1; RC_gt; RC_nexp $3] }
-  | typ5 GtEq rchain
-    { RC_nexp $1 :: RC_gteq :: $3 }
-  | typ5 Gt rchain
-    { RC_nexp $1 :: RC_gt :: $3 }
-
 tyarg:
   | Lparen typ_list Rparen
     { [], $2 }
@@ -398,175 +369,42 @@ typ_eof:
   | typ Eof
     { $1 }
 
+%inline prefix_typ_op:
+  |
+    { [] }
+  | TwoCaret
+    { [(IT_prefix (mk_id (Id "pow2") $startpos $endpos), $startpos, $endpos)] }
+  | Minus
+    { [(IT_prefix (mk_id (Id "negate") $startpos $endpos), $startpos, $endpos)] }
+  | Star
+    { [(IT_prefix (mk_id (Id "__deref") $startpos $endpos), $startpos, $endpos)] }
+
+postfix_typ:
+  | t = atomic_typ
+    { [(IT_primary t, $startpos, $endpos)] }
+  | t = atomic_typ; i = In; Lcurly; xs = num_list; Rcurly
+    { [(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:
+  | prefix = prefix_typ_op;
+    x = postfix_typ;
+    xs = list(op = op_no_caret; prefix = prefix_typ_op; y = postfix_typ { (IT_op op, $startpos(op), $endpos(op)) :: prefix @ y })
+    { simp_infix_typ (mk_typ (ATyp_infix (prefix @ x @ List.concat xs))
+                             (match prefix with [] -> $startpos(x) | _ -> $startpos)
+                             $endpos) }
+
 typ:
-  | typ0
-    { $1 }
+  | prefix = prefix_typ_op;
+    x = postfix_typ;
+    xs = list(op = op; prefix = prefix_typ_op; y = postfix_typ { (IT_op op, $startpos(op), $endpos(op)) :: prefix @ y })
+    { simp_infix_typ (mk_typ (ATyp_infix (prefix @ x @ List.concat xs))
+                             (match prefix with [] -> $startpos(x) | _ -> $startpos)
+                             $endpos) }
 
 /* The following implements all nine levels of user-defined precedence for
 operators in types, with both left, right and non-associative operators */
 
-typ0:
-  | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1 { $1 }
-typ0l:
-  | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ0l op0l typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1 { $1 }
-typ0r:
-  | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1 op0r typ0r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1 { $1 }
-
-typ1:
-  | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ2 { $1 }
-typ1l:
-  | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ1l op1l typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ2 { $1 }
-typ1r:
-  | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ2 op1r typ1r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ2 { $1 }
-
-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 }
-  | typ2l op2l typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ3 { $1 }
-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 }
-  | typ3l op3l typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ4 { $1 }
-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 }
-  | typ4l op4l typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ5 { $1 }
-typ4r:
-  | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ5 op4r typ4r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ5 { $1 }
-
-typ5:
-  | 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 }
-  | typ6 { $1 }
-typ5l:
-  | 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 { $1 }
-typ5r:
-  | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6 op5r typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6 { $1 }
-
-typ6:
-  | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
-  | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos }
-  | typ7 { $1 }
-typ6l:
-  | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6l op6l typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ6l Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
-  | typ6l Minus typ7 { mk_typ (ATyp_minus ($1, $3)) $startpos $endpos }
-  | typ7 { $1 }
-typ6r:
-  | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7 op6r typ6r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7 { $1 }
-
-typ7:
-  | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos }
-  | typ8 { $1 }
-typ7l:
-  | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7l op7l typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ7l Star typ8 { mk_typ (ATyp_times ($1, $3)) $startpos $endpos }
-  | typ8 { $1 }
-typ7r:
-  | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ8 op7r typ7r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ8 { $1 }
-
-typ8:
-  | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
-  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
-  | typ9 { $1 }
-typ8l:
-  | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
-  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
-  | typ9 { $1 }
-typ8r:
-  | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
-  | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
-  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
-  | 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 }
-  | atomic_typ { $1 }
-typ9l:
-  | 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 { $1 }
-typ9r:
-  | atomic_typ op9 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 }
-  | atomic_typ { $1 }
-
 atomic_typ:
   | id
     { mk_typ (ATyp_id $1) $startpos $endpos }
@@ -590,10 +428,10 @@ atomic_typ:
   | Lparen typ Comma typ_list Rparen
     { mk_typ (ATyp_tuple ($2 :: $4)) $startpos $endpos }
   | LcurlyBar num_list RcurlyBar
-    { let v = mk_kid "n" $startpos $endpos in
+    { 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, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
-      let kopt = mk_kopt (KOpt_kind (None, [v], None)) $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 }
   | 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 }
@@ -711,27 +549,28 @@ typschm_eof:
   | typschm Eof
     { $1 }
 
-pat_string_append:
-  | atomic_pat
-    { [$1] }
-  | atomic_pat Caret pat_string_append
-    { $1 :: $3 }
-
 pat1:
-  | atomic_pat
-    { $1 }
-  | atomic_pat At pat_concat
-    { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
-  | atomic_pat ColonColon pat1
-    { mk_pat (P_cons ($1, $3)) $startpos $endpos }
-  | atomic_pat Caret pat_string_append
-    { mk_pat (P_string_append ($1 :: $3)) $startpos $endpos }
-
-pat_concat:
-  | atomic_pat
-    { [$1] }
-  | atomic_pat At pat_concat
-    { $1 :: $3 }
+  | p = atomic_pat; ps = list(op = pat_op; q = atomic_pat { (op, q) })
+    { match ps with
+      | [] -> p
+      | (op, _) :: rest ->
+         same_pat_ops op rest;
+         match string_of_id op with
+         | "@" ->
+            mk_pat (P_vector_concat (p :: List.map snd ps)) $startpos $endpos
+         | "::" ->
+            let rec cons_list = function
+              | [(_, x)] -> x
+              | ((_, x) :: xs) -> mk_pat (P_cons (x, cons_list xs)) (first_pat_range $startpos x) $endpos
+              | _ -> assert false in
+            mk_pat (P_cons (p, cons_list ps)) $startpos $endpos
+         | "^" ->
+            mk_pat (P_string_append (p :: List.map snd ps)) $startpos $endpos
+         | _ ->
+            raise (Reporting.err_syntax_loc
+                     (loc $startpos $endpos)
+                     ("Unrecognised operator " ^ string_of_id op ^ " in pattern."))
+    }
 
 pat:
   | pat1
@@ -767,7 +606,7 @@ atomic_pat:
     { mk_pat (P_vector_subrange ($1, $3, $5)) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $startpos $endpos }
-  | atomic_pat Colon typ
+  | atomic_pat Colon typ_no_caret
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
   | Lparen pat Rparen
     { $2 }
@@ -830,14 +669,12 @@ exp:
     { $1 }
   | Attribute exp
     { mk_exp (E_attribute (fst $1, snd $1, $2)) $startpos $endpos($1) }
-  | atomic_exp Eq exp
+  | exp0 Eq exp
     { mk_exp (E_assign ($1, $3)) $startpos $endpos }
   | Let_ letbind In exp
     { mk_exp (E_let ($2, $4)) $startpos $endpos }
   | Var atomic_exp Eq exp In exp
     { mk_exp (E_var ($2, $4, $6)) $startpos $endpos }
-  | Star atomic_exp
-    { mk_exp (E_deref $2) $startpos $endpos }
   | Lcurly block Rcurly
     { mk_exp (E_block $2) $startpos $endpos }
   | Return exp
@@ -905,170 +742,23 @@ exp:
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */
 
+%inline prefix_op:
+  |
+    { [] }
+  | TwoCaret
+    { [(IT_prefix (mk_id (Id "pow2") $startpos $endpos), $startpos, $endpos)] }
+  | Minus
+    { [(IT_prefix (mk_id (Id "negate") $startpos $endpos), $startpos, $endpos)] }
+  | Star
+    { [(IT_prefix (mk_id (Id "__deref") $startpos $endpos), $startpos, $endpos)] }
+
 exp0:
-  | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1 { $1 }
-exp0l:
-  | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp0l op0l exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1 { $1 }
-exp0r:
-  | exp1 op0 exp1 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1 op0r exp0r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1 { $1 }
-
-exp1:
-  | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2 { $1 }
-exp1l:
-  | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp1l op1l exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2 { $1 }
-exp1r:
-  | exp2 op1 exp2 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2 op1r exp1r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2 { $1 }
-
-exp2:
-  | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp3 { $1 }
-exp2l:
-  | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3 { $1 }
-exp2r:
-  | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp3 { $1 }
-
-exp3:
-  | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp4 { $1 }
-exp3l:
-  | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4 { $1 }
-exp3r:
-  | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp4 { $1 }
-
-exp4:
-  | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp5 EqEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "==") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 { $1 }
-exp4l:
-  | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 { $1 }
-exp4r:
-  | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5 { $1 }
-
-exp5:
-  | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
-  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
-  | exp6 { $1 }
-exp5l:
-  | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp5l op5l exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 { $1 }
-exp5r:
-  | exp6 op5 exp6 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 op5r exp5r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 At exp5r { mk_exp (E_vector_append ($1, $3)) $startpos $endpos }
-  | exp6 ColonColon exp5r { mk_exp (E_cons ($1, $3)) $startpos $endpos }
-  | exp6 { $1 }
-
-exp6:
-  | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp7 { $1 }
-exp6l:
-  | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6l op6l exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6l Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp6l Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp7 { $1 }
-exp6r:
-  | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7 op6r exp6r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7 { $1 }
-
-exp7:
-  | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp8 { $1 }
-exp7l:
-  | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7l op7l exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp7l Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp8 { $1 }
-exp7r:
-  | exp8 op7 exp8 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp8 op7r exp7r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp8 { $1 }
-
-exp8:
-  | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
-  | exp9 { $1 }
-exp8l:
-  | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
-  | exp9 { $1 }
-exp8r:
-  | exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
-  | exp9 { $1 }
-
-exp9:
-  | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | atomic_exp { $1 }
-exp9l:
-  | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp9l op9l atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | atomic_exp { $1 }
-exp9r:
-  | atomic_exp op9 atomic_exp { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | atomic_exp op9r exp9r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | atomic_exp { $1 }
+  | prefix = prefix_op;
+    x = atomic_exp;
+    xs = list(op = exp_op; prefix = prefix_op; y = atomic_exp { (IT_op op, $startpos(op), $endpos(op)) :: prefix @ [(IT_primary y, $startpos(y), $endpos(y))] })
+    { simp_infix (mk_exp (E_infix (prefix @ ((IT_primary x, $startpos(x), $endpos(x)) :: List.concat xs)))
+                         (match prefix with [] -> $startpos(x) | _ -> $startpos)
+                         $endpos) }
 
 case:
   | pat EqGt exp
@@ -1381,29 +1071,30 @@ fun_def_list:
   | fun_def fun_def_list
     { $1 :: $2 }
 
-mpat_string_append:
-  | atomic_mpat
-    { [$1] }
-  | atomic_mpat Caret mpat_string_append
-    { $1 :: $3 }
-
 mpat:
-  | atomic_mpat
-    { $1 }
-  | atomic_mpat As id
-    { mk_mpat (MP_as ($1, $3)) $startpos $endpos }
-  | atomic_mpat At mpat_concat
-    { mk_mpat (MP_vector_concat ($1 :: $3)) $startpos $endpos }
-  | atomic_mpat ColonColon mpat
-    { mk_mpat (MP_cons ($1, $3)) $startpos $endpos }
-  | atomic_mpat Caret mpat_string_append
-    { mk_mpat (MP_string_append ($1 :: $3)) $startpos $endpos }
-
-mpat_concat:
-  | atomic_mpat
-    { [$1] }
-  | atomic_mpat At mpat_concat
-    { $1 :: $3 }
+  | p = atomic_mpat; ps = list(op = pat_op; q = atomic_mpat { (op, q) })
+    { match ps with
+      | [] -> p
+      | (op, _) :: rest ->
+         same_pat_ops op rest;
+         match string_of_id op with
+         | "@" ->
+            mk_mpat (MP_vector_concat (p :: List.map snd ps)) $startpos $endpos
+         | "::" ->
+            let rec cons_list = function
+              | [(_, x)] -> x
+              | ((_, x) :: xs) -> mk_mpat (MP_cons (x, cons_list xs)) (first_mpat_range $startpos x) $endpos
+              | _ -> assert false in
+            mk_mpat (MP_cons (p, cons_list ps)) $startpos $endpos
+         | "^" ->
+            mk_mpat (MP_string_append (p :: List.map snd ps)) $startpos $endpos
+         | _ ->
+            raise (Reporting.err_syntax_loc
+                     (loc $startpos $endpos)
+                     ("Unrecognised operator " ^ string_of_id op ^ " in mapping pattern."))
+    }
+  | p = atomic_mpat; As; id = id
+    { mk_mpat (MP_as (p, id)) $startpos $endpos }
 
 mpat_list:
   | mpat
@@ -1434,7 +1125,7 @@ atomic_mpat:
     { mk_mpat (MP_list []) $startpos $endpos }
   | LsquareBar mpat_list RsquareBar
     { mk_mpat (MP_list $2) $startpos $endpos }
-  | atomic_mpat Colon typ
+  | atomic_mpat Colon typ_no_caret
     { mk_mpat (MP_typ ($1, $3)) $startpos $endpos }
   | Struct Lcurly separated_nonempty_list(Comma, fmpat) Rcurly
     { mk_mpat (MP_struct $3) $startpos $endpos }
diff --git a/test/c/reg_ref_nb.expect b/test/c/reg_ref_nb.expect
new file mode 100644
index 000000000..02a8cd965
--- /dev/null
+++ b/test/c/reg_ref_nb.expect
@@ -0,0 +1 @@
+*x = 0xFFFF
diff --git a/test/c/reg_ref_nb.sail b/test/c/reg_ref_nb.sail
new file mode 100644
index 000000000..3f6ee9fec
--- /dev/null
+++ b/test/c/reg_ref_nb.sail
@@ -0,0 +1,13 @@
+default Order dec
+
+$include <prelude.sail>
+
+register R : bits(16)
+
+val main : unit -> unit
+
+function main() = {
+    let x = ref R;
+    *x = 0xFFFF;
+    print_bits("*x = ", *x)
+}
diff --git a/test/format/default/struct_update.expect b/test/format/default/struct_update.expect
index d4806d096..88273bc44 100644
--- a/test/format/default/struct_update.expect
+++ b/test/format/default/struct_update.expect
@@ -20,7 +20,7 @@ function baz () = {
         foo = 0xFFFF,
         bar = 0b1,
     };
-    (*R) = baz; // trailing comment
+    *R = baz; // trailing comment
 
     return 3 + (return 4)
 }
diff --git a/test/format/struct_update.sail b/test/format/struct_update.sail
index c0fcaa87a..818c70fee 100644
--- a/test/format/struct_update.sail
+++ b/test/format/struct_update.sail
@@ -16,7 +16,7 @@ val bar : unit -> int
 function baz() = {
     ();
     let some_long_named_variable_to_break_the_line = { function_modify_the_struct(struct_with_a_long_name, x) with foo = 0xFFFF, bar = 0b1 };
-    (*R) = baz; // trailing comment
+    *R = baz; // trailing comment
 
 
     return 3 + (return 4)
diff --git a/test/lexing/unknown_operator.expect b/test/lexing/unknown_operator.expect
index 8b1918e5e..25ae747ec 100644
--- a/test/lexing/unknown_operator.expect
+++ b/test/lexing/unknown_operator.expect
@@ -1,5 +1,5 @@
-Lexical error:
-unknown_operator.sail:6.12-12:
+Error:
+unknown_operator.sail:6.12-17:
 6 |  let _ = x <=|=> y;
-  |            ^
-  | Operator fixity undeclared <=|=>
+  |            ^---^
+  | Undeclared fixity for operator <=|=>