Cleaning up the AST and removing redundant and/or unused nodes

14 files changed, 13 insertions, 243 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 710e8067..930af68f 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -264,7 +264,6 @@ type
  | 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 *)
- | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
  | P_vector_concat of ('a pat) list (* concatenated vector pattern *)
  | P_tup of ('a pat) list (* tuple pattern *)
  | P_list of ('a pat) list (* list pattern *)
@@ -303,7 +302,6 @@ type
  | 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_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 *)
  | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *)
  | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 46c79764..a39e570b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -222,8 +222,6 @@ and map_exp_annot_aux f = function
   | 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_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)
   | E_vector_access (exp1, exp2) -> E_vector_access (map_exp_annot f exp1, map_exp_annot f exp2)
   | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3)
   | E_vector_update (exp1, exp2, exp3) -> E_vector_update (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3)
@@ -277,7 +275,6 @@ and map_pat_annot_aux f = function
   | P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
   | P_list pats -> P_list (List.map (map_pat_annot f) pats)
   | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
-  | P_vector_indexed ipats -> P_vector_indexed (List.map (fun (i, pat) -> (i, map_pat_annot f pat)) ipats)
   | P_vector pats -> P_vector (List.map (map_pat_annot f) pats)
   | P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2)
 and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1f7840d0..7b618867 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -429,7 +429,6 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
 		      FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,())))
                  fpats, false)
     | Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env def_ord) pats)
-    | Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env def_ord pat) ipats)
     | Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env def_ord) pats)
     | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats)
     | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats)
@@ -470,19 +469,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | 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)
-    | Parse_ast.E_vector(exps) -> 
-      (match to_ast_iexps false k_env def_ord exps with
-	| Some([]) -> E_vector([])
-	| Some(iexps) -> E_vector_indexed(iexps, 
-					  Def_val_aux(Def_val_empty,(l,())))
-	| None -> E_vector(List.map (to_ast_exp k_env def_ord) exps))
-    | Parse_ast.E_vector_indexed(iexps,Parse_ast.Def_val_aux(default,dl)) -> 
-      (match to_ast_iexps true k_env def_ord iexps with
-	| Some(iexps) -> E_vector_indexed (iexps, 
-					   Def_val_aux((match default with
-					     | Parse_ast.Def_val_empty -> Def_val_empty
-					     | Parse_ast.Def_val_dec e -> Def_val_dec (to_ast_exp k_env def_ord e)),(dl,())))
-	| _ -> raise (Reporting_basic.err_unreachable l "to_ast_iexps didn't throw error"))
+    | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env def_ord) exps)
     | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> 
       E_vector_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
@@ -578,31 +565,6 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp
   | _ ->
     None,Some(l, "Expected a field assignment to be identifier = expression")
 
-and to_ast_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps:Parse_ast.exp list):(int * unit exp) list option =
- match exps with
-   | [] -> Some([])
-   | iexp::exps -> (match to_iexp_try k_env def_ord iexp with
-		     | Some(iexp),None ->
-		       (match to_ast_iexps fail_on_error k_env def_ord exps with
-			 | Some(iexps) -> Some(iexp::iexps)
-			 | _ -> None)
-		     | None,Some(l,msg) ->
-		       if fail_on_error
-		       then typ_error l msg None None None
-		       else None
-		     | _ -> None)
-and to_iexp_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * unit exp) option * (l*string) option) =
-  match exp with
-    | Parse_ast.E_app_infix(left,op,r) ->
-      (match left,op with
-	| Parse_ast.E_aux(Parse_ast.E_lit(Parse_ast.L_aux (Parse_ast.L_num i,ll)),cl), Parse_ast.Id_aux(Parse_ast.Id("="),leq) ->
-	  Some(i,to_ast_exp k_env def_ord r),None
-	| Parse_ast.E_aux(_,li), Parse_ast.Id_aux (Parse_ast.Id("="),leq) ->
-	  None,(Some(li,"Expected a constant number to begin this indexed vector assignemnt"))
-	| Parse_ast.E_aux(_,cl), Parse_ast.Id_aux(_,leq) ->
-	  None,(Some(leq,"Expected an indexed vector assignment constant = expression")))
-    | _ -> None,(Some(l,"Expected an indexed vector assignment: constant = expression"))
-      
 let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : (unit default_spec) envs_out =
   match default with
   | Parse_ast.DT_aux(df,l) ->
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d9ee73b8..e97632ec 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -327,8 +327,6 @@ let nexp_subst_fns substs refinements =
       | E_if (e1,e2,e3) -> re (E_if (s_exp e1, s_exp e2, s_exp e3))
       | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,s_exp e1,s_exp e2,s_exp e3,ord,s_exp e4))
       | E_vector es -> re (E_vector (List.map s_exp es))
