Flow typing and l-expression changes for ASL parser

1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.

2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.

The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.

3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.

4. Include a newly generated version of aarch64_no_vector

5. Update the Ocaml test suite to use builtins in lib/

12 files changed, 228 insertions, 179 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 2f2d27d8..f7574b9d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -449,6 +449,7 @@ and map_lexp_annot_aux f = function
   | LEXP_memory (id, exps) -> LEXP_memory (id, List.map (map_exp_annot f) exps)
   | LEXP_cast (typ, id) -> LEXP_cast (typ, id)
   | LEXP_tup lexps -> LEXP_tup (List.map (map_lexp_annot f) lexps)
+  | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (map_lexp_annot f) lexps)
   | LEXP_vector (lexp, exp) -> LEXP_vector (map_lexp_annot f lexp, map_exp_annot f exp)
   | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (map_lexp_annot f lexp, map_exp_annot f exp1, map_exp_annot f exp2)
   | LEXP_field (lexp, id) -> LEXP_field (map_lexp_annot f lexp, id)
@@ -645,8 +646,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | 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
+  | E_assign (lexp, bind) -> string_of_lexp lexp ^ " = " ^ string_of_exp bind
+  | E_cast (typ, exp) -> string_of_exp exp ^ " : " ^ string_of_typ typ
   | E_vector vec -> "[" ^ string_of_list ", " string_of_exp vec ^ "]"
   | E_vector_access (v, n) -> string_of_exp v ^ "[" ^ string_of_exp n ^ "]"
   | E_vector_update (v, n, exp) -> "[" ^ string_of_exp v ^ " with " ^ string_of_exp n ^ " = " ^ string_of_exp exp ^ "]"
@@ -702,7 +703,7 @@ and string_of_pat (P_aux (pat, l)) =
   | P_wild -> "_"
   | P_id v -> string_of_id v
   | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat
-  | P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
+  | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ
   | 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 ^ ")"
   | P_cons (pat1, pat2) -> string_of_pat pat1 ^ " :: " ^ string_of_pat pat2
@@ -719,7 +720,9 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
   | LEXP_tup lexps -> "(" ^ string_of_list ", " string_of_lexp lexps ^ ")"
   | LEXP_vector (lexp, exp) -> string_of_lexp lexp ^ "[" ^ string_of_exp exp ^ "]"
   | LEXP_vector_range (lexp, exp1, exp2) ->
-     string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ ".." ^ string_of_exp exp2 ^ "]"
+     string_of_lexp lexp ^ "[" ^ string_of_exp exp1 ^ " .. " ^ string_of_exp exp2 ^ "]"
+  | LEXP_vector_concat lexps ->
+     string_of_list " @ " string_of_lexp lexps
   | LEXP_field (lexp, id) -> string_of_lexp lexp ^ "." ^ string_of_id id
   | LEXP_memory (f, xs) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"
 and string_of_letbind (LB_aux (lb, l)) =
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 62c1af02..1ba1b9e6 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -539,35 +539,45 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     ), (l,()))
 
 and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp =
