Get indexed vectors, particularly with default values, working

8 files changed, 268 insertions, 49 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 0cd58e02..4d08e9eb 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -353,8 +353,19 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
     | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
       E_for(to_ast_id id,to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3,to_ast_order k_env atyp, to_ast_exp k_env e4)
-    | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env) exps)
-    | Parse_ast.E_vector_indexed(iexps,default) -> E_vector_indexed(List.map (fun (i,e) -> (i,to_ast_exp k_env e)) iexps, Def_val_aux(Def_val_empty,(l,NoTyp))) (*TODO transform the default *)
+    | Parse_ast.E_vector(exps) -> 
+      (match to_ast_iexps false k_env exps with
+	| Some([]) -> E_vector([])
+	| Some(iexps) -> E_vector_indexed(iexps, 
+					  Def_val_aux(Def_val_empty,(l,NoTyp)))
+	| None -> E_vector(List.map (to_ast_exp k_env) exps))
+    | Parse_ast.E_vector_indexed(iexps,Parse_ast.Def_val_aux(default,dl)) -> 
+      (match to_ast_iexps true k_env 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 e)),(dl,NoTyp)))
+	| _ -> raise (Reporting_basic.err_unreachable l "to_ast_iexps didn't throw error"))
     | Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env vexp, to_ast_exp k_env exp)
     | Parse_ast.E_vector_subrange(vex,exp1,exp2) -> E_vector_subrange(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
     | Parse_ast.E_vector_update(vex,exp1,exp2) -> E_vector_update(to_ast_exp k_env vex, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
@@ -426,6 +437,31 @@ and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_as
       None,Some(l,"Expected a field assignment to be identifier = expression"))
   | _ ->
     None,Some(l, "Expected a field assignment to be identifier = expression")
+
+and to_ast_iexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_ast.exp list) : (int * tannot exp) list option =
+ match exps with
+   | [] -> Some([])
+   | iexp::exps -> (match to_iexp_try k_env iexp with
+		     | Some(iexp),None ->
+		       (match to_ast_iexps fail_on_error k_env 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) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * tannot 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 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, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out =
   match default with
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 7ae5caff..f1c26093 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -66,7 +66,10 @@ type value =
  | V_lit of lit
  | V_tuple of list value
  | V_list of list value
- | V_vector of integer * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
+ (* A full vector: integer is the first index, bool says if that's most or least significant *)
+ | V_vector of integer * bool * list value 
+ (* A vector with default values, second integer stores length; as above otherwise *)
+ | V_vector_sparse of integer * integer * bool * list (integer * value) * value 
  | V_record of t * list (id * value)
  | V_ctor of id * t * value
  | V_unknown (* Distinct from undefined, used by memory system *)
@@ -82,6 +85,8 @@ and value_eq left right =
   | (V_list l, V_list l') -> listEqualBy value_eq l l'
   | (V_vector n b l, V_vector m b' l') ->
       n = m && b = b' && listEqualBy value_eq l l'
+  | (V_vector_sparse n o b l v, V_vector_sparse m p b' l' v') ->
+    n=m && o=p && b=b' && listEqualBy (fun (i,v) (i',v') -> i=i' && (value_eq v v')) l l' && value_eq v v'
   | (V_record t l, V_record t' l') ->
       t = t' &&
       listEqualBy id_value_eq l l'
@@ -105,7 +110,7 @@ let emem = LMem 1 Map.empty
 
 type read_kind = Read_plain | Read_reserve | Read_acquire
 type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = | Barrier_plain  (* ... *) 
+type barrier_kind = | Barrier_plain  (* ?? *) 
 
 (*top_level is a tuple of 
   (all definitions, letbound and enum values, register values, Typedef union constructors, and sub register mappings) *)
@@ -205,15 +210,6 @@ let rec to_data_constructors (Defs defs) =
     | _ -> to_data_constructors (Defs defs) end
    end
 
-(* Due to type checker, all variables should be in the environment unless an Unknown has matched a pattern,
-   so unfound identifiers propogate Unknown *)
-val in_venv : (list (id * value)) -> id -> value
-let rec in_venv env id =
- match env with
- | [] -> V_unknown
- | (eid,value)::env -> if (get_id eid) = (get_id id) then value else in_venv env id
- end 
-
 val in_env :forall 'a. (list (id * 'a)) -> id -> maybe 'a
 let rec in_env env id =
  match env with
@@ -297,6 +293,10 @@ let access_vector v n =
     if inc then
     list_nth vs (n - m)
     else list_nth vs (m - n)
+  | V_vector_sparse _ _ _ vs d ->
+    match (List.lookup n vs) with
+      | Nothing -> d
+      | Just v  -> v end 
   end
 
 val from_n_to_n :forall 'a. integer -> integer  -> list 'a -> list 'a
@@ -305,6 +305,22 @@ let from_n_to_n from to_ ls =
   let to_ = natFromInteger to_ in
   take (to_ - from + 1) (drop from ls)
 
+val slice_sparse_list : (integer -> integer -> bool) -> (integer -> integer) -> 
+                        list (integer * value) -> integer -> integer -> ((list (integer * value)) * bool)
+let rec slice_sparse_list compare update_n vals n1 n2 = 
+  let sl = slice_sparse_list compare update_n in
+  if n1 = n2 
+  then ([],false)
+  else match vals with
+    | [] -> ([],true)
+    | (i,v)::vals -> 
+      if n1 = i 
+      then let (rest,still_sparse) = (sl vals (update_n n1) n2) in ((i,v)::rest,still_sparse)
+      else if (compare n1 i)
+      then  (sl vals (update_n n1) n2)
+      else let (rest,_) = (sl vals (update_n i) n2) in ((i,v)::rest,true)
+  end
+
 val slice_vector : value -> integer -> integer -> value
 let slice_vector v n1 n2 =
   match v with
@@ -312,6 +328,16 @@ let slice_vector v n1 n2 =
     if inc 
     then V_vector 0 inc (from_n_to_n (n1 - m) (n2 - m) vs)
     else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs)
+  | V_vector_sparse m n inc vs d -> 
+    let (slice, still_sparse) = 
+      if inc 
+      then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
+      else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
+    if still_sparse && inc
+    then V_vector_sparse 0 (n2 - n1) inc slice d
+    else if inc then V_vector 0 inc (List.map snd slice)
+    else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d
+    else V_vector (n1 - n2 +1) inc (List.map snd slice)
   end
 
 val update_field_list : list (id * value) -> list (id * value) -> list (id * value)
@@ -335,17 +361,39 @@ let rec update_vector_slice vector value mem =
     foldr2 (fun vbox v mem -> match vbox with
                                        | V_boxref n t -> update_mem mem n v end)
       mem vs vals
+  | ((V_vector m inc vs),(V_vector_sparse n o inc2 vals d)) -> 
+    let (_,mem) = foldr (fun vbox (i,mem) ->
+                          match vbox with
+			    | V_boxref n t -> 
+			      (if inc then i+1 else i-1,
+				update_mem mem n (match List.lookup i vals with
+				  | Nothing -> d
+				  | Just v  -> v end))
+                          end) (m,mem) vs in 
+    mem
   | ((V_vector m inc vs),v) ->
     List.foldr (fun vbox mem -> match vbox with
                                     | V_boxref n t -> update_mem mem n v end)
       mem vs
 end
 
+val fupdate_sparse : (integer -> integer -> bool) -> list (integer*value) -> integer -> value -> list (integer*value)
+let rec fupdate_sparse compare vs n vexp =
+  match vs with
+    | [] -> [(n,vexp)]
+    | (i,v)::vs ->
+      if i = n then (i,vexp)::vs
+      else if (compare i n) then (n,vexp)::(i,v)::vs
+      else (i,v)::(fupdate_sparse compare vs n vexp)
+end
+
 val fupdate_vec : value -> integer -> value -> value
 let fupdate_vec v n vexp =
   match v with
   | V_vector m inc vals -> 
     V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
+  | V_vector_sparse m o inc vals d ->
+    V_vector_sparse m o inc (fupdate_sparse (if inc then (>) else (<)) vals n vexp) d
   end
 
 val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
@@ -360,6 +408,17 @@ let rec replace_is ls vs base start stop =
     else l::(replace_is ls (v::vs) (base+1) start stop)
   end
 
+val replace_sparse : (integer -> integer -> bool) -> list (integer * value) -> list (integer * value) -> list (integer * value)
+let rec replace_sparse compare vals reps =
+  match (vals,reps) with
+    | ([],rs) -> rs
+    | (vs,[]) -> vs
+    | ((i1,v)::vs,(i2,r)::rs) ->
+      if i1 = i2 then (i2,r)::(replace_sparse compare vs rs)
+      else if (compare i1 i2) then (i1,v)::(replace_sparse compare vs ((i2,r)::rs))
+      else (i2,r)::(replace_sparse compare ((i1,v)::vs) rs)
+end
+
 val fupdate_vector_slice : value -> value -> integer -> integer -> value
 let fupdate_vector_slice vec replace start stop =
   match (vec,replace) with
@@ -369,6 +428,9 @@ let fupdate_vector_slice vec replace start stop =
 	 (if inc=inc' then reps 
 	  else (List.reverse reps)) 
 	 0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
+  | (V_vector_sparse m n inc vals d,V_vector _ _ reps) ->
+    let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
+    (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d)
   end
 
 val in_ctors : list (id * typ) -> id -> maybe typ
@@ -460,6 +522,12 @@ let rec val_typ v =
       T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
 			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
 			      T_arg_typ t])