-      | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,s_exp e)) ies,
-                                                           s_opt_default ed))
       | E_vector_access (e1,e2) -> re (E_vector_access (s_exp e1,s_exp e2))
       | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (s_exp e1,s_exp e2,s_exp e3))
       | E_vector_update (e1,e2,e3) -> re (E_vector_update (s_exp e1,s_exp e2,s_exp e3))
@@ -401,7 +399,6 @@ let bindings_from_pat p =
     | P_list ps
       -> List.concat (List.map aux_pat ps)
     | P_record (fps,_) -> List.concat (List.map aux_fpat fps)
-    | P_vector_indexed ips -> List.concat (List.map (fun (_,p) -> aux_pat p) ips)
     | P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
   and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
   in aux_pat p
@@ -440,12 +437,6 @@ let rec deexist_exp (E_aux (e,(l,(annot : Type_check.tannot))) as exp) =
   | E_for (id,e1,e2,e3,ord,e4) ->
      re (E_for (id,deexist_exp e1,deexist_exp e2,deexist_exp e3,ord,deexist_exp e4))
   | E_vector es -> re (E_vector (List.map deexist_exp es))
-  | E_vector_indexed (ies,def) ->
-     re (E_vector_indexed
-           (List.map (fun (i,e) -> (i,deexist_exp e)) ies,
-            match def with
-            | Def_val_aux (Def_val_empty,(l,ann)) -> Def_val_aux (Def_val_empty,(l,ann))
-            | Def_val_aux (Def_val_dec e,(l,ann)) -> Def_val_aux (Def_val_dec (deexist_exp e),(l,ann))))
   | E_vector_access (e1,e2) -> re (E_vector_access (deexist_exp e1,deexist_exp e2))
   | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (deexist_exp e1,deexist_exp e2,deexist_exp e3))
   | E_vector_update (e1,e2,e3) -> re (E_vector_update (deexist_exp e1,deexist_exp e2,deexist_exp e3))
@@ -719,8 +710,6 @@ let split_defs splits defs =
        | _ -> re (E_if (e1',e2',e3')))
     | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3,ord,const_prop_exp (ISubst.remove id substs) e4))
     | E_vector es -> re (E_vector (List.map (const_prop_exp substs) es))
-    | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,const_prop_exp substs e)) ies,
-                                                         const_prop_opt_default substs ed))
     | E_vector_access (e1,e2) -> re (E_vector_access (const_prop_exp substs e1,const_prop_exp substs e2))
     | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3))
     | E_vector_update (e1,e2,e3) -> re (E_vector_update (const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3))
@@ -950,8 +939,6 @@ let split_defs splits defs =
            relist fpat (fun fps -> P_record (fps,flag)) fps
         | P_vector ps ->
            relist spl (fun ps -> P_vector ps) ps
-        | P_vector_indexed ips ->
-           relist ipat (fun ips -> P_vector_indexed ips) ips
         | P_vector_concat ps ->
            relist spl (fun ps -> P_vector_concat ps) ps
         | P_tup ps ->