-  LEXP_aux(
-    (match exp with
-     | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
-     | Parse_ast.E_deref(exp) -> LEXP_deref(to_ast_exp k_env def_ord exp)
-     | Parse_ast.E_cast(typ,Parse_ast.E_aux(Parse_ast.E_id(id),l')) ->
-       LEXP_cast(to_ast_typ k_env def_ord typ, to_ast_id id)
-     | Parse_ast.E_tuple(tups) ->
+  let lexp = match exp with
+    | Parse_ast.E_id id -> LEXP_id (to_ast_id id)
+    | Parse_ast.E_deref exp -> LEXP_deref (to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_cast (typ, Parse_ast.E_aux (Parse_ast.E_id id, l')) ->
+       LEXP_cast (to_ast_typ k_env def_ord typ, to_ast_id id)
+    | Parse_ast.E_tuple tups ->
        let ltups = List.map (to_ast_lexp k_env def_ord) tups in
-       let is_ok_in_tup (LEXP_aux (le,(l,_))) =
+       let is_ok_in_tup (LEXP_aux (le, (l, _))) =
          match le with
-         | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
+         | LEXP_id _ | LEXP_cast _ | LEXP_vector _ | LEXP_vector_concat _ | LEXP_field _ | LEXP_vector_range _ | LEXP_tup _ -> ()
          | LEXP_memory _ | LEXP_deref _ ->
-           typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None in
+            typ_error l "only identifiers, fields, and vectors may be set in a tuple" None None None
+       in
        List.iter is_ok_in_tup ltups;
-       LEXP_tup(ltups)
-    | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) ->
-      (match f with
-      | Parse_ast.Id(id) ->
-	(match List.map (to_ast_exp k_env def_ord) args with
-          | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[])
-	  | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps)
-	  | args -> LEXP_memory(to_ast_id f', args))
-      | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
-    | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
-    | Parse_ast.E_vector_subrange(vexp,exp1,exp2) ->
-      LEXP_vector_range(to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
-    | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env def_ord fexp, to_ast_id id)
-    | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
-      , (l,()))
+       LEXP_tup ltups
+    | Parse_ast.E_app ((Parse_ast.Id_aux (f, l') as f'), args) ->
+       begin match f with
+       | Parse_ast.Id(id) ->
+          (match List.map (to_ast_exp k_env def_ord) args with
+           | [E_aux (E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory (to_ast_id f', [])
+           | [E_aux (E_tuple exps,_)] -> LEXP_memory (to_ast_id f', exps)
+           | args -> LEXP_memory(to_ast_id f', args))
+       | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None
+       end
+    | Parse_ast.E_vector_append (exp1, exp2) ->
+       LEXP_vector_concat (to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2)
+    | Parse_ast.E_vector_access (vexp, exp) -> LEXP_vector (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_vector_subrange (vexp, exp1, exp2) ->
+       LEXP_vector_range (to_ast_lexp k_env def_ord vexp, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
+    | Parse_ast.E_field (fexp, id) -> LEXP_field (to_ast_lexp k_env def_ord fexp, to_ast_id id)
+    | _ -> typ_error l "Only identifiers, cast identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None
+  in
+  LEXP_aux (lexp, (l, ()))
+
+and to_ast_lexp_vector_concat k_env def_ord (Parse_ast.E_aux (exp_aux, l) as exp) =
+  match exp_aux with
+  | Parse_ast.E_vector_append (exp1, exp2) ->
+     to_ast_lexp k_env def_ord exp1 :: to_ast_lexp_vector_concat k_env def_ord exp2
+  | _ -> [to_ast_lexp k_env def_ord exp]
 
 and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : unit pexp =
   match pex with
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 87439e83..e62fcfc3 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -505,6 +505,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
      else
        puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp
   | E_assign (LEXP_aux (LEXP_tup lexps, annot), exp) -> failwith "Tuple assignment"
+  | E_assign (LEXP_aux (LEXP_vector_concat lexps, annot), exp) -> failwith "Vector concat assignment"
      (*
      let values = coerce_tuple (value_of_exp exp) in
      wrap (E_block (List.map2 (fun lexp v -> E_aux (E_assign (lexp, exp_of_value v), (Parse_ast.Unknown, None))) lexps values))
@@ -556,6 +557,9 @@ and exp_of_lexp (LEXP_aux (lexp_aux, _) as lexp) =
   | LEXP_tup lexps -> mk_exp (E_tuple (List.map exp_of_lexp lexps))
   | LEXP_vector (lexp, exp) -> mk_exp (E_vector_access (exp_of_lexp lexp, exp))
   | LEXP_vector_range (lexp, exp1, exp2) -> mk_exp (E_vector_subrange (exp_of_lexp lexp, exp1, exp2))
+  | LEXP_vector_concat [] -> failwith "Empty LEXP_vector_concat node in exp_of_lexp"
+  | LEXP_vector_concat [lexp] -> exp_of_lexp lexp
+  | LEXP_vector_concat (lexp :: lexps) -> mk_exp (E_vector_append (exp_of_lexp lexp, exp_of_lexp (mk_lexp (LEXP_vector_concat lexps))))
   | LEXP_field (lexp, id) -> mk_exp (E_field (exp_of_lexp lexp, id))
 
 and pattern_match env (P_aux (p_aux, _) as pat) value =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 826d8eb1..55ed57d2 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -517,6 +517,7 @@ lexp_aux =  (* lvalue expression, can't occur out of the parser *)
  | LEXP_mem of id * (exp) list
  | LEXP_vector of lexp * exp (* vector element *)
  | LEXP_vector_range of lexp * exp * exp (* subvector *)
+ | LEXP_vector_concat of lexp list
  | LEXP_field of lexp * id (* struct field *)
 
 and lexp = 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index c0658a83..5a26cb42 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -418,6 +418,7 @@ and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
   | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
   | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
   | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2])
+  | LEXP_vector_concat lexps -> parens (separate_map (string " @ ") doc_lexp lexps)
   | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
   | _ -> parens (doc_lexp lexp)
 and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 203e8a58..82e3ab05 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -197,6 +197,8 @@ let fix_eff_lexp (LEXP_aux (lexp,((l,_) as annot))) = match snd annot with
     | LEXP_memory (_,es) -> union_eff_exps es
     | LEXP_tup les ->
       List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les
+    | LEXP_vector_concat les ->
+      List.fold_left (fun eff le -> union_effects eff (effect_of_lexp le)) no_effect les
     | LEXP_vector (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
     | LEXP_vector_range (lexp,e1,e2) ->
       union_effects (effect_of_lexp lexp)
@@ -384,6 +386,7 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
     rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters lexp,
                                rewriters.rewrite_exp rewriters exp1,
                                rewriters.rewrite_exp rewriters exp2))
+  | LEXP_vector_concat lexps -> rewrap (LEXP_vector_concat (List.map (rewriters.rewrite_lexp rewriters) lexps))
   | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters lexp,id))
 
 let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = 
@@ -556,6 +559,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; lEXP_tup                 : 'lexp list -> 'lexp_aux
   ; lEXP_vector              : 'lexp * 'exp -> 'lexp_aux
   ; lEXP_vector_range        : 'lexp * 'exp * 'exp -> 'lexp_aux
+  ; lEXP_vector_concat       : 'lexp list -> 'lexp_aux
   ; lEXP_field               : 'lexp * id -> 'lexp_aux
   ; lEXP_aux                 : 'lexp_aux * 'a annot -> 'lexp
   ; fE_Fexp                  : id * 'exp -> 'fexp_aux
@@ -635,7 +639,8 @@ and fold_lexp_aux alg = function
   | LEXP_vector (lexp,e) -> alg.lEXP_vector (fold_lexp alg lexp, fold_exp alg e)
   | LEXP_vector_range (lexp,e1,e2) ->
      alg.lEXP_vector_range (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2)
- | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id)
+  | LEXP_vector_concat les -> alg.lEXP_vector_concat (List.map (fold_lexp alg) les)
+  | LEXP_field (lexp,id) -> alg.lEXP_field (fold_lexp alg lexp, id)
 and fold_lexp alg (LEXP_aux (lexp_aux,annot)) =
   alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot)
 and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e)
@@ -706,6 +711,7 @@ let id_exp_alg =
   ; lEXP_tup = (fun tups -> LEXP_tup tups)
   ; lEXP_vector = (fun (lexp,e2) -> LEXP_vector (lexp,e2))
   ; lEXP_vector_range = (fun (lexp,e2,e3) -> LEXP_vector_range (lexp,e2,e3))
+  ; lEXP_vector_concat = (fun lexps -> LEXP_vector_concat lexps)
   ; lEXP_field = (fun (lexp,id) -> LEXP_field (lexp,id))
   ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot))
   ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e))
@@ -813,6 +819,9 @@ let compute_exp_alg bot join =
   ; lEXP_vector = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, LEXP_vector (lexp,e2)))
   ; lEXP_vector_range = (fun ((vl,lexp),(v2,e2),(v3,e3)) ->
     (join_list [vl;v2;v3], LEXP_vector_range (lexp,e2,e3)))
+  ; lEXP_vector_concat = (fun ls ->
+    let (vs,ls) = List.split ls in
+    (join_list vs, LEXP_vector_concat ls))
   ; lEXP_field = (fun ((vl,lexp),id) -> (vl, LEXP_field (lexp,id)))
   ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot)))
   ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e)))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index f8982d69..ccc1f951 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -155,6 +155,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; lEXP_tup                 : 'lexp list -> 'lexp_aux
  ; lEXP_vector              : 'lexp * 'exp -> 'lexp_aux
  ; lEXP_vector_range        : 'lexp * 'exp * 'exp -> 'lexp_aux
