Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments

17 files changed, 605 insertions, 135 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 6a74d5b2..710e8067 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -238,7 +238,6 @@ and typ_arg_aux =  (* Type constructor arguments of all kinds *)
    Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
- | Typ_arg_effect of effect
 
 and typ_arg =
    Typ_arg_aux of typ_arg_aux * l
@@ -261,6 +260,7 @@ type
  | P_as of 'a pat * id (* named pattern *)
  | P_typ of typ * 'a pat (* typed pattern *)
  | P_id of id (* identifier *)
+ | P_var of kid (* bind identifier and type variable *)
  | P_app of id * ('a pat) list (* union constructor pattern *)
  | P_record of ('a fpat) list * bool (* struct pattern *)
  | P_vector of ('a pat) list (* vector pattern *)
@@ -320,6 +320,8 @@ type
  | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
  | E_constraint of n_constraint (* Expression to evaluate the n_constraint at run time *)
  | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_throw of 'a exp
+ | E_try of 'a exp * ('a pexp) list
  | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
  | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
  | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 67381c52..ddd83429 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -77,11 +77,13 @@ and map_exp_annot_aux f = function
   | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, map_fexps_annot f fexps)
   | E_field (exp, id) -> E_field (map_exp_annot f exp, id)
   | E_case (exp, cases) -> E_case (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
+  | E_try (exp, cases) -> E_try (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
   | E_let (letbind, exp) -> E_let (map_letbind_annot f letbind, map_exp_annot f exp)
   | E_assign (lexp, exp) -> E_assign (map_lexp_annot f lexp, map_exp_annot f exp)
   | E_sizeof nexp -> E_sizeof nexp
   | E_constraint nc -> E_constraint nc
   | E_exit exp -> E_exit (map_exp_annot f exp)
+  | E_throw exp -> E_throw (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
   | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
   | E_internal_cast (annot, exp) -> E_internal_cast (f annot, map_exp_annot f exp)
@@ -110,6 +112,7 @@ and map_pat_annot_aux f = function
   | P_as (pat, id) -> P_as (map_pat_annot f pat, id)
   | P_typ (typ, pat) -> P_typ (typ, map_pat_annot f pat)
   | P_id id -> P_id id
+  | P_var kid -> P_var kid
   | P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
   | P_record (fpats, b) -> P_record (List.map (map_fpat_annot f) fpats, b)
   | P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
@@ -143,6 +146,9 @@ let string_of_id = function
   | Id_aux (Id v, _) -> v
   | Id_aux (DeIid v, _) -> "(deinfix " ^ v ^ ")"
 
+let id_of_kid = function
+  | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
+
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
@@ -220,7 +226,6 @@ and string_of_typ_arg_aux = function
   | Typ_arg_nexp n -> string_of_nexp n
   | Typ_arg_typ typ -> string_of_typ typ
   | Typ_arg_order o -> string_of_order o
-  | Typ_arg_effect eff -> string_of_effect eff
 and string_of_n_constraint = function
   | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
   | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
@@ -279,6 +284,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")"
   | E_case (exp, cases) ->
      "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
+  | E_try (exp, cases) ->
+     "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
   | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp
   | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind
   | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
@@ -297,6 +304,7 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ string_of_exp body
   | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
+  | E_throw exp -> "throw " ^ string_of_exp exp
   | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
   | E_list xs -> "[||" ^ string_of_list ", " string_of_exp xs ^ "||]"
   | _ -> "INTERNAL"
@@ -309,6 +317,7 @@ and string_of_pat (P_aux (pat, l)) =
   | P_lit lit -> string_of_lit lit
   | P_wild -> "_"
   | P_id v -> string_of_id v
+  | P_var kid -> string_of_kid kid
   | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
   | P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
   | P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ae340839..94f3f0cc 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -86,6 +86,8 @@ val string_of_index_range : index_range -> string
 
 val id_of_fundef : 'a fundef -> id
 
+val id_of_kid : kid -> id
+
 module Id : sig
   type t = id
   val compare : id -> id -> int
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 9d295dda..e5717389 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -73,7 +73,7 @@ let rec kind_to_string kind = match kind.k with
   | K_Lam (kinds,kind) -> "Lam [" ^ string_of_list ", " kind_to_string kinds ^ "] -> " ^ (kind_to_string kind)
 
 (*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *)
-type envs = Nameset.t * kind Envmap.t * order 
+type envs = Nameset.t * kind Envmap.t * order
 type 'a envs_out = 'a * envs
 
 let id_to_string (Id_aux(id,l)) =
@@ -236,7 +236,7 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
         let n1 = to_ast_nexp k_env t1 in
         let n2 = to_ast_nexp k_env t2 in
         Nexp_aux (Nexp_minus (n1, n2), l)
-     | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None)
+     | _ -> typ_error l "Required an item of kind Nat, encountered an illegal form for this kind" None None None)
 
 and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order =
   match o with
@@ -301,7 +301,6 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg
     | K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg)
     | K_Nat  -> Typ_arg_nexp (to_ast_nexp k_env arg)
     | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg)
-    | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg)
     | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))),
     l)
 
@@ -416,6 +415,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
     | Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id)
     | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
     | Parse_ast.P_id(id) -> P_id(to_ast_id id)
+    | Parse_ast.P_var kid -> P_var (to_ast_var kid)
     | Parse_ast.P_app(id,pats) ->
       if pats = [] 
       then P_id (to_ast_id id)
@@ -498,11 +498,13 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
       | _ -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none"))
     | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id)
     | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