@@ -1039,8 +1026,6 @@ let split_defs splits defs =
       | E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3))
       | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,map_exp e1,map_exp e2,map_exp e3,ord,map_exp e4))
       | E_vector es -> re (E_vector (List.map map_exp es))
-      | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,map_exp e)) ies,
-                                                           map_opt_default ed))
       | E_vector_access (e1,e2) -> re (E_vector_access (map_exp e1,map_exp e2))
       | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (map_exp e1,map_exp e2,map_exp e3))
       | E_vector_update (e1,e2,e3) -> re (E_vector_update (map_exp e1,map_exp e2,map_exp e3))
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b259611d..1036fab8 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -238,7 +238,6 @@ pat_aux =  (* Pattern *)
  | P_app of id * (pat) list (* union constructor pattern *)
  | P_record of (fpat) list * bool (* struct pattern *)
  | P_vector of (pat) list (* vector pattern *)
- | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *)
  | P_vector_concat of (pat) list (* concatenated vector pattern *)
  | P_tup of (pat) list (* tuple pattern *)
  | P_list of (pat) list (* list pattern *)
@@ -267,7 +266,6 @@ exp_aux =  (* Expression *)
  | E_if of exp * exp * exp (* conditional *)
  | 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) *)
  | E_vector_access of exp * exp (* vector access *)
  | E_vector_subrange of exp * exp * exp (* subvector extraction *)
  | E_vector_update of exp * exp * exp (* vector functional update *)
diff --git a/src/parser.mly b/src/parser.mly
index 5413ac0d..c756cf74 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -511,8 +511,6 @@ atomic_pat:
     { ploc (P_vector([$2])) }
   | Lsquare Rsquare
     { ploc (P_vector []) }
-  | Lsquare npats Rsquare
-    { ploc (P_vector_indexed($2)) }
   | Lparen comma_pats Rparen
     { ploc (P_tup($2)) }
   | SquareBarBar BarBarSquare
@@ -603,8 +601,6 @@ atomic_exp:
     { eloc (E_vector([$2])) }
   | Lsquare comma_exps Rsquare
     { eloc (E_vector($2)) }
-  | Lsquare comma_exps Semi Default Eq exp Rsquare
-    { eloc (E_vector_indexed($2,(Def_val_aux(Def_val_dec $6, locn 3 6)))) }
   | Lsquare exp With atomic_exp Eq exp Rsquare
     { eloc (E_vector_update($2,$4,$6)) }
   | Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1bfb19aa..a247b973 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -343,7 +343,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
       | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
   | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
   | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
-  | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *)
+  | P_record (_,_) -> empty (* TODO *)
 
 let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
   | Typ_tup ts -> List.exists contains_bitvector_typ ts
@@ -770,63 +770,6 @@ let doc_exp_lem, doc_let_lem =
                 else (epp,aexp_needed) in
               if aexp_needed then parens (align epp) else epp
        (* *)