+ ; lEXP_vector_concat       : 'lexp list -> 'lexp_aux
  ; lEXP_field               : 'lexp * id -> 'lexp_aux
  ; lEXP_aux                 : 'lexp_aux * 'a annot -> 'lexp
  ; fE_Fexp                  : id * 'exp -> 'fexp_aux
@@ -167,7 +168,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; pat_exp                  : 'pat * 'exp -> 'pexp_aux
  ; pat_when                 : 'pat * 'exp * 'exp -> 'pexp_aux
  ; pat_aux                  : 'pexp_aux * 'a annot -> 'pexp
- ; lB_val          : 'pat * 'exp -> 'letbind_aux
+ ; lB_val                   : 'pat * 'exp -> 'letbind_aux
  ; lB_aux                   : 'letbind_aux * 'a annot -> 'letbind
  ; pat_alg                  : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
  }
diff --git a/src/rewrites.ml b/src/rewrites.ml
index cfeae1e3..a61f2622 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -127,7 +127,7 @@ let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_local_var id env
-  | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
+  | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
   | LEXP_vector (lexp,_)
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local lexp env
@@ -136,7 +136,7 @@ let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
   | LEXP_memory _ | LEXP_deref _ -> false
   | LEXP_id id
   | LEXP_cast (_, id) -> id_is_unbound id env