+    | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
     | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp)
     | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc)
     | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp)
     | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
     ), (l,()))
diff --git a/src/lexer.mll b/src/lexer.mll
index 228ca38f..cf3c9baf 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -78,6 +78,9 @@ let kw_table =
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
+     ("try",                     (fun _ -> Try));
+     ("catch",                   (fun _ -> Catch));
+     ("throw",                   (fun _ -> Throw));
      ("forall",                  (fun _ -> Forall));
      ("exist",                   (fun _ -> Exist));
      ("foreach",                 (fun _ -> Foreach));
diff --git a/src/lexer2.mll b/src/lexer2.mll
index a51067aa..f5350ea8 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -49,18 +49,41 @@ 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 n op =
-  match n with
-  | 0 -> Op0 op
-  | 1 -> Op1 op
-  | 2 -> Op2 op
-  | 3 -> Op3 op
-  | 4 -> Op4 op
-  | 5 -> Op5 op
-  | 6 -> Op6 op
-  | 7 -> Op7 op
-  | 8 -> Op8 op
-  | 9 -> Op9 op
+type prec = Infix | InfixL | InfixR
+
+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 M.empty
 
@@ -82,13 +105,11 @@ let kw_table =
      ("def",                     (fun _ -> Def));
      ("op",                      (fun _ -> Op));
      ("default",		 (fun _ -> Default));
-     ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
      ("Effect",                  (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
      ("enum",		         (fun _ -> Enum));
      ("else",                    (fun _ -> Else));
-     ("exit",                    (fun _ -> Exit));
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
@@ -96,6 +117,9 @@ let kw_table =
      ("foreach",                 (fun _ -> Foreach));
      ("function",                (fun x -> Function_));
      ("overload",                (fun _ -> Overload));
+     ("throw",                   (fun _ -> Throw));
+     ("try",                     (fun _ -> Try));
+     ("catch",                   (fun _ -> Catch));
      ("if",                      (fun x -> If_));
      ("in",			 (fun x -> In));
      ("inc",                     (fun _ -> Inc));
@@ -112,7 +136,6 @@ let kw_table =
      ("sizeof",                  (fun x -> Sizeof));
      ("constraint",              (fun x -> Constraint));
      ("struct",                  (fun x -> Struct));
-     ("switch",			 (fun x -> Switch));
      ("then",                    (fun x -> Then));
      ("true",                    (fun x -> True));
      ("Type",                    (fun x -> TYPE));
@@ -120,7 +143,6 @@ let kw_table =
      ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
-     ("when",                    (fun x -> When));
      ("val",                     (fun x -> Val));
 
      ("div",			 (fun x -> Div_));
@@ -145,12 +167,7 @@ let kw_table =
      ("unspec",                  (fun x -> Unspec));
      ("nondet",                  (fun x -> Nondet));
      ("escape",                  (fun x -> Escape));
-
-]
-
-let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int"; "real";
-			  "uint8";"uint16";"uint32";"uint64";"atom";"implicit";"string";"option"]
-let custom_type_names : string list ref = ref []
+   ]
 
 }
 
@@ -164,6 +181,7 @@ let startident = letter|'_'
 let ident = alphanum|['_''\'']
 let tyvar_start = '\''
 let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
+let operator = oper_char+ ('_' ident)?
 let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
 
 rule token = parse
@@ -173,11 +191,12 @@ rule token = parse
     { Lexing.new_line lexbuf;
       token lexbuf }
   | "&"					{ (Amp(r"&")) }
-  | "|"                                 { Bar }
+  | "@"                                 { (At "@") }
   | "2" ws "^"                          { TwoCaret }
   | "^"					{ (Caret(r"^")) }
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
+  | ".."                                { DotDot }
   | "."                                 { Dot }
   | "="                                 { (Eq(r"=")) }
   | ">"					{ (Gt(r">")) }
@@ -187,6 +206,9 @@ rule token = parse
   | ";"                                 { Semi }
   | "*"                                 { (Star(r"*")) }
   | "_"                                 { Under }
+  | "{|"                                { LcurlyBar }
+  | "|}"                                { RcurlyBar }
+  | "|"                                 { Bar }
   | "{"                                 { Lcurly }
   | "}"                                 { Rcurly }
   | "()"                                { Unit(r"()") }
@@ -199,10 +221,16 @@ rule token = parse
   | "->"                                { MinusGt }
   | "=>"                                { EqGt(r "=>") }
   | "<="				{ (LtEq(r"<=")) }