-    | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) ->
-      let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
-      let (start, len, order, etyp) =
-        if is_vector_typ t then vector_typ_args_of t
-        else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in
-       let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-       let start = match simplify_nexp start with
-         | Nexp_aux (Nexp_constant i, _) -> string_of_int i
-         | _ -> if dir then "0" else string_of_int (List.length iexps) in
-       let size = match simplify_nexp len with
-         | Nexp_aux (Nexp_constant i, _)-> string_of_int i
-         | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
-           string_of_int (Util.power 2 i)
-         | _ ->
-           raise (Reporting_basic.err_unreachable l
-             "trying to pretty-print indexed vector without constant size") in
-       let default_string =
-         match default with
-         | Def_val_empty ->
-            if is_bitvector_typ t then string "BU"
-            else failwith "E_vector_indexed of non-bitvector type without default argument"
-         | Def_val_dec e ->
-            (*let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
-            match t with
-            | Tapp ("register",
-                    [TA_typ ({t = rt})]) ->
-               (* TODO: Does this case still occur with the new type checker? *)
-               let n = match rt with
-                 | Tapp ("vector",TA_nexp {nexp = Nconst i} :: TA_nexp {nexp = Nconst j} ::_) ->
-                    abs_big_int (sub_big_int i j)
-                 | _ ->
-                    raise ((Reporting_basic.err_unreachable dl)
-                             ("not the right type information available to construct "^
-                                "undefined register")) in
-               parens (string ("UndefinedRegister " ^ string_of_big_int n))
-            | _ ->*) expY e in
-       let iexp (i,e) = parens (doc_int i ^^ comma ^^ expN e) in
-       let expspp =
-         match iexps with
-         | [] -> empty
-         | e :: es ->
-            let (expspp,_) =
-              List.fold_left
-                (fun (pp,count) e ->
-                  (pp ^^ semi ^^ (if count = 5 then break 1 else empty) ^^ iexp e),
-                  if count = 5 then 0 else count + 1)
-                (iexp e,0) es in
-            align (expspp) in
-       let call = string "make_indexed_vector" in
-       let epp =
-         align (group (call ^//^ brackets expspp ^/^
-                         separate space [default_string;string start;string size;string dir_out])) in
-       let (bepp, aexp_needed) =
-         if is_bitvector_typ t && mwords
-         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem sequential mwords false t, true)
-         else (epp, aexp_needed) in
-       if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
        let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 73f06d1a..48ec37b8 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -338,8 +338,6 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
                                           "(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats
                        ^ "])"
   | P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
-  | P_vector_indexed(ipats) ->
-    "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])"
   | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
   | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
   | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
@@ -387,15 +385,6 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
         pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
     | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]"
                           kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
-    | E_vector_indexed(iexps,(Def_val_aux (default, (dl,dannot)))) ->
-      let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
-      let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
-      let default_string ppf _ = (match default with
-        | Def_val_empty -> fprintf ppf "(Def_val_aux Def_val_empty (%a,%a))" pp_lem_l dl pp_annot dannot
-        | Def_val_dec e -> fprintf ppf "(Def_val_aux (Def_val_dec %a) (%a,%a))"
-                             pp_lem_exp e pp_lem_l dl pp_annot dannot) in
-      fprintf ppf "@[<0>(E_aux (%a [%a] %a) (%a, %a))@]" kwd "E_vector_indexed"
-        (list_pp iformat lformat) iexps default_string () pp_lem_l l pp_annot annot
     | E_vector_access(v,e) ->
       fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]"
         kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index b331a6cf..d94879ee 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -198,7 +198,6 @@ let doc_pat_ocaml =
   | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*)
   | P_cons (p,p') -> doc_op (string "::") (pat p) (pat p')
   | P_record _ -> raise (Reporting_basic.err_unreachable l "unhandled record pattern")
-  | P_vector_indexed _ -> raise (Reporting_basic.err_unreachable l  "unhandled vector_indexed pattern")
   | P_vector_concat _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_concat pattern")
   in pat
 
@@ -391,42 +390,6 @@ let doc_exp_ocaml, doc_let_ocaml =
            parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps);
                                                                    string start;
                                                                    string dir_out])])