-  | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
+  | LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
   | LEXP_vector (lexp,_)
   | LEXP_vector_range (lexp,_,_)
   | LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
@@ -281,7 +281,7 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
        scope. *)
     | Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
        let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
-       Some (E_aux (E_app (mk_id "add_range", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
+       Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, Some (env, atom_typ (nsum size (nint 1)), no_effect))))
     | _ ->
        begin
          match destruct_vector env typ with
@@ -293,12 +293,12 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
   let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) =
     match nexp_aux with
     | Nexp_sum (n1, n2) ->
-       mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2]))
+       mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2]))
     | Nexp_minus (n1, n2) ->
-       mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2]))
+       mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2]))
     | Nexp_times (n1, n2) ->
-       mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2]))
-    | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp]))
+       mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2]))
+    | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp]))
     | _ -> mk_exp (E_sizeof nexp)
   in
   let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
@@ -487,6 +487,7 @@ let rewrite_sizeof (Defs defs) =
     ; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
     ; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2')))
     ; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3')))
+    ; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps'))
     ; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id)))
     ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot)))
     ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e')))
@@ -2281,11 +2282,11 @@ let rewrite_simple_types (Defs defs) =
   let defs = Defs (List.map simple_def defs) in
   rewrite_defs_base simple_defs defs
 
-let rewrite_tuple_vector_assignments defs =
+let rewrite_vector_concat_assignments defs =
   let assign_tuple e_aux annot =
     let env = env_of_annot annot in
     match e_aux with
-    | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) ->
+    | E_assign (LEXP_aux (LEXP_vector_concat lexps, lannot), exp) ->
        let typ = Env.base_typ_of env (typ_of exp) in
        if is_vector_typ typ then
          (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *)