-  | "infix" ws (digit as p) ws (oper_char+ as op)
-    { operators := M.add op (mk_operator (int_of_string (Char.escaped p)) op) !operators;
+  | "infix" ws (digit as p) ws (operator as op)
+    { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
+      token lexbuf }
+  | "infixl" ws (digit as p) ws (operator as op)
+    { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators;
+      token lexbuf }
+  | "infixr" ws (digit as p) ws (operator as op)
+    { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators;
       token lexbuf }
-  | oper_char+ as op
+  | operator as op
     { try M.find op !operators
       with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
   | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index a9ddd1a7..d9ee73b8 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -56,8 +56,7 @@ let subst_src_typ substs t =
     match ta with
     | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (s_snexp ne),l)
     | Typ_arg_typ t -> Typ_arg_aux (Typ_arg_typ (s_styp t),l)
-    | Typ_arg_order _
-    | Typ_arg_effect _ -> targ
+    | Typ_arg_order _ -> targ
   in s_styp t
 
 let make_vector_lit sz i =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 8ce5e77d..3951ab51 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -234,6 +234,7 @@ pat_aux =  (* Pattern *)
  | P_as of pat * id (* named pattern *)
  | P_typ of atyp * pat (* typed pattern *)
  | P_id of id (* identifier *)
+ | P_var of kid
  | P_app of id * (pat) list (* union constructor pattern *)
  | P_record of (fpat) list * bool (* struct pattern *)
  | P_vector of (pat) list (* vector pattern *)
@@ -283,6 +284,8 @@ exp_aux =  (* Expression *)
  | E_sizeof of atyp
  | E_constraint of n_constraint
  | E_exit of exp
+ | E_throw of exp
+ | E_try of exp * pexp list
  | E_return of exp
  | E_assert of exp * exp
 
diff --git a/src/parser.mly b/src/parser.mly
index d6da6e63..12e64141 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -131,7 +131,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
 %token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
-%token Undefined Union With When Val Constraint
+%token Undefined Union With When Val Constraint Try Catch Throw
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 
@@ -609,10 +609,14 @@ atomic_exp:
     { eloc (E_list($2)) }
   | Switch exp Lcurly case_exps Rcurly
     { eloc (E_case($2,$4)) }
+  | Try exp Catch Lcurly case_exps Rcurly
+    { eloc (E_try ($2, $5)) }
   | Sizeof atomic_typ
     { eloc (E_sizeof($2)) }
   | Constraint Lparen nexp_constraint Rparen
     { eloc (E_constraint $3) }
+  | Throw atomic_exp
+    { eloc (E_throw $2) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
   | Return atomic_exp
diff --git a/src/parser2.mly b/src/parser2.mly
index c67fad59..bde542e0 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -53,6 +53,7 @@ let mk_kid str n m = Kid_aux (Var str, loc n m)
 
 let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
 
+let mk_effect e n m = BE_aux (e, loc n m)
 let mk_typ t n m = ATyp_aux (t, loc n m)
 let mk_pat p n m = P_aux (p, loc n m)
 let mk_pexp p n m = Pat_aux (p, loc n m)
@@ -61,12 +62,14 @@ let mk_lit l n m = L_aux (l, loc n m)
 let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
 let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
 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_funcl f n m = FCL_aux (f, loc n m)
 let mk_fun fn n m = FD_aux (fn, loc n m)
 let mk_td t n m = TD_aux (t, loc n m)
 let mk_vs v n m = VS_aux (v, loc n m)
 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 qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l)
 
@@ -118,10 +121,10 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Deinfix Effect EFFECT End Op
-%token Enum Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
-%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With When Val Constraint
+%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Effect EFFECT End Op
+%token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
+%token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
+%token Undefined Union With Val Constraint Throw Try Catch
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 %nonassoc Then
@@ -129,10 +132,10 @@ let rec desugar_rchain chain s e =
 
 %token Div_ Mod ModUnderS Quot Rem QuotUnderS
 
-%token Bar Comma Dot Eof Minus Semi Under
-%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare DotDot
-%token MinusGt LtBar LtColon SquareBar SquareBarBar SquareColon
+%token Bar Comma Dot Eof Minus Semi Under DotDot
+%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar
+%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare
+%token MinusGt LtBar LtColon SquareBar SquareBarBar
 
 /*Terminals with content*/
 
@@ -140,17 +143,14 @@ let rec desugar_rchain chain s e =
 %token <int> Num
 %token <string> String Bin Hex Real
 
-%token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star Tilde EqGt Unit
+%token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star EqGt Unit
 %token <string> Colon ExclEq
 %token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
 %token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar
 
-%token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
-%token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
-%token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi PlusUnderS MinusUnderS
-
 %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
 
 %start file
 %type <Parse_ast.defs> defs
@@ -159,32 +159,44 @@ let rec desugar_rchain chain s e =
 %%
 
 id:
-  | Id
-    { mk_id (Id $1) $startpos $endpos }
-  | Op Op1
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op2
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op3
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op4
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op5
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op6
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op7
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op8
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Op9
-    { mk_id (DeIid $2) $startpos $endpos }
-  | Op Plus
-    { mk_id (DeIid "+") $startpos $endpos }
-  | Op Minus
-    { mk_id (DeIid "-") $startpos $endpos }
-  | Op Star
-    { mk_id (DeIid "*") $startpos $endpos }
+  | Id { mk_id (Id $1) $startpos $endpos }
+
+  | Op Op0 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op1 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op2 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op3 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op4 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op5 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op6 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op7 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op8 { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op9 { mk_id (DeIid $2) $startpos $endpos }
+
+  | Op Op0l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op1l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op2l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op3l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op4l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op5l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op6l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op7l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op8l { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op9l { mk_id (DeIid $2) $startpos $endpos }
+
+  | Op Op0r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op1r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op2r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op3r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op4r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op5r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op6r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op7r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op8r { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op9r { mk_id (DeIid $2) $startpos $endpos }
+
+  | Op Plus { mk_id (DeIid "+") $startpos $endpos }
+  | Op Minus { mk_id (DeIid "-") $startpos $endpos }
+  | Op Star { mk_id (DeIid "*") $startpos $endpos }
 
 op0: Op0 { mk_id (Id $1) $startpos $endpos }
 op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -197,6 +209,28 @@ 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 }
+
 decl:
   | Decl
     { mk_id (Id $1) $startpos $endpos }
@@ -281,48 +315,156 @@ typ:
   | typ0
     { $1 }
 
+/* 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 { $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 }
+  | 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 }
-  | typ6 Plus typ7 { mk_typ (ATyp_sum ($1, $3)) $startpos $endpos }
-  | typ6 Minus typ7 { mk_typ (ATyp_minus ($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 }
-  | typ7 Star typ8 { mk_typ (ATyp_times ($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 }
+  | 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 }
+  | 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 }
   | typ9 { $1 }
 
 typ9:
   | 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:
@@ -342,6 +484,11 @@ atomic_typ:
     { $2 }
   | Lparen typ Comma typ_list Rparen
     { mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos }
+  | LcurlyBar num_list RcurlyBar
+    { 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_nat_set_bounded (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
@@ -386,11 +533,59 @@ typquant:
   | kopt_list
     { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) }
 
+effect:
+  | Barr
+    { mk_effect BE_barr $startpos $endpos }
+  | Depend
+    { mk_effect BE_depend $startpos $endpos }
+  | Rreg
+    { mk_effect BE_rreg $startpos $endpos }
+  | Wreg
+    { mk_effect BE_wreg $startpos $endpos }
+  | Rmem
+    { mk_effect BE_rmem $startpos $endpos }
+  | Rmemt
+    { mk_effect BE_rmemt $startpos $endpos }
+  | Wmem
+    { mk_effect BE_wmem $startpos $endpos }
+  | Wmv
+    { mk_effect BE_wmv $startpos $endpos }
+  | Wmvt
+    { mk_effect BE_wmvt $startpos $endpos }
+  | Eamem
+    { mk_effect BE_eamem $startpos $endpos }
+  | Exmem
+    { mk_effect BE_exmem $startpos $endpos }
+  | Undef
+    { mk_effect BE_undef $startpos $endpos }
+  | Unspec
+    { mk_effect BE_unspec $startpos $endpos }
+  | Nondet
+    { mk_effect BE_nondet $startpos $endpos }
+  | Escape
+    { mk_effect BE_escape $startpos $endpos }
+
+effect_list:
+  | effect
+    { [$1] }
+  | effect Comma effect_list
+    { $1::$3 }
+
+effect_set:
+  | Lcurly effect_list Rcurly
+    { mk_typ (ATyp_set $2) $startpos $endpos }
+  | Pure
+    { mk_typ (ATyp_set []) $startpos $endpos }
+
 typschm:
   | typ MinusGt typ
     { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
   | Forall typquant Dot typ MinusGt typ
     { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
+  | typ MinusGt typ Effect effect_set
+    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, $5)) s e) s e) $startpos $endpos }
+  | Forall typquant Dot typ MinusGt typ Effect effect_set
+    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
 
 pat:
   | atomic_pat
@@ -413,6 +608,12 @@ atomic_pat:
     { mk_pat (P_lit $1) $startpos $endpos }
   | id
     { mk_pat (P_id $1) $startpos $endpos }
+  | kid
+    { mk_pat (P_var $1) $startpos $endpos }
+  | tydecl typ
+    { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos }
+  | id Lparen pat_list Rparen
+    { mk_pat (P_app ($1, $3)) $startpos $endpos }
   | pat Colon typ
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
   | decl typ
@@ -431,6 +632,16 @@ lit:
     { mk_lit (L_num $1) $startpos $endpos }
   | Undefined
     { mk_lit L_undef $startpos $endpos }
+  | Bitzero
+    { mk_lit L_zero $startpos $endpos }
+  | Bitone
+    { mk_lit L_one $startpos $endpos }
+  | Bin
+    { mk_lit (L_bin $1) $startpos $endpos }
+  | Hex
+    { mk_lit (L_hex $1) $startpos $endpos }
+  | String
+    { mk_lit (L_string $1) $startpos $endpos }
 
 exp:
   | cast_exp Colon typ
@@ -449,55 +660,171 @@ cast_exp:
     { mk_exp (E_block $2) $startpos $endpos }
   | Return cast_exp
     { mk_exp (E_return $2) $startpos $endpos }
+  | Throw cast_exp
+    { mk_exp (E_throw $2) $startpos $endpos }
   | If_ exp Then cast_exp Else cast_exp
     { mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
-  | Match exp0 Lcurly case_list Rcurly
+  | If_ exp Then cast_exp
+    { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos }
+  | Match exp Lcurly case_list Rcurly
     { mk_exp (E_case ($2, $4)) $startpos $endpos }
-  | Lparen exp Comma exp_list Rparen
+  | Try exp Catch Lcurly case_list Rcurly
+    { mk_exp (E_try ($2, $5)) $startpos $endpos }
+  | Lparen exp0 Comma exp_list Rparen
     { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
 
+/* The following implements all nine levels of user-defined precedence for
+operators in expressions, with both left, right and non-associative operators */
+
 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 }
+  | 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 { $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 { $1 }
 
 exp6:
   | exp7 op6 exp7 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
-  | exp6 Plus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "+") $startpos($2) $endpos($2), $3)) $startpos $endpos }
-  | exp6 Minus exp7 { mk_exp (E_app_infix ($1, mk_id (Id "-") $startpos($2) $endpos($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 }
-  | exp7 Star exp8 { mk_exp (E_app_infix ($1, mk_id (Id "*") $startpos($2) $endpos($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 }
 
 case:
@@ -515,8 +842,6 @@ case_list:
 block:
   | exp
     { [$1] }
-  | If_ exp Then exp Semi block
-    { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $startpos($5) $endpos($5))) $startpos $endpos($5) :: $6 }
   | Let_ letbind Semi block
     { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] }
   | exp Semi /* Allow trailing semicolon in block */
@@ -539,6 +864,22 @@ atomic_exp:
     { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
   | id Lparen exp_list Rparen
     { mk_exp (E_app ($1, $3)) $startpos $endpos }
+  | Sizeof Lparen typ Rparen
+    { mk_exp (E_sizeof $3) $startpos $endpos }
+  | Constraint Lparen nc Rparen
+    { mk_exp (E_constraint $3) $startpos $endpos }
+  | Assert Lparen exp Comma exp Rparen
+    { mk_exp (E_assert ($3, $5)) $startpos $endpos }
+  | atomic_exp Lsquare exp Rsquare
+    { mk_exp (E_vector_access ($1, $3)) $startpos $endpos }
+  | atomic_exp Lsquare exp DotDot exp Rsquare
+    { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos }
+  | Lsquare exp_list Rsquare
+    { mk_exp (E_vector $2) $startpos $endpos }
+  | Lsquare exp With atomic_exp Eq exp Rsquare
+    { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos }
+  | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare
+    { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos }
   | Lparen exp Rparen
     { $2 }
 
@@ -548,12 +889,6 @@ exp_list:
   | exp Comma exp_list
     { $1 :: $3 }
 
-cast_exp_list:
-  | cast_exp
-    { [$1] }
-  | cast_exp Comma exp_list
-    { $1 :: $3 }
-
 funcl:
   | id pat Eq exp
     { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
@@ -634,6 +969,20 @@ register_def:
   | Register id Colon typ
     { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
 
+default_def:
+  | Default base_kind Inc
+    { mk_default (DT_order ($2, mk_typ ATyp_inc $startpos($3) $endpos)) $startpos $endpos }
+  | Default base_kind Dec
+    { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos }
+
+scattered_def:
+  | Union id typquant
+    { mk_sd (SD_scattered_variant($2, mk_namesectn, $3)) $startpos $endpos }
+  | Union id
+    { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos }
+  | Function_ id
+    { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
+
 def:
   | fun_def
     { DEF_fundef $1 }
@@ -649,6 +998,16 @@ def:
     { DEF_overload ($2, $5) }
   | Overload id Eq enum_bar
     { DEF_overload ($2, $4) }
+  | Scattered scattered_def
+    { DEF_scattered $2 }
+  | Function_ Clause funcl
+    { DEF_scattered (mk_sd (SD_scattered_funcl $3) $startpos $endpos) }
+  | Union Clause id Eq type_union
+    { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) }
+  | End id
+    { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) }
+  | default_def
+    { DEF_default $1 }
 
 defs_list:
   | def
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index bd43c1a7..70f5b749 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -189,7 +189,6 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   | Typ_arg_typ t -> app_typ t
   | Typ_arg_nexp n -> nexp n
   | Typ_arg_order o -> doc_ord o
-  | Typ_arg_effect e -> doc_effects e
 
   (* same trick to handle precedence of nexp *)
   and nexp ne = sum_typ ne
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 586773ca..9b66331b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -208,7 +208,6 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_arg_typ t -> app_typ regtypes true t
       | Typ_arg_nexp n -> empty
       | Typ_arg_order o -> empty
-      | Typ_arg_effect e -> empty
   in typ', atomic_typ
 
 (* Check for variables in types that would be pretty-printed.
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 018a93f5..adddcee6 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -210,8 +210,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
   (match t with
   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
-  | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
-  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^
+  | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")");
   (pp_format_l_lem l) ^ ")"
 and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   "(NC_aux " ^
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index fc02f568..b331a6cf 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -121,7 +121,6 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml =
   | Typ_arg_typ t -> app_typ t
   | Typ_arg_nexp n -> empty
   | Typ_arg_order o -> empty
-  | Typ_arg_effect e -> empty
   in typ, atomic_typ
 
 let doc_lit_ocaml in_pat (L_aux(l,_)) =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a63df7ea..bb1d7357 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -277,6 +277,10 @@ let doc_exp, doc_let =
         (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3)))
   | E_list exps ->
       squarebarbars (separate_map comma exp exps)
+  | E_try(e,pexps) ->
+      let opening = separate space [string "try"; exp e; string "catch"; lbrace] in
+      let cases = separate_map (break 1) doc_case pexps in
+      surround 2 1 opening cases rbrace
   | E_case(e,pexps) ->
       let opening = separate space [string "switch"; exp e; lbrace] in
       let cases = separate_map (break 1) doc_case pexps in
@@ -287,6 +291,8 @@ let doc_exp, doc_let =
      string "constraint" ^^ parens (doc_nexp_constraint nc)
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
+  | E_throw e ->
+    separate space [string "throw"; atomic_exp e;]
   | E_return e ->
     separate space [string "return"; atomic_exp e;]
   | E_assert(c,m) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index a2481f3f..ec0b4a58 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -149,6 +149,8 @@ let vector_typ n m ord typ =
                     mk_typ_arg (Typ_arg_order ord);
                     mk_typ_arg (Typ_arg_typ typ)]))
 
+let exc_typ = mk_id_typ (mk_id "exception")
+
 let is_range (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
@@ -194,7 +196,7 @@ let rec nc_negate (NC_aux (nc, _)) =
   | NC_or (n1, n2) -> mk_nc (NC_and (nc_negate n1, nc_negate n2))
   | NC_false -> mk_nc NC_true
   | NC_true -> mk_nc NC_false
-  | NC_nat_set_bounded (kid, []) -> typ_error Parse_ast.Unknown "Cannot negate empty nexp set"
+  | NC_nat_set_bounded (kid, []) -> nc_false
   | NC_nat_set_bounded (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
   | NC_nat_set_bounded (kid, int :: ints) ->
      mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_nat_set_bounded (kid, ints)))))