-    | E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
-      let (start, len, order, _) = vector_typ_args_of (Env.base_typ_of env typ) in
-      (*match annot with
-       | Base((_,t),_,_,_,_,_) ->
-         match t.t with
-         | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])
-         | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])})
-         | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) ->*)
-           let call =
-             if is_bitvector_typ (Env.base_typ_of env typ)
-             then (string "make_indexed_bitv")
-             else (string "make_indexed_v") in
-           let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-           let start = match start with
-             | Nexp_aux (Nexp_constant i, _) -> string_of_int i
-             | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
-               string_of_int (Util.power 2 i)
-             | _ -> if dir then "0" else string_of_int (List.length iexps) in
-           let size = match len with
-             | Nexp_aux (Nexp_constant i, _) -> string_of_int i
-             | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
-               string_of_int (Util.power 2 i)
-             | _ ->
-               raise (Reporting_basic.err_unreachable l
-                 "indexed vector without known length") in
-           let default_string =
-             (match default with
-              | Def_val_empty -> string "None"
-              | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in
-           let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in
-           parens (separate space [call;
-                                   (brackets (separate_map semi iexp iexps));
-                                   default_string;
-                                   string start;
-                                   string size;
-                                   string dir_out])
   | E_vector_update(v,e1,e2) ->
     (*Has never happened to date*)
       brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2)))
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 2f38fe02..8101d45f 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -115,7 +115,6 @@ let doc_pat, doc_atomic_pat =
   | P_app(id,[]) -> doc_id id
   | P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats)
   | P_vector pats  -> brackets (separate_map comma_sp atomic_pat pats)
-  | P_vector_indexed ipats  -> brackets (separate_map comma_sp npat ipats)
   | P_tup pats  -> parens (separate_map comma_sp atomic_pat pats)
   | P_list pats  -> squarebarbars (separate_map semi_sp atomic_pat pats)
   | P_cons (pat1, pat2) -> separate space [atomic_pat pat1; coloncolon; pat pat2]
@@ -263,13 +262,6 @@ let doc_exp, doc_let =
                         ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst)
                       | _ -> assert false)) exps ""))
           | _ -> default_print ()))
-  | E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
-    let default_string =
-      (match default with
-        | Def_val_empty -> string ""
-        | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in
-      let iexp (i,e) = doc_op equals (doc_int i) (exp e) in
-      brackets (concat [(separate_map comma iexp iexps); default_string])
   | E_vector_update(v,e1,e2) ->
       brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2)))
   | E_vector_update_subrange(v,e1,e2,e3) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index fed8408d..ad4b88c4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -131,9 +131,6 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | 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_vector es -> union_eff_exps es
-    | E_vector_indexed (ies,opt_default) ->
-       let (_,es) = List.split ies in
-       union_effects (effect_of_opt_default opt_default) (union_eff_exps es)
     | E_vector_access (e1,e2) -> union_eff_exps [e1;e2]
     | E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
     | E_vector_update (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
@@ -363,7 +360,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
     rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats,
                      false))
   | P_vector pats -> rewrap (P_vector(List.map rewrite pats))
-  | P_vector_indexed ipats -> rewrap (P_vector_indexed(List.map (fun (i,pat) -> (i, rewrite pat)) ipats))
   | P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats))
   | P_tup pats -> rewrap (P_tup (List.map rewrite pats))
   | P_list pats -> rewrap (P_list (List.map rewrite pats))
@@ -389,11 +385,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
   | E_for (id, e1, e2, e3, o, body) ->
     rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
   | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
-  | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
-    let def = match default with
-      | Def_val_empty -> default
-      | Def_val_dec e -> Def_val_dec (rewrite e) in
-    rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot)))
   | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
   | E_vector_subrange (vec,i1,i2) ->
     rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2))
@@ -626,7 +617,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_app            : id * 'pat list -> 'pat_aux
   ; p_record         : 'fpat list * bool -> 'pat_aux
   ; p_vector         : 'pat list -> 'pat_aux
-  ; p_vector_indexed : (int * 'pat) list -> 'pat_aux
   ; p_vector_concat  : 'pat list -> 'pat_aux
   ; p_tup            : 'pat list -> 'pat_aux
   ; p_list           : 'pat list -> 'pat_aux
@@ -647,7 +637,6 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
   | P_app (id,ps)       -> alg.p_app (id,List.map (fold_pat alg) ps)
   | P_record (ps,b)     -> alg.p_record (List.map (fold_fpat alg) ps, b)
   | P_vector ps         -> alg.p_vector (List.map (fold_pat alg) ps)
-  | P_vector_indexed ps -> alg.p_vector_indexed (List.map (fun (i,p) -> (i, fold_pat alg p)) ps)
   | P_vector_concat ps  -> alg.p_vector_concat (List.map (fold_pat alg) ps)
   | P_tup ps            -> alg.p_tup (List.map (fold_pat alg) ps)
   | P_list ps           -> alg.p_list (List.map (fold_pat alg) ps)
@@ -663,7 +652,7 @@ and fold_fpat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat_a
 and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'fpat =
   function
   | FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot)