@@ -2518,8 +2519,11 @@ let rewrite_defs_letbind_effects =
     | LEXP_vector_range (lexp,e1,e2) ->
        n_lexp lexp (fun lexp ->
        n_exp_name e1 (fun e1 ->
-    n_exp_name e2 (fun e2 ->
+       n_exp_name e2 (fun e2 ->
        k (fix_eff_lexp (LEXP_aux (LEXP_vector_range (lexp,e1,e2),annot))))))
+    | LEXP_vector_concat es ->
+       n_lexpL es (fun es ->
+       k (fix_eff_lexp (LEXP_aux (LEXP_vector_concat es,annot))))
     | LEXP_field (lexp,id) ->
        n_lexp lexp (fun lexp ->
        k (fix_eff_lexp (LEXP_aux (LEXP_field (lexp,id),annot))))
@@ -3198,7 +3202,7 @@ let merge_funcls (Defs defs) =
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem = [
-  ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+  ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3233,7 +3237,7 @@ let rewrite_defs_ocaml = [
     (* ("undefined", rewrite_undefined); *)
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
   ("pat_lits", rewrite_defs_pat_lits);
-  ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+  ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3252,7 +3256,7 @@ let rewrite_defs_ocaml = [
 let rewrite_defs_c = [
   ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
   ("pat_lits", rewrite_defs_pat_lits);
-  ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+  ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
@@ -3268,7 +3272,7 @@ let rewrite_defs_c = [
 
 let rewrite_defs_interpreter = [
     ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
-    ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+    ("vector_concat_assignments", rewrite_vector_concat_assignments);
     ("tuple_assignments", rewrite_tuple_assignments);
     ("simple_assignments", rewrite_simple_assignments);
     ("remove_vector_concat", rewrite_defs_remove_vector_concat);
diff --git a/src/sail.ml b/src/sail.ml
index 4d32fb94..f459d774 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -157,6 +157,9 @@ let options = Arg.align ([
   ( "-enum_casts",
     Arg.Set Initial_check.opt_enum_casts,
     " allow enumerations to be automatically casted to numeric range types");
+  ( "-no_lexp_bounds_check",
+    Arg.Set Type_check.opt_no_lexp_bounds_check,
+    " turn off bounds checking for vector assignments in l-expressions");
   ( "-no_effects",
     Arg.Set Type_check.opt_no_effects,
     " (experimental) turn off effect checking");
diff --git a/src/type_check.ml b/src/type_check.ml
index de4c22c3..65d07859 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -63,6 +63,10 @@ let opt_tc_debug = ref 0
    re-writer passes, so it should only be used for debugging. *)
 let opt_no_effects = ref false
 
+(* opt_no_lexp_bounds_check turns of the bounds checking in vector
+   assignments in l-expressions *)
+let opt_no_lexp_bounds_check = ref false
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -314,6 +318,7 @@ module Env : sig
   val add_union_id : id -> typquant * typ -> t -> t
   val add_flow : id -> (typ -> typ) -> t -> t
   val get_flow : id -> t -> typ -> typ
+  val remove_flow : id -> t -> t
   val is_register : id -> t -> bool
   val get_register : id -> t -> typ
   val add_register : id -> typ -> t -> t
@@ -346,7 +351,7 @@ module Env : sig
   val add_cast : id -> t -> t
   val allow_polymorphic_undefineds : t -> t
   val polymorphic_undefineds : t -> bool
-  val lookup_id : id -> t -> lvar
+  val lookup_id : ?raw:bool -> id -> t -> lvar
   val fresh_kid : ?kid:kid -> t -> kid
   val expand_synonyms : t -> typ -> typ
   val canonicalize : t -> typ -> typ
@@ -856,10 +861,12 @@ end = struct
     | Not_found -> fun typ -> typ
 
   let add_flow id f env =
-    begin
-      typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
-      { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
-    end
+    typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
+    { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
+
+  let remove_flow id env =
+    typ_print (lazy ("Removing flow constraints for " ^ string_of_id id));
+    { env with flow = Bindings.remove id env.flow }
 
   let is_register id env =
     Bindings.mem id env.registers
@@ -898,11 +905,11 @@ end = struct
 
   let get_locals env = env.locals
 
-  let lookup_id id env =
+  let lookup_id ?raw:(raw=false) id env =
     try
       let (mut, typ) = Bindings.find id env.locals in
       let flow = get_flow id env in
-      Local (mut, flow typ)
+      Local (mut, if raw then typ else flow typ)
     with
     | Not_found ->
        begin
@@ -943,12 +950,11 @@ end = struct
 
   let add_constraint (NC_aux (nc_aux, l) as constr) env =
     wf_constraint env constr;
-    begin
-      typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
-      match nc_aux with
-      | NC_true -> env
-      | _ -> { env with constraints = constr :: env.constraints }
-    end
+    match nc_aux with
+    | NC_true -> env
+    | _ ->
+       typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
+       { env with constraints = constr :: env.constraints }
 
   let get_ret_typ env = env.ret_typ
 
@@ -1095,6 +1101,12 @@ let destruct_numeric env typ =
      Some ([kid], nc_true, nvar kid)
   | _, _ -> None
 
+let bind_numeric l typ env =
+  match destruct_numeric env typ with
+  | Some (kids, nc, nexp) ->
+     nexp, add_existential kids nc env
+  | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric")
+
 (** Pull an (potentially)-existentially qualified type into the global
    typing environment **)
 let bind_existential typ env =
@@ -1224,7 +1236,7 @@ let prove_z3' env constr =
   | Constraint.Unknown -> typ_debug (lazy "unknown"); false
 
 let prove_z3 env nc =
-  typ_print (lazy ("Prove " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
+  typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
   prove_z3' env (fun var_of -> Constraint.negate (nc_constraint env var_of nc))
 
 let solve env nexp =
@@ -1743,7 +1755,10 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t
   match destruct_exist env typ1, unwrap_exist env (Env.canonicalize env typ2) with
   | Some (kids, nc, typ1), _ ->
      let env = add_existential kids nc env in subtyp l env typ1 typ2
+  (* | None, ([], _, typ2) ->
+     typ_error l (string_of_typ typ1 ^ " < " ^ string_of_typ typ2) *)
   | None, (kids, nc, typ2) ->
+     typ_debug (lazy "Subtype check with unification");
      let env = add_typ_vars kids env in
      let kids' = KidSet.elements (KidSet.diff (KidSet.of_list kids) (typ_frees typ2)) in
      let unifiers, existential_kids, existential_nc =
@@ -1913,6 +1928,10 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
 let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
+let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
+
+let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot)
+
 (* Flow typing *)
 
 let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with
@@ -2096,7 +2115,7 @@ let rec filter_casts env from_typ to_typ casts =
 
 let crule r env exp typ =
   incr depth;
-  typ_print (lazy ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
+  typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
   try
     let checked_exp = r env exp typ in
     decr depth; checked_exp
@@ -2107,7 +2126,7 @@ let irule r env exp =
   incr depth;
   try
     let inferred_exp = r env exp in
-    typ_print (lazy ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
+    typ_print (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
     decr depth;
     inferred_exp
   with
@@ -2695,7 +2714,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
      let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
      annot_assign tlexp checked_exp, env'
   | LEXP_id v when has_typ v env ->
-     begin match Env.lookup_id v env with
+     begin match Env.lookup_id ~raw:true v env with
      | Local (Mutable, vtyp) | Register vtyp ->
         let checked_exp = crule check_exp env exp vtyp in
         let tlexp, env' = bind_lexp env lexp (typ_of checked_exp) in
@@ -2708,9 +2727,26 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
      annot_assign tlexp inferred_exp, env'
 
 and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
+  typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^  " to " ^ string_of_typ typ));
   let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
   let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
   match lexp_aux with
+  | LEXP_cast (typ_annot, v) ->
+     begin match Env.lookup_id ~raw:true v env with
+       | Local (Immutable, _) | Enum _ ->
+          typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+       | Local (Mutable, vtyp) ->
+          subtyp l env typ typ_annot;
+          subtyp l env typ_annot vtyp;
+          annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+       | Register vtyp ->
+          subtyp l env typ typ_annot;
+          subtyp l env typ_annot vtyp;
+          annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env
+       | Unbound ->
+          subtyp l env typ typ_annot;
+          annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
+     end
   | LEXP_deref exp ->
      let inferred_exp = infer_exp env exp in
      begin match typ_of inferred_exp with
@@ -2719,39 +2755,16 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
      | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ vtyp, _)]), _) when string_of_id r = "register" ->
         subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
      | _ ->
-        typ_error l (string_of_typ typ  ^ " must be a ref or register type in (*" ^ string_of_exp exp ^ ")")
+        typ_error l (string_of_typ typ  ^ " must be a ref or register type in " ^ string_of_exp exp ^ ")")
      end
   | LEXP_id v ->
-     begin match Env.lookup_id v env with
+     begin match Env.lookup_id ~raw:true v env with
      | Local (Immutable, _) | Enum _ ->
         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
-     | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
+     | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env
      | Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
      | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
      end
-  | LEXP_cast (typ_annot, v) ->
-     begin
-       match Env.lookup_id v env with
-       | Local (Immutable, _) | Enum _ ->
-          typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
-       | Local (Mutable, vtyp) ->
-          begin
-            subtyp l env typ typ_annot;
-            subtyp l env typ_annot vtyp;
-            annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
-          end
-       | Register vtyp ->
-          begin
-            subtyp l env typ typ_annot;
-            subtyp l env typ_annot vtyp;
-            annot_lexp_effect (LEXP_cast (typ_annot, v)) typ (mk_effect [BE_wreg]), env
-          end
-       | Unbound ->
-          begin
-            subtyp l env typ typ_annot;
-            annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
-          end
-     end
   | LEXP_tup lexps ->
      begin
        let typ = Env.expand_synonyms env typ in
@@ -2766,99 +2779,85 @@ 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
-       (* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *)
-       (* Maybe this code can be made not horrible? *)
-       | Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 ->
-          begin
-            match destruct_vector env typ with
-            | Some (vec_len, _, _) ->
-               let bind_bits_tuple lexp (tlexps, env, llen) =
-                 match lexp with
-                 | LEXP_aux (LEXP_id v, _) ->
-                    begin
-                      match Env.lookup_id v env with
-                      | Local (Immutable, _) | Enum _ ->
-                         typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
-                      | Unbound ->
-                         typ_error l "Unbound variable in vector tuple assignment"
-                      | Local (Mutable, vtyp) | Register vtyp ->
-                         let llen' = match destruct_vector env vtyp with
-                           | Some (llen', _, _) -> llen'
-                           | None -> typ_error l "Variables in vector tuple assignment must be vectors"
-                         in
-                         let tlexp, env = bind_lexp env lexp vtyp in
-                         tlexp :: tlexps, env, nsum llen llen'
-                    end
-                 | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) ->
-                   (* FIXME: will only work for ASL *)
-                   let rec_id =
-                     match Env.lookup_id v env with
-                     | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
-                     | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
-                   in
-                   let typq, _, vtyp, _ = Env.get_accessor rec_id fid env in
-                   let llen' = match destruct_vector env vtyp with
-                     | Some (llen', _, _) -> llen'
-                     | None -> typ_error l "Variables in vector tuple assignment must be vectors"
-                   in
-                   let tlexp, env = bind_lexp env lexp vtyp in
-                   tlexp :: tlexps, env, nsum llen llen'
-                 | _ -> typ_error l "bit vector assignment must only contain identifiers"
-               in
-               let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nint 0) in
-               if prove env (nc_eq vec_len lexp_len)
-               then 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 ("Malformed vector type " ^ string_of_typ typ)
+       | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ)
+     end
+  | _ ->
+     let inferred_lexp = infer_lexp env lexp in
+     subtyp l env typ (lexp_typ_of inferred_lexp);
+     inferred_lexp, env
+
+and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
+  let annot_lexp_effect lexp typ eff = LEXP_aux (lexp, (l, Some (env, typ, eff))) in
+  let annot_lexp lexp typ = annot_lexp_effect lexp typ no_effect in
+  match lexp_aux with
+  | LEXP_id v ->
+     begin match Env.lookup_id v env with
+     | Local (Mutable, typ) -> annot_lexp (LEXP_id v) typ
+     (* Probably need to remove flows here *)
+     | Register typ -> annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg])
+     | Local (Immutable, _) | Enum _ ->
+        typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+     | Unbound ->
+        typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp)
+     end
+  | LEXP_vector_range (v_lexp, exp1, exp2) ->
+     begin
+       let inferred_v_lexp = infer_lexp env v_lexp in
+       let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+       match v_typ_aux with
+       | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+            when Id.compare id (mk_id "vector") = 0 ->
+          let inferred_exp1 = infer_exp env exp1 in
+          let inferred_exp2 = infer_exp env exp2 in
+          let nexp1, env = bind_numeric l (typ_of inferred_exp1) env in
+          let nexp2, env = bind_numeric l (typ_of inferred_exp2) env in
+          begin match ord with
+          | Ord_aux (Ord_inc, _) when !opt_no_lexp_bounds_check || prove env (nc_lteq nexp1 nexp2) ->
+             let len = nexp_simp (nsum (nminus nexp2 nexp1) (nint 1)) in
+             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+          | Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove env (nc_gteq nexp1 nexp2) ->
+             let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
+             annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
+          | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
           end
-       | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
+       | _ -> typ_error l "Cannot assign slice of non vector type"
      end
-  | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) ->
+  | LEXP_vector (v_lexp, exp) ->
      begin
-       let is_immutable, is_register, vtyp = match Env.lookup_id v env with
-         | Unbound -> typ_error l "Cannot assign to element of unbound vector"
-         | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Local (Immutable, vtyp) -> true, false, vtyp
-         | Local (Mutable, vtyp) -> false, false, vtyp
-         | Register vtyp -> false, true, vtyp
-       in
-       let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
-       let inferred_exp1, inferred_exp2 = match access with
-         | E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) -> inferred_exp1, inferred_exp2
-         | _ -> assert false
-       in
-       match typ_of access with
-       | _ when not is_immutable && is_register ->
-          subtyp l env typ (typ_of access);
-          annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
-       | _ when not is_immutable ->
-          subtyp l env typ (typ_of access);
-          annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env
-       | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp)
+       let inferred_v_lexp = infer_lexp env v_lexp in
+       let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+       match v_typ_aux with
+       | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+            when Id.compare id (mk_id "vector") = 0 ->
+          let inferred_exp = infer_exp env exp in
+          let nexp, env = bind_numeric l (typ_of inferred_exp) env in
+          if !opt_no_lexp_bounds_check || prove env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
+            annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
+          else
+            typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+       | _ -> typ_error l "Cannot assign vector element of non vector type"
      end
-  (* Not sure about this case... can the left lexp be anything other than an identifier? *)
-  | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
+  | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression"
+  | LEXP_vector_concat (v_lexp :: v_lexps) ->
      begin
-       let is_immutable, is_register, vtyp = match Env.lookup_id v env with
-         | Unbound -> typ_error l "Cannot assign to element of unbound vector"
-         | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
-         | Local (Immutable, vtyp) -> true, false, vtyp
-         | Local (Mutable, vtyp) -> false, false, vtyp
-         | Register vtyp -> false, true, vtyp
-       in
-       let access = infer_exp (Env.enable_casts env) (E_aux (E_app (mk_id "vector_access", [E_aux (E_id v, (l, ())); exp]), (l, ()))) in
-       let inferred_exp = match access with
-         | E_aux (E_app (_, [_; inferred_exp]), _) -> inferred_exp
-         | _ -> assert false
+       let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
+         match v_typ_aux with
+         | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+              when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord ->
+            typ_equality l env elem_typ first_elem_typ;
+            nsum acc len
+         | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order"
        in
-       match typ_of access with
-       | _ when not is_immutable && is_register ->
-          subtyp l env typ (typ_of access);
-          annot_lexp (LEXP_vector (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp)) typ, env
-       | _ when not is_immutable ->
-          subtyp l env typ (typ_of access);
-          annot_lexp (LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp)) typ, env
-       | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp)
+       let inferred_v_lexp = infer_lexp env v_lexp in
+       let inferred_v_lexps = List.map (infer_lexp env) v_lexps in
+       let (Typ_aux (v_typ_aux, _) as v_typ) = Env.expand_synonyms env (lexp_typ_of inferred_v_lexp) in
+       let v_typs = List.map (fun lexp -> Env.expand_synonyms env (lexp_typ_of lexp)) inferred_v_lexps in
+       match v_typ_aux with
+       | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp len, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)])
+            when Id.compare id (mk_id "vector") = 0 ->
+          let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in
+          annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ)
+       | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ)
      end
   | LEXP_field (LEXP_aux (LEXP_id v, _), fid) ->
      (* FIXME: will only work for ASL *)
