Merge branch 'experiments' into mono-experiments

16 files changed, 245 insertions, 8 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 710e8067..1728f492 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -289,6 +289,7 @@ type
 'a reg_id_aux =
    RI_id of id
 
+type loop = While | Until
 
 type
 'a exp_aux =  (* Expression *)
@@ -301,7 +302,8 @@ type
  | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
  | E_tuple of ('a exp) list (* tuple *)
  | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
- | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *)
+ | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* for loop *)
+ | E_loop of loop * 'a exp * 'a exp
  | E_vector of ('a exp) list (* vector (indexed from 0) *)
  | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *)
  | E_vector_access of 'a exp * 'a exp (* vector access *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2f630021..048fbb15 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -70,6 +70,14 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
 
 let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, pat, body), no_annot)
 
+let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown)
+
+let mk_qi_id bk kid =
+  let kopt =
+    KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown)
+  in
+  QI_aux (QI_id kopt, Parse_ast.Unknown)
+
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
   let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
@@ -155,6 +163,8 @@ let range_typ nexp1 nexp2 =
 let bool_typ = mk_id_typ (mk_id "bool")
 let string_typ = mk_id_typ (mk_id "string")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
+let tuple_typ typs = mk_typ (Typ_tup typs)
+let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff))
 
 let vector_typ n m ord typ =
   mk_typ (Typ_app (mk_id "vector",
@@ -173,6 +183,7 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
 let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
 let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
 
+let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints))
 let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
 let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
 let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
@@ -210,6 +221,7 @@ and map_exp_annot_aux f = function
   | E_tuple xs -> E_tuple (List.map (map_exp_annot f) xs)
   | E_if (cond, t, e) -> E_if (map_exp_annot f cond, map_exp_annot f t, map_exp_annot f e)
   | E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4)
+  | E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2)
   | E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
   | E_vector_indexed (iexps, opt_default) ->
      E_vector_indexed (List.map (fun (i, exp) -> (i, map_exp_annot f exp)) iexps, map_opt_default_annot f opt_default)
@@ -297,6 +309,10 @@ let string_of_id = function
 let id_of_kid = function
   | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
+let kid_of_id = function
+  | Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l)
+  | Id_aux (DeIid v, _) -> assert false
+
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
@@ -461,6 +477,8 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord
      ^ ") { "
      ^ string_of_exp body
+  | E_loop (While, cond, body) -> "while " ^ string_of_exp cond ^ " do " ^ string_of_exp body
+  | E_loop (Until, cond, body) -> "repeat " ^ string_of_exp body ^ " until " ^ string_of_exp cond
   | 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
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 246e0ebd..33d65ede 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -60,6 +60,8 @@ val mk_funcl : id -> unit pat -> unit exp -> unit funcl
 val mk_fundef : (unit funcl) list -> unit def
 val mk_val_spec : val_spec_aux -> unit def
 val mk_typschm : typquant -> typ -> typschm
+val mk_qi_id : base_kind_aux -> kid -> quant_item
+val mk_qi_nc : n_constraint -> quant_item
 val mk_fexp : id -> unit exp -> unit fexp
 val mk_fexps : (unit fexp) list -> unit fexps
 val mk_letbind : unit pat -> unit exp -> unit letbind
@@ -94,6 +96,8 @@ val real_typ : typ
 val vector_typ : nexp -> nexp -> order -> typ -> typ
 val list_typ : typ -> typ
 val exc_typ : typ
+val tuple_typ : typ list -> typ
+val function_typ : typ -> typ -> effect -> typ
 
 val no_effect : effect
 val mk_effect : base_effect_aux list -> effect
@@ -120,6 +124,7 @@ 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
+val nc_set : kid -> int list -> n_constraint
 
 val quant_items : typquant -> quant_item list
 
@@ -164,6 +169,7 @@ val string_of_index_range : index_range -> string
 val id_of_fundef : 'a fundef -> id
 
 val id_of_kid : kid -> id
+val kid_of_id : id -> kid
 
 val prepend_id : string -> id -> id
 
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 5c539354..8e04bd30 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -170,6 +170,35 @@ let rec foreachM_dec (i,stop,by) vars body =
     foreachM_dec (i - by,stop,by) vars body
   else return vars
 