-                                      
+
 (* identity fold from term alg to term alg *)
 let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = 
   { p_lit            = (fun lit -> P_lit lit)
@@ -675,7 +664,6 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   ; p_app            = (fun (id,ps) -> P_app (id,ps))
   ; p_record         = (fun (ps,b) -> P_record (ps,b))
   ; p_vector         = (fun ps -> P_vector ps)
-  ; p_vector_indexed = (fun ps -> P_vector_indexed ps)
   ; p_vector_concat  = (fun ps -> P_vector_concat ps)
   ; p_tup            = (fun ps -> P_tup ps)
   ; p_list           = (fun ps -> P_list ps)
@@ -699,7 +687,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
   ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * '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
   ; e_vector_subrange        : 'exp * 'exp * 'exp -> 'exp_aux
   ; e_vector_update          : 'exp * 'exp * 'exp -> 'exp_aux
@@ -764,8 +751,6 @@ let rec fold_exp_aux alg = function
   | 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_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)
   | E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2)
   | E_vector_subrange (e1,e2,e3) ->
      alg.e_vector_subrange (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
@@ -841,7 +826,6 @@ let id_exp_alg =
   ; 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_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))
   ; e_vector_subrange =  (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3))
   ; e_vector_update = (fun (e1,e2,e3) -> E_vector_update (e1,e2,e3))
@@ -910,10 +894,6 @@ let compute_pat_alg bot join =
   ; p_app            = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps)
   ; p_record         = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps)
   ; p_vector         = split_join (fun ps -> P_vector ps)
-  ; p_vector_indexed = (fun ps ->
-                          let (is,ps) = List.split ps in
-                          let (vs,ps) = List.split ps in
-                          (join_list vs, P_vector_indexed (List.combine is ps)))
   ; p_vector_concat  = split_join (fun ps -> P_vector_concat ps)
   ; p_tup            = split_join (fun ps -> P_tup ps)
   ; p_list           = split_join (fun ps -> P_list ps)
@@ -938,10 +918,6 @@ let compute_exp_alg bot join =
   ; 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_vector = split_join (fun es -> E_vector es)
-  ; e_vector_indexed = (fun (es,(v2,opt2)) ->
-    let (is,es) = List.split es in
-    let (vs,es) = List.split es in
-    (join_list (vs @ [v2]), E_vector_indexed (List.combine is es,opt2)))
   ; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2)))
   ; e_vector_subrange =  (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3)))
   ; e_vector_update = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_update (e1,e2,e3)))