@@ -2868,7 +2867,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
        | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
      in
      let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
-     annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg]), env
+     annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ (mk_effect [BE_wreg])
   | _ -> typ_error l ("Unhandled l-expression " ^ string_of_lexp lexp)
 
 and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
@@ -2951,7 +2950,8 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
   | 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
+     let flows, constrs = infer_flow env checked_cond in
+     let checked_body = crule check_exp (add_flows true flows 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
@@ -3485,6 +3485,9 @@ and propagate_lexp_effect_aux = function
      let p_exp2 = propagate_exp_effect exp2 in
      LEXP_vector_range (p_lexp, p_exp1, p_exp2),
      union_effects (collect_effects [p_exp1; p_exp2]) (effect_of_lexp p_lexp)
+  | LEXP_vector_concat lexps ->
+     let p_lexps = List.map propagate_lexp_effect lexps in
+     LEXP_vector_concat p_lexps, collect_effects_lexp p_lexps
   | LEXP_field (lexp, id) ->
      let p_lexp = propagate_lexp_effect lexp in
      LEXP_field (p_lexp, id),effect_of_lexp p_lexp
diff --git a/src/type_check.mli b/src/type_check.mli
index bb52f2aa..ed240839 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -63,6 +63,10 @@ val opt_tc_debug : int ref
    re-writer passes, so it should only be used for debugging. *)
 val opt_no_effects : bool ref
 