@@ -318,7 +320,6 @@ and typ_subst_arg_nexp_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp)
   | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ)
   | Typ_arg_order ord -> Typ_arg_order ord
-  | Typ_arg_effect eff -> Typ_arg_effect eff
 
 let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l)
 and typ_subst_typ_aux sv subst = function
@@ -334,7 +335,6 @@ and typ_subst_arg_typ_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
   | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ)
   | Typ_arg_order ord -> Typ_arg_order ord
-  | Typ_arg_effect eff -> Typ_arg_effect eff
 
 let order_subst_aux sv subst = function
   | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid
@@ -357,7 +357,6 @@ and typ_subst_arg_order_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp nexp
   | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ)
   | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord)
-  | Typ_arg_effect eff -> Typ_arg_effect eff
 
 let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l)
 and typ_subst_kid_aux sv subst = function
@@ -374,7 +373,6 @@ and typ_subst_arg_kid_aux sv subst = function
   | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp)
   | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ)
   | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord)
-  | Typ_arg_effect eff -> Typ_arg_effect eff
 
 let quant_item_subst_kid_aux sv subst = function
   | QI_id (KOpt_aux (KOpt_none kid, l)) as qid ->
@@ -582,7 +580,6 @@ end = struct
     | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp
     | Typ_arg_typ typ -> wf_typ ~exs:exs env typ
     | Typ_arg_order ord -> wf_order env ord