@@ -1178,7 +1154,6 @@ let rewrite_sizeof (Defs defs) =
     ; 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_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')))
     ; e_vector_subrange =  (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3')))
     ; e_vector_update = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_update (e1,e2,e3), E_vector_update (e1',e2',e3')))
@@ -1377,7 +1352,6 @@ let remove_vector_concat_pat pat =
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
     ; p_record = (fun (fpats,b) -> P_record (fpats, b))
     ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
-    ; p_vector_indexed = (fun ps -> P_vector_indexed (List.map (fun (i,p) -> (i,p false)) ps))
     ; p_vector_concat  = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
@@ -1511,10 +1485,6 @@ let remove_vector_concat_pat pat =
                                         (P_record (ps,b),List.flatten decls))
     ; p_vector         = (fun ps -> let (ps,decls) = List.split ps in
                                     (P_vector ps,List.flatten decls))
-    ; p_vector_indexed = (fun ps -> let (is,ps) = List.split ps in
-                                    let (ps,decls) = List.split ps in
-                                    let ps = List.combine is ps in
-                                    (P_vector_indexed ps,List.flatten decls))
     ; p_vector_concat  = (fun ps -> let (ps,decls) = List.split ps in
                                     (P_vector_concat ps,List.flatten decls))
     ; p_tup            = (fun ps -> let (ps,decls) = List.split ps in
@@ -1740,10 +1710,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
     (match subsumes_pat pat1 pat2, subsumes_pat pats1 pats2 with
     | Some substs1, Some substs2 -> Some (substs1 @ substs2)
     | _ -> None)
-  | P_vector_indexed ips1, P_vector_indexed ips2 ->
-    let (is1,ps1) = List.split ips1 in
-    let (is2,ps2) = List.split ips2 in
-    if is1 = is2 then subsumes_list subsumes_pat ps1 ps2 else None
   | _ -> None
 and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
   if id1 = id2 then subsumes_pat pat1 pat2 else None
@@ -1782,8 +1748,6 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
   | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats))
   | P_list pats -> rewrap (E_list (List.map pat_to_exp pats))
   | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps))
-  | P_vector_indexed ipats -> raise (Reporting_basic.err_unreachable l
-      "pat_to_exp not implemented for P_vector_indexed") (* TODO *)
 and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
   FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
 
@@ -1853,7 +1817,7 @@ let bitwise_and_exp exp1 exp2 =
 let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
 | P_lit _ | P_wild | P_id _ -> false
 | P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat
-| P_vector _ | P_vector_concat _ | P_vector_indexed _ ->
+| P_vector _ | P_vector_concat _ ->
     let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
     is_bitvector_typ typ
 | P_app (_,pats) | P_tup pats | P_list pats ->
@@ -1881,7 +1845,6 @@ let remove_bitvector_pat pat =
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
     ; p_record = (fun (fpats,b) -> P_record (fpats, b))
     ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
-    ; p_vector_indexed = (fun ps -> P_vector_indexed (List.map (fun (i,p) -> (i,p false)) ps))
     ; p_vector_concat  = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
     ; p_tup            = (fun ps -> P_tup (List.map (fun p -> p false) ps))
     ; p_list           = (fun ps -> P_list (List.map (fun p -> p false) ps))
@@ -1893,8 +1856,6 @@ let remove_bitvector_pat pat =
           let (l,_) = annot in
           match pat, is_bitvector_typ t, contained_in_p_as with
           | P_vector _, true, false
-          | P_vector_indexed _, true, false ->
-            P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot)
           | _ -> P_aux (pat,annot)
         )
     ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
@@ -2047,10 +2008,6 @@ let remove_bitvector_pat pat =
                                         (P_record (ps,b), flatten_guards_decls gdls))
     ; p_vector         = (fun ps -> let (ps,gdls) = List.split ps in
                                     (P_vector ps, flatten_guards_decls gdls))
-    ; p_vector_indexed = (fun p -> let (is,p) = List.split p in
-                                   let (ps,gdls) = List.split p in
-                                   let ps = List.combine is ps in
-                                   (P_vector_indexed ps, flatten_guards_decls gdls))
     ; p_vector_concat  = (fun ps -> let (ps,gdls) = List.split ps in
                                     (P_vector_concat ps, flatten_guards_decls gdls))
     ; p_tup            = (fun ps -> let (ps,gdls) = List.split ps in
@@ -2065,8 +2022,6 @@ let remove_bitvector_pat pat =
                            (match pat, is_bitvector_typ t with
                            | P_as (P_aux (P_vector ps, _), id), true ->
                              (P_aux (P_id id, annot), collect_guards_decls ps id t)
-                           | P_as (P_aux (P_vector_indexed ips, _), id), true ->
-                             (P_aux (P_id id, annot), collect_guards_decls_indexed ips id t)
                            | _, _ -> (P_aux (pat,annot), gdls)))
     ; fP_aux           = (fun ((fpat,gdls),annot) -> (FP_aux (fpat,annot), gdls))
     ; fP_Fpat          = (fun (id,(pat,gdls)) -> (FP_Fpat (id,pat), gdls))