+val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while_PP is_while vars cond body =
+  if (cond vars = is_while)
+  then while_PP is_while (body vars) cond body
+  else vars
+
+val while_PM : forall 'vars 'r. bool -> 'vars -> ('vars -> bool) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec while_PM is_while vars cond body =
+  if (cond vars = is_while)
+  then body vars >>= fun vars -> while_PM is_while vars cond body
+  else return vars
+
+val while_MP : forall 'vars 'r. bool -> 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> 'vars) -> MR 'vars 'r
+let rec while_MP is_while vars cond body =
+  cond vars >>= fun continue ->
+  if (continue = is_while)
+  then while_MP is_while (body vars) cond body
+  else return vars
+
+val while_MM : forall 'vars 'r. bool -> 'vars -> ('vars -> MR bool 'r) ->
+                ('vars -> MR 'vars 'r) -> MR 'vars 'r
+let rec while_MM is_while vars cond body =
+  cond vars >>= fun continue ->
+  if (continue = is_while)
+  then body vars >>= fun vars -> while_MM is_while vars cond body
+  else return vars
+
 let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 0ea65551..fa6515fb 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -203,6 +203,35 @@ let rec foreachM_dec (i,stop,by) vars body =
     foreachM_dec (i - by,stop,by) vars body
   else return vars
 
+val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
+let rec while_PP is_while vars cond body =
+  if (cond vars = is_while)
+  then while_PP is_while (body vars) cond body
+  else vars
+
+val while_PM : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> bool) ->
+                ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+let rec while_PM is_while vars cond body =
+  if (cond vars = is_while)
+  then body vars >>= fun vars -> while_PM is_while vars cond body
+  else return vars
+
+val while_MP : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> ME 'regs bool 'e) ->
+                ('vars -> 'vars) -> ME 'regs 'vars 'e
+let rec while_MP is_while vars cond body =
+  cond vars >>= fun continue ->
+  if (continue = is_while)
+  then while_MP is_while (body vars) cond body
+  else return vars
+
+val while_MM : forall 'regs 'vars 'e. bool -> 'vars -> ('vars -> ME 'regs bool 'e) ->
+                ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
+let rec while_MM is_while vars cond body =
+  cond vars >>= fun continue ->
+  if (continue = is_while)
+  then body vars >>= fun vars -> while_MM is_while vars cond body
+  else return vars
+
 (*let write_two_regs r1 r2 bvec state =
   let vec = bvec_to_vec bvec in
   let is_inc =
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1f7840d0..83c79646 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -469,7 +469,9 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3)
     | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
       E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2,
-	    to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
+            to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
+    | Parse_ast.E_loop(Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
+    | Parse_ast.E_loop(Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
     | Parse_ast.E_vector(exps) -> 
       (match to_ast_iexps false k_env def_ord exps with
 	| Some([]) -> E_vector([])
diff --git a/src/lexer.mll b/src/lexer.mll
index cf3c9baf..fb091f67 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -112,6 +112,10 @@ let kw_table =
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
      ("when",                    (fun x -> When));
+     ("repeat",                  (fun x -> Repeat));
+     ("until",                   (fun x -> Until));
+     ("while",                   (fun x -> While));
+     ("do",                      (fun x -> Do));
      ("val",                     (fun x -> Val));
 
      ("div",			 (fun x -> Div_));
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 2509f8ef..1e2c8bc6 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -137,6 +137,15 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      separate space [string "let"; ocaml_atomic_lexp ctx lexp;
                      equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
      ^/^ ocaml_exp ctx exp2
+  | E_loop (While, cond, body) ->
+     let loop_body =
+       separate space [string "if"; ocaml_atomic_exp ctx cond;
+                       string "then"; parens (ocaml_atomic_exp ctx body ^^ semi ^^ space ^^ string "loop ()");
+                       string "else ()"]
+     in
+     (string "let rec loop () =" ^//^ loop_body)
+     ^/^ string "in"
+     ^/^ string "loop ()"
   | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
   | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
 and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b259611d..6424d682 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -253,6 +253,7 @@ and fpat_aux =  (* Field pattern *)
 and fpat = 
    FP_aux of fpat_aux * l
 
+type loop = While | Until
 
 type 
 exp_aux =  (* Expression *)
@@ -265,6 +266,7 @@ exp_aux =  (* Expression *)
  | E_app_infix of exp * id * exp (* infix function application *)
  | E_tuple of (exp) list (* tuple *)
  | E_if of exp * exp * exp (* conditional *)
+ | E_loop of loop * exp * exp
  | E_for of id * exp * exp * exp * atyp * exp (* loop *)
  | E_vector of (exp) list (* vector (indexed from 0) *)
  | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *)
diff --git a/src/parser.mly b/src/parser.mly
index 5413ac0d..0c3dbb03 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,6 +133,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %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
+%token While Do Repeat Until
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -689,6 +690,8 @@ right_atomic_exp:
         then ATyp_aux(ATyp_inc,(locn 6 6))
         else ATyp_aux(ATyp_dec,(locn 6 6)) in
       eloc (E_for($3,$5,$7,step,ord,$9)) }
+  | While exp Do exp
+    { eloc (E_loop (While, $2, $4)) }
   | letbind In exp
     { eloc (E_let($1,$3)) }
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1bfb19aa..f981297d 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -514,6 +514,26 @@ let doc_exp_lem, doc_let_lem =
                    (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
                 )
             )
+       | Id_aux ((Id (("while_PP" | "while_PM" |
+                       "while_MP" | "while_MM" ) as loopf),_)) ->
+          let [is_while;cond;body;e5] = args in
+          let varspp = match e5 with
+            | E_aux (E_tuple vars,_) ->
+               let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+               begin match vars with
+               | [v] -> v
+               | _ -> parens (separate comma vars) end
+            | E_aux (E_id (Id_aux (Id name,_)),_) ->
+               string name
+            | E_aux (E_lit (L_aux (L_unit,_)),_) ->
+               string "_" in
+          parens (
+              (prefix 2 1)
+                ((separate space) [string loopf;expY is_while;expY e5])
+                ((prefix 0 1)
+                  (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN cond)))
+                  (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN body))))
+            )
        (* | Id_aux (Id "append",_) ->
           let [e1;e2] = args in
           let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 2bd5d5bc..e552dca4 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -99,9 +99,16 @@ let rec skip_lines in_chan = function
   | n when n <= 0 -> ()
   | n -> input_line in_chan; skip_lines in_chan (n - 1)
 
+let rec read_lines in_chan = function
+  | n when n <= 0 -> []
+  | n ->
+     let l = input_line in_chan in
+     let ls = read_lines in_chan (n - 1) in
+     l :: ls
+
 let termcode n = "\x1B[" ^ string_of_int n ^ "m"
 
-let print_code ff fname lnum1 cnum1 cnum2 =
+let print_code1 ff fname lnum1 cnum1 cnum2 =
   try
     let in_chan = open_in fname in
     begin
@@ -119,6 +126,31 @@ let print_code ff fname lnum1 cnum1 cnum2 =
     end
   with _ -> ()
 
+let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
+  try
+    let in_chan = open_in fname in
+    begin
+      try
+        skip_lines in_chan (lnum1 - 1);
+        let line = input_line in_chan in
+        Format.fprintf ff "%s%s%s%s\n"
+                       (Str.string_before line cnum1)
+                       (termcode 41)
+                       (Str.string_after line cnum1)
+                       (termcode 49);
+        let lines = read_lines in_chan (lnum2 - lnum1 - 1) in
+        List.iter (fun l -> Format.fprintf ff "%s%s%s\n" (termcode 41) l (termcode 49)) lines;
+        let line = input_line in_chan in
+        Format.fprintf ff "%s%s%s%s"
+                       (termcode 41)
+                       (Str.string_before line cnum2)
+                       (termcode 49)
+                       (Str.string_after line cnum2);
+        close_in in_chan
+      with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e))
+    end
+  with _ -> ()
+
 let format_pos2 ff p1 p2 =
   let open Lexing in
   begin