-    | Typ_arg_effect _ -> () (* Check: is this ever used? *)
   and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) =
     match nexp_aux with
     | Nexp_id _ -> ()
@@ -814,7 +811,7 @@ end = struct
     then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
     else
       begin
-        typ_debug ("Adding kind identifier binding " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k);
+        typ_print ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k);
         { env with typ_vars = KBindings.add kid k env.typ_vars }
       end
 
@@ -964,7 +961,7 @@ let fresh_existential () =
   let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter), Parse_ast.Unknown) in
   incr ex_counter; fresh
 
-let destructure_exist env typ =
+let destruct_exist env typ =
   match Env.expand_synonyms env typ with
   | Typ_aux (Typ_exist (kids, nc, typ), _) ->
      let fresh_kids = List.map (fun kid -> (kid, fresh_existential ())) kids in
@@ -981,8 +978,8 @@ let exist_typ constr typ =
   let fresh_kid = fresh_existential () in
   mk_typ (Typ_exist ([fresh_kid], constr fresh_kid, typ fresh_kid))
 
-let destruct_vector_typ env typ =
-  let destruct_vector_typ' = function
+let destruct_vector env typ =
+  let destruct_vector' = function
     | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
                              Typ_arg_aux (Typ_arg_nexp n2, _);
                              Typ_arg_aux (Typ_arg_order o, _);