@@ -2843,12 +2798,6 @@ let rewrite_defs_letbind_effects  =
     | E_vector exps ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_vector exps)))
-    | E_vector_indexed (exps,opt_default)  ->
-       let (is,exps) = List.split exps in
-       n_exp_nameL exps (fun exps -> 
-       n_opt_default opt_default (fun opt_default ->
-       let exps = List.combine is exps in
-       k (rewrap (E_vector_indexed (exps,opt_default)))))
     | E_vector_access (exp1,exp2) ->
        n_exp_name exp1 (fun exp1 ->
        n_exp_name exp2 (fun exp2 ->
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 010f1003..645ecbf4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -70,7 +70,6 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   ; p_app            : id * 'pat list -> 'pat_aux
   ; p_record         : 'fpat list * bool -> 'pat_aux
   ; p_vector         : 'pat list -> 'pat_aux
-  ; p_vector_indexed : (int * 'pat) list -> 'pat_aux
   ; p_vector_concat  : 'pat list -> 'pat_aux
   ; p_tup            : 'pat list -> 'pat_aux
   ; p_list           : 'pat list -> 'pat_aux
@@ -98,7 +97,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
  ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * '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
  ; e_vector_subrange        : 'exp * 'exp * 'exp -> 'exp_aux
  ; e_vector_update          : 'exp * 'exp * 'exp -> 'exp_aux
diff --git a/src/sail.ml b/src/sail.ml
index b63f807c..624c90be 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -50,6 +50,7 @@ let opt_print_verbose = ref false
 let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 let opt_print_ocaml = ref false
+let opt_convert = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_ocaml = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
@@ -100,6 +101,9 @@ let options = Arg.align ([
   ( "-just_check",
     Arg.Set opt_just_check,
     " (experimental) terminate immediately after typechecking");
+  ( "-convert",
+    Arg.Set opt_convert,
+    " Convert sail to new syntax");
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
@@ -145,6 +149,11 @@ let main() =
       List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
                         -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
     let ast = convert_ast Ast_util.inc_ord ast in
+
+    if !opt_convert
+    then (Pretty_print_sail2.pp_defs stdout ast; exit 0)
+    else ();
+
     let (ast, type_envs) = check_ast ast in
 
     let (ast, type_envs) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index d349037e..e04b7d33 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -291,8 +291,6 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
     List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
         pat_bindings consider_var bound used p) fpats (bound,used)
   | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
-  | P_vector_indexed ipats ->
-    List.fold_right (fun (_,p) (b,n) -> pat_bindings consider_var b n p) ipats (bound,used)
   | _ -> bound,used
 
 let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.t * Nameset.t * Nameset.t) =
@@ -317,13 +315,6 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
   | E_for(id,from,to_,by,_,body) ->
     let _,used,set = list_fv bound used set [from;to_;by] in
     fv_of_exp consider_var (Nameset.add (string_of_id id) bound) used set body
-  | E_vector_indexed (es_i,(Ast.Def_val_aux(default,_))) ->
-    let bound,used,set =
-      List.fold_right
-        (fun (_,e) (b,u,s) -> fv_of_exp consider_var b u s e) es_i (bound,used,set) in
-    (match default with
-     | Def_val_empty -> bound,used,set
-     | Def_val_dec e -> fv_of_exp consider_var bound used set e)
   | E_vector_access(v,i) -> list_fv bound used set [v;i]
   | E_vector_subrange(v,i1,i2) -> list_fv bound used set [v;i1;i2]
   | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e]