+    | V_vector_sparse n m inc vals d ->
+      let ts = List.map val_typ (d::(List.map snd vals)) in
+      let t = combine_typs ts in
+      T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const m);
+			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
+			      T_arg_typ t])
     | V_record t ivals -> t
     | V_list vals -> 
       let ts = List.map val_typ vals in
@@ -480,9 +548,15 @@ let rec to_exp v =
 	if (inc && n=0) 
 	then E_vector (List.map to_exp vals) 
 	else if inc then
-          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals))) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
+          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+	                   (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
 	else 
-          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
+          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) 
+	                   (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
+      | V_vector_sparse n m inc vals d ->
+	E_vector_indexed ((if inc then List.reverse else (fun i -> i)) 
+			     (List.map (fun (i,v) -> (i, to_exp v)) vals))
+	                 (Def_val_aux (Def_val_dec (to_exp d)) (Interp_ast.Unknown,Nothing)) (*Can possibly do better*)
       | V_record t ivals -> 
 	E_record(FES_aux (FES_Fexps
 			    (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false) 
@@ -608,6 +682,20 @@ let rec match_pattern (P_aux p _) value =
 	 else (false,false,[]))
        (true,false,[]) (if inc then pats else List.reverse pats) vals
      else (false,false,[])
+   | V_vector_sparse n m inc vals d ->
+     if ((natFromInteger m) = (List.length pats))
+     then let (_,matched_p,used_unknown,bounds) =
+	    foldr
+	      (fun pat (i,matched_p,used_unknown,bounds) ->
+		if matched_p 
+		then let (matched_p,used_unknown',new_bounds) = 
+		       match_pattern pat (match List.lookup i vals with
+			 | Nothing -> d
+			 | Just v  -> v end) in
+		     ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(new_bounds ++ bounds))
+                else (i,false,false,[])) (n,true,false,[]) pats in
+	  (matched_p,used_unknown,bounds)
+     else (false,false,[])
    | V_unknown -> (true,true,[])
    | _ -> (false,false,[])
      end
@@ -621,6 +709,13 @@ let rec match_pattern (P_aux p _) value =
 	   (matched_p,used_unknown||used_unknown',new_bounds++bounds)
          else (false,false,[]))
        (true,false,[]) ipats
+   | V_vector_sparse n m inc vals d ->
+     List.foldr
+       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < m then
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> v end) in
+	   (matched_p,used_unknown||used_unknown',new_bounds++bounds)
+	 else (false,false,[]))
+       (true,false,[]) ipats
    | V_unknown -> (true,true,[])
    | _ -> (false,false, [])
    end 
@@ -793,7 +888,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			      if start = i 
 			      then (Value v tag,lm,le)
 			      else (Value (V_vector i inc items) tag,lm,le)
-			    | _ -> (Value v tag,lm,le) end) 
+			    | _ -> (Value v tag,lm,le) end)
+			| (_,V_vector_sparse start inc len items def) ->
+			  (match typ with
+			    | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
+			      if start = i
+			      then (Value v tag,lm,le)
+			      else (Value (V_vector_sparse i inc len items def) tag,lm,le) (*Shoud I trim any actual items*)
+			    | _ -> (Value v tag,lm,le) end)
                         | _ -> (Value v Tag_empty,lm,le) end)
 	              (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast ctyp e) (l,annot)))))
     | E_id id -> 