@@ -126,7 +158,9 @@ let format_pos2 ff p1 p2 =
                    p1.pos_fname
                    p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
                    p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
-    print_code ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol);
+    if p1.pos_lnum == p2.pos_lnum
+    then print_code1 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol)
+    else print_code2 ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
     Format.pp_print_flush ff ()
   end
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index fed8408d..5cf1a6b9 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -130,6 +130,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
       union_effects (fun_app_effects f env) (union_eff_exps [e1;e2])
     | E_if (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
     | E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4]
+    | E_loop (_,e1,e2) -> union_eff_exps [e1;e2]
     | E_vector es -> union_eff_exps es
     | E_vector_indexed (ies,opt_default) ->
        let (_,es) = List.split ies in
@@ -388,6 +389,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
   | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e))
   | E_for (id, e1, e2, e3, o, body) ->
     rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
+  | E_loop (loop, e1, e2) ->
+    rewrap (E_loop (loop, rewrite e1, rewrite e2))
   | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
   | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
     let def = match default with
@@ -698,6 +701,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_tuple                  : 'exp list -> 'exp_aux
   ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
   ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
+  ; e_loop                   : loop * 'exp * 'exp -> 'exp_aux
   ; e_vector                 : 'exp list -> 'exp_aux
   ; e_vector_indexed         : (int * 'exp) list * 'opt_default -> 'exp_aux
   ; e_vector_access          : 'exp * 'exp -> 'exp_aux
@@ -763,6 +767,8 @@ let rec fold_exp_aux alg = function
   | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
   | E_for (id,e1,e2,e3,order,e4) ->
      alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4)