@@ -990,7 +987,7 @@ let destruct_vector_typ env typ =
                        ), _) when string_of_id id = "vector" -> Some (n1, n2, o, vtyp)
     | typ -> None
   in
-  destruct_vector_typ' (Env.expand_synonyms env typ)
+  destruct_vector' (Env.expand_synonyms env typ)
 
 (**************************************************************************)
 (* 3. Subtyping and constraint solving                                    *)
@@ -1073,7 +1070,6 @@ and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) =
   | Typ_arg_nexp n -> Tnf_arg_nexp n
   | Typ_arg_typ typ -> Tnf_arg_typ (normalize_typ env typ)
   | Typ_arg_order o -> Tnf_arg_order o
-  | Typ_arg_effect e -> Tnf_arg_effect e
 
 (* Here's how the constraint generation works for subtyping
 
@@ -1258,7 +1254,6 @@ and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   | Typ_arg_nexp n -> nexp_frees ~exs:exs n
   | Typ_arg_typ typ -> typ_frees ~exs:exs typ
   | Typ_arg_order ord -> order_frees ord
-  | Typ_arg_effect _ -> assert false
 
 let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
   match nexp1, nexp2 with
@@ -1300,7 +1295,6 @@ and typ_arg_identical (Typ_arg_aux (arg1, _)) (Typ_arg_aux (arg2, _)) =
   | Typ_arg_nexp n1, Typ_arg_nexp n2 -> nexp_identical n1 n2
   | Typ_arg_typ typ1, Typ_arg_typ typ2 -> typ_identical typ1 typ2
   | Typ_arg_order ord1, Typ_arg_order ord2 -> ord_identical ord1 ord2
-  | Typ_arg_effect _, Typ_arg_effect _ -> assert false
 
 type uvar =
   | U_nexp of nexp
@@ -1475,10 +1469,9 @@ let rec unify l env typ1 typ2 =
        end
     | Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2
     | Typ_arg_order ord1, Typ_arg_order ord2 -> unify_order l ord1 ord2
-    | Typ_arg_effect _, Typ_arg_effect _ -> assert false
     | _, _ -> unify_error l (string_of_typ_arg typ_arg1 ^ " cannot be unified with type argument " ^ string_of_typ_arg typ_arg2)
   in
-  match destructure_exist env typ2 with
+  match destruct_exist env typ2 with
   | Some (kids, nc, typ2) ->
      let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in
      let (unifiers, _, _) = unify l env typ1 typ2 in
@@ -1508,7 +1501,7 @@ let uv_nexp_constraint env (kid, uvar) =
   | _ -> env
 
 let rec subtyp l env typ1 typ2 =
-  match destructure_exist env typ1, destructure_exist env typ2 with
+  match destruct_exist env typ1, destruct_exist env typ2 with
   | Some (kids, nc, typ1), _ ->
      let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
      let env = Env.add_constraint nc env in
@@ -1626,8 +1619,8 @@ let rec instantiate_quants quants kid uvar = match quants with
        | _ -> (QI_aux (QI_const nc, l)) :: instantiate_quants quants kid uvar
      end
 
-let destructure_vec_typ l env typ =
-  let destructure_vec_typ' l = function
+let destruct_vec_typ l env typ =
+  let destruct_vec_typ' l = function
     | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n1, _);
                              Typ_arg_aux (Typ_arg_nexp n2, _);
                              Typ_arg_aux (Typ_arg_order o, _);