@@ -998,6 +1100,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                           (fun vvec lm le ->
                                             match vvec with
                                             | V_vector base inc vals -> (Value (access_vector vvec n) Tag_empty,lm,le)
+					    | V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n) Tag_empty,lm,le)
 					    | V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                             | _ -> (Error l "Vector access of non-vector",lm,le)end)
                                           (fun a -> update_stack a 
@@ -1018,7 +1121,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                               resolve_outcome (interp_main mode t_level l_env lm vec)
                                                               (fun vvec lm le ->
                                                                 match vvec with
-                                                                | V_vector base inc vals -> (Value (slice_vector vvec n1 n2) Tag_empty,lm,le)
+                                                                | V_vector _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty,lm,le)
+								| V_vector_sparse _ _ _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty, lm,le)
 								| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                                                 | _ -> (Error l "Vector slice of non-vector",lm,le)end)
                                                               (fun a -> update_stack a 
@@ -1047,7 +1151,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                             resolve_outcome (interp_main mode t_level le lm vec)
                                                             (fun vec lm le ->
                                                               match vec with
-                                                              | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup) Tag_empty, lm,le)
+                                                              | V_vector _ _ _ -> (Value (fupdate_vec vec n1 vup) Tag_empty, lm,le)
+							      | V_vector_sparse _ _ _ _ _ -> (Value (fupdate_vec vec n1 vup) Tag_empty,lm,le)
 							      | V_unknown -> (Value V_unknown Tag_empty, lm, le)
                                                               | _ -> (Error l "Update of vector given non-vector",lm,le) end)
                                                             (fun a -> update_stack a 
@@ -1078,7 +1183,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                        (interp_main mode t_level l_env lm vec)
                                        (fun vvec lm le ->
                                          match vvec with
-                                         | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
+                                         | V_vector _ _ _ -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
+					 | V_vector_sparse _ _ _ _ _ -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
 					 | V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                          | _ -> (Error l "Vector update requires vector",lm,le) end)
                                        (fun a -> update_stack a 
@@ -1106,6 +1212,26 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                             (fun v2 lm le ->
                                               match v2 with
                                               | V_vector _ _ vals2 -> (Value (V_vector m inc (vals1++vals2)) Tag_empty,lm,l_env)
+					      | V_vector_sparse _ len _ vals2 d ->
+						let original_len = integerFromNat (List.length vals1) in
+						let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
+						let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
+						(Value (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) Tag_empty, lm,l_env)
+					      | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
+                                              | _ -> (Error l "vector concat requires vector",lm,le) end)
+                                            (fun a -> update_stack a (add_to_top_frame 
+                                                                        (fun e -> E_aux (E_vector_append (to_exp v1) e) (l,annot)))))
+			| V_vector_sparse m len inc vals1 d ->
+			  (resolve_outcome (interp_main mode t_level l_env lm e2)
+                                            (fun v2 lm le ->
+                                              match v2 with
+                                              | V_vector _ _ vals2 -> 
+						let new_len = integerFromNat (List.length vals2) in
+						let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
+						(Value (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) Tag_empty, lm,l_env)
+					      | V_vector_sparse _ new_len _ vals2 _ ->
+						let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
+						(Value (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) Tag_empty, lm,l_env)
 					      | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                                               | _ -> (Error l "vector concat requires vector",lm,le) end)
                                             (fun a -> update_stack a (add_to_top_frame 
@@ -1117,13 +1243,25 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
       exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
-    | E_vector_indexed iexps default ->
+    | E_vector_indexed iexps (Def_val_aux default dannot) ->
       let (indexes,exps) = List.unzip iexps in
-      let is_inc = match typ with
-        | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
-        | _ -> false end in
-      exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) default) (l,annot))) 
-                       (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
+      let (is_inc,base,len) = (match typ with
+        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) -> (true,base,len)
+        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) -> (false,base,len) end) in
+      (match default with
+	| Def_val_empty ->
+	  exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) (Def_val_aux default dannot)) (l,annot))) 
+                                (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
+	| Def_val_dec default_exp ->
+	  let (b,len) = match (base,len) with
+	    | (Ne_const b,Ne_const l) -> (b,l) end in
+	  resolve_outcome (interp_main mode t_level l_env l_mem default_exp)
+	                  (fun v lm le -> 
+			    exp_list mode t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
+								                      (Def_val_aux (Def_val_dec (to_exp v)) dannot))
+								    (l,annot)))
+			                          (fun vs -> (V_vector_sparse b len is_inc (map2 (fun i v -> (i,v)) indexes vs) v)) l_env l_mem [] exps)
+	                 (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot)))) end)	  
     | E_block(exps) -> interp_block mode t_level l_env l_env l_mem l annot exps
     | E_app f args ->
       (match (exp_list mode t_level (fun es -> E_aux (E_app f es) (l,annot)) 
@@ -1410,6 +1548,20 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               | (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
               | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n) Tag_empty,lm, l_env),Just (next_builder lexp_builder))
               | (v,false, Just lexp_builder) -> ((Value v Tag_empty,lm,le), Just (next_builder lexp_builder)) end)