+(** [opt_no_lexp_bounds_check] turns of the bounds checking in vector
+   assignments in l-expressions. *)
+val opt_no_lexp_bounds_check : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
@@ -148,8 +152,9 @@ module Env : sig
   (** Lookup id searchs for a specified id in the environment, and
      returns it's type and what kind of identifier it is, using the
      lvar type. Returns Unbound if the identifier is unbound, and
-     won't throw any exceptions. *)
-  val lookup_id : id -> t -> lvar
+     won't throw any exceptions. If the raw option is true, then look
+     up the type without any flow typing modifiers. *)
+  val lookup_id : ?raw:bool -> id -> t -> lvar
 
   val is_union_constructor : id -> t -> bool
 
diff --git a/src/value.ml b/src/value.ml
index 4b4f0865..e9a98160 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -183,6 +183,10 @@ let value_eq_string = function
   | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2))
   | _ -> failwith "value eq_string"
 
+let value_eq_bit = function
+  | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2))
+  | _ -> failwith "value eq_bit"
+
 let value_length = function
   | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int)
   | _ -> failwith "value length"
@@ -417,6 +421,7 @@ let primops =
       ("eq_list", value_eq_list);
       ("eq_bool", value_eq_bool);
       ("eq_string", value_eq_string);
+      ("eq_bit", value_eq_bit);
       ("eq_anything", value_eq_anything);
       ("length", value_length);
       ("subrange", value_subrange);