@@ -1635,7 +1628,7 @@ let destructure_vec_typ l env typ =
                        ), _) when string_of_id id = "vector" -> (n1, n2, o, vtyp)
     | typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ)
   in
-  destructure_vec_typ' l (Env.expand_synonyms env typ)
+  destruct_vec_typ' l (Env.expand_synonyms env typ)
 
 
 let env_of_annot (l, tannot) = match tannot with
@@ -1660,7 +1653,7 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
 (* Flow typing *)
 
-let destructure_atom (Typ_aux (typ_aux, _)) =
+let destruct_atom (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant c, _)), _)])
        when string_of_id f = "atom" -> c
@@ -1668,7 +1661,7 @@ let destructure_atom (Typ_aux (typ_aux, _)) =
        when string_of_id f = "range" && c1 = c2 -> c1
   | _ -> assert false
 
-let destructure_atom_nexp (Typ_aux (typ_aux, _)) =
+let destruct_atom_nexp (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
        when string_of_id f = "atom" -> n
@@ -1721,36 +1714,36 @@ let apply_flow_constraint = function
 let rec infer_flow env (E_aux (exp_aux, (l, _))) =
   match exp_aux with
   | E_app (f, [x; y]) when string_of_id f = "lteq_atom_atom" ->
-     let n1 = destructure_atom_nexp (typ_of x) in
-     let n2 = destructure_atom_nexp (typ_of y) in
+     let n1 = destruct_atom_nexp (typ_of x) in
+     let n2 = destruct_atom_nexp (typ_of y) in
      [], [nc_lteq n1 n2]
   | E_app (f, [x; y]) when string_of_id f = "gteq_atom_atom" ->
-     let n1 = destructure_atom_nexp (typ_of x) in
-     let n2 = destructure_atom_nexp (typ_of y) in
+     let n1 = destruct_atom_nexp (typ_of x) in
+     let n2 = destruct_atom_nexp (typ_of y) in
      [], [nc_gteq n1 n2]
   | E_app (f, [x; y]) when string_of_id f = "lt_atom_atom" ->
-     let n1 = destructure_atom_nexp (typ_of x) in
-     let n2 = destructure_atom_nexp (typ_of y) in
+     let n1 = destruct_atom_nexp (typ_of x) in
+     let n2 = destruct_atom_nexp (typ_of y) in
      [], [nc_lt n1 n2]
   | E_app (f, [x; y]) when string_of_id f = "gt_atom_atom" ->
-     let n1 = destructure_atom_nexp (typ_of x) in
-     let n2 = destructure_atom_nexp (typ_of y) in
+     let n1 = destruct_atom_nexp (typ_of x) in
+     let n2 = destruct_atom_nexp (typ_of y) in
      [], [nc_gt n1 n2]
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destructure_atom (typ_of y) in
+     let c = destruct_atom (typ_of y) in
      [(v, Flow_lteq (c - 1))], []
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destructure_atom (typ_of y) in
+     let c = destruct_atom (typ_of y) in
      [(v, Flow_lteq c)], []
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gt_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destructure_atom (typ_of y) in
+     let c = destruct_atom (typ_of y) in
      [(v, Flow_gteq (c + 1))], []
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "gteq_range_atom" ->
      let kid = Env.fresh_kid env in
-     let c = destructure_atom (typ_of y) in
+     let c = destruct_atom (typ_of y) in
      [(v, Flow_gteq c)], []
   | _ -> [], []
 
@@ -1877,6 +1870,18 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
      in
      annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ
+  | E_try (exp, cases), _ ->
+     let checked_exp = crule check_exp env exp typ in
+     let check_case pat typ = match pat with
+       | Pat_aux (Pat_exp (pat, case), (l, _)) ->
+          let tpat, env = bind_pat env pat exc_typ in
+          Pat_aux (Pat_exp (tpat, crule check_exp env case typ), (l, None))
+       | Pat_aux (Pat_when (pat, guard, case), (l, _)) ->
+          let tpat, env = bind_pat env pat exc_typ in
+          let checked_guard = check_exp env guard bool_typ in
+          Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
+     in
+     annot_exp (E_try (checked_exp, List.map (fun case -> check_case case typ) cases)) typ
   | E_cons (x, xs), _ ->
      begin
        match is_list (Env.expand_synonyms env typ) with
@@ -1941,9 +1946,12 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_exit exp, _ ->
      let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
      annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape])
+  | E_throw exp, _ ->
+     let checked_exp = crule check_exp env exp exc_typ in
+     annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
   | E_vector vec, _ ->
      begin
-       let (start, len, ord, vtyp) = destructure_vec_typ l env typ in
+       let (start, len, ord, vtyp) = destruct_vec_typ l env typ in
        let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
        match nexp_simp len with
        | Nexp_aux (Nexp_constant lenc, _) ->
@@ -2056,6 +2064,23 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
             | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
           end
      end