+	    | V_vector_sparse n m inc vs d ->
+              let nth = access_vector v n in
+              (match (nth,is_top_level,maybe_builder) with
+		| (V_register regform,true,_) ->
+		  ((Action (Write_reg regform Nothing value)
+		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),Nothing)
+		| (V_register regform,false,Just lexp_builder) ->
+		  ((Action (Write_reg regform Nothing value)
+		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),
+                   Just (next_builder lexp_builder))
+		| (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, update_mem lm n value, l_env),Nothing)
+		| (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
+		| ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n) Tag_empty,lm, l_env),Just (next_builder lexp_builder))
+		| (v,false, Just lexp_builder) -> ((Value v Tag_empty,lm,le), Just (next_builder lexp_builder)) end)
             | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end)
          | ((Action a s,lm,le),Just lexp_builder) ->
            (match (a,is_top_level) with
diff --git a/src/parser.mly b/src/parser.mly
index aa088994..2679c2ca 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -547,6 +547,8 @@ 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.ml b/src/pretty_print.ml
index 0f1f461f..86772b80 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -338,10 +338,13 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (%a %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" 
 	kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 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,default) -> (*TODO print out default when it is an nonempty*) 
+    | 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
-      fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps pp_lem_l l pp_annot annot
+      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
     | E_vector_subrange(v,e1,e2) -> 
       fprintf ppf "@[<0>(E_aux (%a %a %a %a) (%a, %a))@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index 8940eaad..79f3bf23 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -11,9 +11,13 @@ function forall Type 'a . 'a id ( x ) = x
 
 register nat match_success
 register nat add_check
+register bit partial_check
 
 let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check,slice_check]
 