+  | E_loop (loop_type, e1, e2) ->
+     alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2)
   | E_vector es -> alg.e_vector (List.map (fold_exp alg) es)
   | E_vector_indexed (es,opt) ->
      alg.e_vector_indexed (List.map (fun (id,e) -> (id,fold_exp alg e)) es, fold_opt_default alg opt)
@@ -840,6 +846,7 @@ let id_exp_alg =
   ; e_tuple = (fun es -> E_tuple es)
   ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3))
   ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4))
+  ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2))
   ; e_vector = (fun es -> E_vector es)
   ; e_vector_indexed = (fun (es,opt2) -> E_vector_indexed (es,opt2))
   ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2))
@@ -937,6 +944,8 @@ let compute_exp_alg bot join =
   ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3)))
   ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) ->
     (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4)))
+  ; e_loop = (fun (lt, (v1, e1), (v2, e2)) ->
+    (join_list [v1;v2], E_loop (lt, e1, e2)))
   ; e_vector = split_join (fun es -> E_vector es)
   ; e_vector_indexed = (fun (es,(v2,opt2)) ->
     let (is,es) = List.split es in
@@ -1177,6 +1186,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es'))
     ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3')))
     ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4')))
+    ; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2')))
     ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es'))
     ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2')))
     ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2')))
@@ -2840,6 +2850,10 @@ let rewrite_defs_letbind_effects  =
        n_exp_name by (fun by ->
        let body = n_exp_term (effectful body) body in
        k (rewrap (E_for (id,start,stop,by,dir,body))))))
+    | E_loop (loop, cond, body) ->
+       let cond = n_exp_term (effectful cond) cond in
+       let body = n_exp_term (effectful body) body in
+       k (rewrap (E_loop (loop,cond,body)))
     | E_vector exps ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_vector exps)))
@@ -3164,6 +3178,29 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          else P_aux (P_tup [pat; mktup_pat pl vars],
                      simple_annot pl (typ_of v)) in
        Added_vars (v,pat)
+     | E_loop(loop,cond,body) ->
+        let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in
+        let vartuple = mktup el vars in
+        (* let cond = rewrite_var_updates (add_vars false cond vartuple) in *)
+        let body = rewrite_var_updates (add_vars overwrite body vartuple) in
+        let (E_aux (_,(_,bannot))) = body in
+        let fname = match effectful cond, effectful body with
+          | false, false -> "while_PP"
+          | false, true  -> "while_PM"
+          | true,  false -> "while_MP"
+          | true,  true  -> "while_MM" in
+        let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+        let is_while =
+          match loop with
+          | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ)
+          | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in
+        let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]),
+                       (Parse_ast.Generated el, bannot)) in
+        let pat =
+          if overwrite then mktup_pat el vars
+          else P_aux (P_tup [pat; mktup_pat pl vars],
+                      simple_annot pl (typ_of v)) in
+        Added_vars (v,pat)
     | E_if (c,e1,e2) ->
        let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t)))
                            (dedup eqidtyp (find_updated_vars e1 @ find_updated_vars e2)) in
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 010f1003..11394ec6 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -97,6 +97,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_tuple                  : 'exp list -> 'exp_aux
  ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
  ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
+ ; e_loop                   : loop * 'exp * 'exp -> 'exp_aux
  ; e_vector                 : 'exp list -> 'exp_aux
  ; e_vector_indexed         : (int * 'exp) list * 'opt_default -> 'exp_aux
  ; e_vector_access          : 'exp * 'exp -> 'exp_aux
diff --git a/src/type_check.ml b/src/type_check.ml
index f952d0d6..5a98704c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -68,9 +68,11 @@ let typ_warning m = prerr_endline ("Warning: " ^ m)
 type type_error =
   (* First parameter is the error that caused us to start doing type
      coercions, the second is the errors encountered by all possible
-     coerctions *)
+     coercions *)
   | Err_no_casts of type_error * type_error list