+  | P_var kid ->
+     begin
+       let v = id_of_kid kid in
+       match Env.lookup_id v env with
+       | Local (Immutable, _) | Unbound ->
+          begin
+            match destruct_exist env typ with
+            | Some ([kid'], nc, typ) ->
+               let env = Env.add_typ_var kid BK_nat env in
+               let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in
+               let env = Env.add_local v (Immutable, typ_subst_nexp kid' (Nexp_var kid) typ) env in
+               annot_pat (P_var kid) typ, env
+            | Some _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential")
+            | None _ -> typ_error l ("Cannot bind type variable against non existential type")
+          end
+       | _ -> typ_error l ("Bad type identifer pattern: " ^ string_of_pat pat)
+     end
   | P_wild -> annot_pat P_wild typ, env
   | P_cons (hd_pat, tl_pat) ->
      begin
@@ -2171,9 +2196,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
        pats @ [inferred_pat], env
      in
      let (inferred_pat :: inferred_pats), env = List.fold_left fold_pats ([], env) (pat :: pats) in
-     let (_, len, _, vtyp) = destructure_vec_typ l env (pat_typ_of inferred_pat) in
+     let (_, len, _, vtyp) = destruct_vec_typ l env (pat_typ_of inferred_pat) in
      let fold_len len pat =
-       let (_, len', _, vtyp') = destructure_vec_typ l env (pat_typ_of pat) in
+       let (_, len', _, vtyp') = destruct_vec_typ l env (pat_typ_of pat) in
        typ_equality l env vtyp vtyp';
        nsum len len'
      in
@@ -2729,6 +2754,11 @@ and propagate_exp_effect_aux = function
      let p_cases = List.map propagate_pexp_effect cases in
      let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
      E_case (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
+  | E_try (exp, cases) ->
+     let p_exp = propagate_exp_effect exp in
+     let p_cases = List.map propagate_pexp_effect cases in
+     let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
+     E_try (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
   | E_for (v, f, t, step, ord, body) ->
      let p_f = propagate_exp_effect f in
      let p_t = propagate_exp_effect t in
@@ -2756,6 +2786,9 @@ and propagate_exp_effect_aux = function
   | E_exit exp ->
      let p_exp = propagate_exp_effect exp in
      E_exit p_exp, effect_of p_exp
+  | E_throw exp ->
+     let p_exp = propagate_exp_effect exp in
+     E_throw p_exp, effect_of p_exp
   | E_return exp ->
      let p_exp = propagate_exp_effect exp in
      E_return p_exp, effect_of p_exp
@@ -2813,6 +2846,7 @@ and propagate_pat_effect_aux = function
      let p_pat = propagate_pat_effect pat in
      P_typ (typ, p_pat), effect_of_pat p_pat
   | P_id id -> P_id id, no_effect
+  | P_var kid -> P_var kid, no_effect
   | P_app (id, pats) ->
      let p_pats = List.map propagate_pat_effect pats in
      P_app (id, p_pats), collect_effects_pat p_pats
diff --git a/src/type_check.mli b/src/type_check.mli
index 0a85624c..d451e4d9 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -135,6 +135,7 @@ module Env : sig
 
 end
 
+(* Push all the type variables and constraints from a typquant into an environment *)
 val add_typquant : typquant -> Env.t -> Env.t
 
 (* Some handy utility functions for constructing types. *)
@@ -155,9 +156,24 @@ val nsum : nexp -> nexp -> nexp
 val ntimes : nexp -> nexp -> nexp
 val npow2 : nexp -> nexp
 val nvar : kid -> nexp
-val nid : id -> nexp
+val nid : id -> nexp (* NOTE: Nexp_id's don't do anything currently *)
 
+(* Numeric constraint builders *)
+val nc_eq : nexp -> nexp -> n_constraint
+val nc_neq : nexp -> nexp -> n_constraint
+val nc_lteq : nexp -> nexp -> n_constraint
 val nc_gteq : nexp -> nexp -> n_constraint
+val nc_lt : nexp -> nexp -> n_constraint
+val nc_gt : nexp -> nexp -> n_constraint
+val nc_and : n_constraint -> n_constraint -> n_constraint
+val nc_or : n_constraint -> n_constraint -> n_constraint
+val nc_true : n_constraint
+val nc_false : n_constraint
+
+(* Negate a n_constraint. Note that there's no NC_not constructor, so
+   this flips all the inequalites a the n_constraint leaves and uses
+   de-morgans to switch and to or and vice versa. *)
+val nc_negate : n_constraint -> n_constraint
 
 (* Sail builtin types. *)
 val int_typ : typ
@@ -172,6 +188,7 @@ val real_typ : typ
 val vector_typ : nexp -> nexp -> order -> typ -> typ
 val list_typ : typ -> typ
 val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
+val exc_typ : typ
 
 val inc_ord : order
 val dec_ord : order
@@ -217,9 +234,15 @@ val pat_typ_of : tannot pat -> typ
 val effect_of : tannot exp -> effect
 val effect_of_annot : tannot -> effect
 
-val destructure_atom_nexp : typ -> nexp
+(* TODO: make return option *)
+val destruct_atom_nexp : typ -> nexp
 
-val destruct_vector_typ : Env.t -> typ -> (nexp * nexp * order * typ) option
+(* Safely destructure an existential type. Returns None if the type is
+   not existential. This function will pick a fresh name for the
+   existential to ensure that no name-clashes occur. *)
+val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option
+
+val destruct_vector : Env.t -> typ -> (nexp * nexp * order * typ) option
 
 type uvar =
   | U_nexp of nexp