+let (bit[3]) indexed = [0=1,1=1,2=0]
+let (bit[50]) partial = [0 = 0, 5=1, 32=0; default = 0]
+
 function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
 and decode x = match_success := x
 
@@ -37,6 +41,8 @@ function bit main _ = {
   result := gpr_small[1] + id(gpr_small[1]);
  
   add_check := gpr_small[2] + 3;
+  partial_check := partial[5];
+  partial_check := partial[49];
 
   i := [bitzero, bitzero, bitone, bitzero];
 
diff --git a/src/type_check.ml b/src/type_check.ml
index d7c3787d..87560fa1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -442,8 +442,9 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
     | E_cast(typ,e) ->
       let cast_t = typ_to_t typ in
       let cast_t,cs_a = get_abbrev d_env cast_t in
-      let (e',u,t_env,cs,ef) = check_exp envs cast_t e in
-(*      let t',cs2,e' = type_coerce (Expr l) d_env true u e' cast_t in*)
+      let ct = {t = Toptions(cast_t,None)} in
+      let (e',u,t_env,cs,ef) = check_exp envs ct e in
+      let t',cs2,e' = type_coerce (Expr l) d_env true u e' cast_t in
       let t',cs3,e'' = type_coerce (Expr l) d_env false cast_t e' expect_t in 
       (e'',t',t_env,cs_a@cs@cs3,ef)
     | E_app(id,parms) -> 
@@ -656,25 +657,38 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
       let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst zero});TA_nexp({nexp=Nconst (big_int_of_int (List.length es))});TA_ord({order=Oinc});TA_typ item_t])} in
       let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_vector es,(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
       (e',t',t_env,cs@cs',effect)
-    | E_vector_indexed(eis,default) ->
-      let item_t = match expect_t.t with
-        | Tapp("vector",[base;rise;ord;TA_typ item_t]) -> item_t
-        | _ -> new_t () in
+    | E_vector_indexed(eis,(Def_val_aux(default,(ld,annot)))) ->
+      let item_t,base_n,rise_n = match expect_t.t with
+        | Tapp("vector",[TA_nexp base;TA_nexp rise;ord;TA_typ item_t]) -> item_t,base,rise
+        | _ -> new_t (),new_n (), new_n () in
       let first,last = fst (List.hd eis), fst (List.hd (List.rev eis)) in
       let is_increasing = first <= last in
       let es,cs,effect,_ = (List.fold_right 
 			      (fun ((i,e),c,ef) (es,cs,effect,prev) -> 
+				(*let _ = Printf.printf "Checking increasing %b %i %i\n" is_increasing prev i in*)
 				if is_increasing 
-				then if prev <= i then (((i,e)::es),(c@cs),union_effects ef effect,i) 
+				then if prev >= i then (((i,e)::es),(c@cs),union_effects ef effect,i) 
 				  else (typ_error l "Indexed vector is not consistently increasing")
-				else if i <= prev then (((i,e)::es),(c@cs),union_effects ef effect,i) 
+				else if i >= prev then (((i,e)::es),(c@cs),union_effects ef effect,i) 
 				else (typ_error l "Indexed vector is not consistently decreasing"))
 			      (List.map (fun (i,e) -> let (e,_,_,cs,eft) = (check_exp envs item_t e) in ((i,e),cs,eft))
-				 eis) ([],[],pure_e,first)) in
-      let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst (big_int_of_int first)});TA_nexp({nexp=Nconst (big_int_of_int (List.length eis))});
-				  TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
-      let t',cs',e' = type_coerce (Expr l) d_env false t (E_aux(E_vector_indexed(es,default),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
-      (e',t',t_env,cs@cs',effect)
+				 eis) ([],[],pure_e,last)) in
+      let (default',fully_enumerate,cs_d,ef_d) = match default with
+	| Def_val_empty -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e)
+	| Def_val_dec e -> let (de,t,_,cs_d,ef_d) = (check_exp envs item_t e) in
+			   (*Check that ef_d doesn't write to memory or registers? *)
+			   (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in
+      let (base_bound,length_bound,cs_bounds) = 
+	if fully_enumerate
+	then ({nexp=Nconst (big_int_of_int first)},{nexp = Nconst (big_int_of_int (List.length eis))},[])
+	else (base_n,rise_n,[LtEq(Expr l, base_n,{nexp = Nconst (big_int_of_int first)});
+			     GtEq(Expr l,rise_n,{nexp = Nconst (big_int_of_int (List.length eis))})]) in	     
+      let t = {t = Tapp("vector",
+			[TA_nexp(base_bound);TA_nexp length_bound;
+			 TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in
+      let t',cs',e' = type_coerce (Expr l) d_env false t 
+	                          (E_aux (E_vector_indexed(es,default'),(l,Base(([],t),Emp_local,[],pure_e)))) expect_t in
+      (e',t',t_env,cs@cs_d@cs_bounds@cs',union_effects ef_d effect)
     | E_vector_access(vec,i) ->
       let base,rise,ord = new_n(),new_n(),new_o() in
       let item_t = new_t () in
@@ -1192,7 +1206,7 @@ and check_lbind envs is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot let
     | Base((params,t),tag,cs,ef) ->
       let t,cs,ef = subst params t cs ef in
       let (pat',env,cs1,u) = check_pattern envs emp_tag t pat in
-      let (e,t,_,cs2,ef2) = check_exp envs u e in
+      let (e,t,_,cs2,ef2) = check_exp envs t e in
       let cs = resolve_constraints cs@cs1@cs2 in
       let ef = union_effects ef ef2 in
       let tannot = check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 72f0b3f7..9d222672 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -32,7 +32,7 @@ and t_aux =
   | Ttup of t list
   | Tapp of string * t_arg list
   | Tabbrev of t * t
-  | Toptions of t * t
+  | Toptions of t * t option
   | Tuvar of t_uvar
 and t_uvar = { index : int; mutable subst : t option }
 and nexp = { mutable nexp : nexp_aux }
@@ -136,7 +136,8 @@ let rec t_to_string t =
     | Ttup(tups) -> "(" ^ string_of_list ", " t_to_string tups ^ ")"
     | Tapp(i,args) -> i ^ "<" ^  string_of_list ", " targ_to_string args ^ ">"
     | Tabbrev(ti,ta) -> (t_to_string ti) ^ " : " ^ (t_to_string ta)
-    | Toptions(t1,t2) -> if !debug_mode then ("(either "^ (t_to_string t1) ^ " or " ^ (t_to_string t2) ^ ")") else "_"
+    | Toptions(t1,None) -> if !debug_mode then ("optionally " ^ (t_to_string t1)) else (t_to_string t1)
+    | Toptions(t1,Some t2) -> if !debug_mode then ("(either "^ (t_to_string t1) ^ " or " ^ (t_to_string t2) ^ ")") else "_"
     | Tuvar({index = i;subst = a}) -> 
       if !debug_mode then "Tu_" ^ string_of_int i ^ "("^ (match a with | None -> "None" | Some t -> t_to_string t) ^")" else "_"
 and targ_to_string = function
@@ -573,7 +574,8 @@ let rec occurs_check_t (t_box : t) (t : t) : unit =
       List.iter (occurs_check_t t_box) ts
     | Tapp(_,targs) -> List.iter (occurs_check_ta (TA_typ t_box)) targs
     | Tabbrev(t,ta) -> occurs_check_t t_box t; occurs_check_t t_box ta
-    | Toptions(t1,t2) -> occurs_check_t t_box t1; occurs_check_t t_box t2
+    | Toptions(t1,None) -> occurs_check_t t_box t1
+    | Toptions(t1,Some t2) -> occurs_check_t t_box t1; occurs_check_t t_box t2
     | _ -> ()
 and occurs_check_ta (ta_box : t_arg) (ta : t_arg) : unit =
   match ta_box,ta with
@@ -1002,7 +1004,8 @@ let rec t_subst s_env t =
   | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) }
   | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)}
   | Tabbrev(ti,ta) -> {t = Tabbrev(t_subst s_env ti,t_subst s_env ta) }
-  | Toptions(t1,t2) -> {t = Toptions(t_subst s_env t1,t_subst s_env t2) }
+  | Toptions(t1,None) -> {t = Toptions(t_subst s_env t1,None)}
+  | Toptions(t1,Some t2) -> {t = Toptions(t_subst s_env t1,Some (t_subst s_env t2)) }
 and ta_subst s_env ta =
   match ta with
   | TA_typ t -> TA_typ (t_subst s_env t)
@@ -1375,14 +1378,16 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 =
   | Tabbrev(_,t1),Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
   | Tabbrev(_,t1),_ -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
   | _,Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2
-  | Toptions(to1,to2),_ -> 
+  | Toptions(to1,Some to2),_ -> 
     if (conforms_to_t false to1 t2 || conforms_to_t false to2 t2)
     then begin t1.t <- t2.t; (t2,csp,e) end
     else eq_error l ("Neither " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2))
-  | _,Toptions(to1,to2) -> 
+  | Toptions(to1,None),_ -> (t2,csp,e)
+  | _,Toptions(to1,Some to2) -> 
     if (conforms_to_t false to1 t1 || conforms_to_t false to2 t1)
     then begin t2.t <- t1.t; (t1,csp,e) end
     else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2))
+  | _,Toptions(to1,None) -> (t1,csp,e)
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -1529,7 +1534,8 @@ let rec select_overload_variant d_env params_check get_all variants actual_type
 	  let is_matching = 
 	    if params_check then conforms_to_t true a actual_type 
 	    else match actual_type.t with
-	      | Toptions(at1,at2) -> (conforms_to_t false at1 r || conforms_to_t false at2 r)
+	      | Toptions(at1,Some at2) -> (conforms_to_t false at1 r || conforms_to_t false at2 r)
+	      | Toptions(at1,None) -> conforms_to_t false at1 r
 	      | _ -> conforms_to_t true actual_type r in
 	  if is_matching 
 	  then (Base(([],t),tag,cs@cs',ef))::(if get_all then (recur ()) else [])
diff --git a/src/type_internal.mli b/src/type_internal.mli
index a228750f..5203f51e 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -32,7 +32,7 @@ and t_aux =
   | Ttup of t list (* concrete: no t can be fn *)
   | Tapp of string * t_arg list (* concrete *)
   | Tabbrev of t * t (* first t is the specified type, which may itself be an abbrev; second is the ground type, never an abbrev *)
-  | Toptions of t * t (* used in overload or cast to specify a set of types to expect; first is always concrete. Should never appear after type checking *)
+  | Toptions of t * t option (* used in overload or cast to specify a set of types to expect; first is always concrete. Should never appear after type checking *)
   | Tuvar of t_uvar
 and nexp = { mutable nexp : nexp_aux }
 and nexp_aux =