+  | Err_unresolved_quants of id * quant_item list
   | Err_subtype of typ * typ * n_constraint list
+  | Err_no_num_ident of id
   | Err_other of string
 
 let pp_type_error err =
@@ -91,6 +93,8 @@ let pp_type_error err =
                         string (string_of_typ typ2) ]
        ^/^ string "in context"
        ^//^ string (string_of_list ", " string_of_n_constraint constrs)
+    | Err_no_num_ident id ->
+       string "No num identifier" ^^ space ^^ string (string_of_id id)
     | Err_other str -> string str
   in
   pp_err err
@@ -769,7 +773,7 @@ end = struct
 
   let get_num_def id env =
     try Bindings.find id env.num_defs with
-    | Not_found -> typ_error (id_loc id) ("No Num identifier " ^ string_of_id id)
+    | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id)
 
   let rec wf_constraint env (NC_aux (nc, _)) =
     match nc with
@@ -2371,6 +2375,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
      end
   | LEXP_tup lexps ->
      begin
+       let typ = Env.expand_synonyms env typ in
        let (Typ_aux (typ_aux, _)) = typ in
        match typ_aux with
        | Typ_tup typs ->
@@ -2382,7 +2387,23 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
             | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length"
           in
           annot_lexp (LEXP_tup tlexps) typ, env
-       | _ -> typ_error l "Cannot bind tuple l-expression against non tuple type"
+       (* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *)
+       | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 ->
+          begin
+            match destruct_vector env typ with
+            | Some (_, vec_len, _, _) ->
+               let bind_bit_tuple lexp (tlexps, env) =
+                 let tlexp, env = bind_lexp env lexp (lvector_typ env (nconstant 1) bit_typ) in
+                 tlexp :: tlexps, env
+               in
+               if prove env (nc_eq vec_len (nconstant (List.length lexps)))
+               then
+                 let (tlexps, env) = List.fold_right bind_bit_tuple lexps ([], env) in
+                 annot_lexp (LEXP_tup tlexps) typ, env
+               else typ_error l "Vector and tuple length must be the same in assignment"
+            | None -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
+          end
+       | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
      end
   | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) ->
      begin
@@ -2538,6 +2559,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      in
      try_overload (Env.get_overloads f env)
   | E_app (f, xs) -> infer_funapp l env f xs None
+  | E_loop (loop_type, cond, body) ->
+     let checked_cond = crule check_exp env cond bool_typ in
+     let checked_body = crule check_exp env body unit_typ in
+     annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ
   | E_for (v, f, t, step, ord, body) ->
      begin
        let f, t = match ord with
@@ -2836,6 +2861,11 @@ and propagate_exp_effect_aux = function
      let p_body = propagate_exp_effect body in
      E_for (v, p_f, p_t, p_step, ord, p_body),
      collect_effects [p_f; p_t; p_step; p_body]
+  | E_loop (loop_type, cond, body) ->
+     let p_cond = propagate_exp_effect cond in
+     let p_body = propagate_exp_effect body in
+     E_loop (loop_type, p_cond, p_body),
+     union_effects (effect_of p_cond) (effect_of p_body)
   | E_let (letbind, exp) ->
      let p_lb, eff = propagate_letbind_effect letbind in
      let p_exp = propagate_exp_effect exp in
diff --git a/src/type_check.mli b/src/type_check.mli
index e5279067..838cab7d 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -47,10 +47,17 @@ open Ast_util
 val opt_tc_debug : int ref
 val opt_no_effects : bool ref
 
-type type_error
+type type_error =
+  | Err_no_casts of type_error * type_error list
+  | Err_unresolved_quants of id * quant_item list
+  | Err_subtype of typ * typ * n_constraint list
+  | Err_no_num_ident of id
+  | Err_other of string
 
 exception Type_error of l * type_error;;
 
+val string_of_type_error : type_error -> string
+
 type mut = Immutable | Mutable
 
 type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
@@ -251,4 +258,8 @@ Some invariants that will hold of a fully checked AST are:
    for them to have type annotations. *)
 val check : Env.t -> 'a defs -> tannot defs * Env.t
 
+(* Like check but throws type_errors rather than Sail generic errors
+   from Reporting_basic. *)
+val check' : Env.t -> 'a defs -> tannot defs * Env.t
+
 val initial_env : Env.t