Use type information in vector concatenation pattern matching in interpreter.

Does not properly bind variables (i.e. in the pattern 0b01:(bit[3]) a: 0b0001 subsequent uses of a will not be bound in the interpreter, though they are in the type checker), so until bug is fixed, treat all such identifiers as _

2 files changed, 42 insertions, 2 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 64727503..733c32d0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -519,10 +519,45 @@ let rec match_pattern (P_aux p _) value =
    | V_vector n inc vals ->
      let (matched_p,bounds,remaining_vals) =
        List.foldl 
-         (fun (matched_p,bounds,r_vals) (P_aux pat _) ->
+         (fun (matched_p,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
            match pat with
+	   | P_lit (L_aux (L_bin bin_string) l') ->
+	     let bin_chars = toCharList bin_string in
+	     let binpats = List.map (fun b -> P_aux (match b with | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
+	     vec_concat_match binpats r_vals
            | P_vector pats -> vec_concat_match pats r_vals
-           | P_id id -> (false,[],[]) (*Need to have at least a guess of how many to consume*)
+           | P_id id -> (match t with
+	       | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+		 let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+		 vec_concat_match wilds r_vals (*TODO need to add to bounds*)
+	       | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+		 (false,[],[]) (*TODO see if can have some constraint bounds here*)
+	       | _ -> (false,[],[]) end)
+	   | P_wild -> (match t with
+	       | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+		 let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+		 vec_concat_match wilds r_vals (*TODO need to add to bounds*)
+	       | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+		 (false,[],[]) (*TODO see if can have some constraint bounds here*)
+	       | _ -> (false,[],[]) end)
+	   | P_typ _ (P_aux p (l',Just(t',_,_,_))) ->
+	     (match p with
+	       | P_vector pats -> vec_concat_match pats r_vals
+	       | P_id id -> (match t with
+		   | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+		     let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+		     vec_concat_match wilds r_vals (*TODO need to add to bounds*)
+		   | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+		     (false,[],[]) (*TODO see if can have some constraint bounds here*)
+		   | _ -> (false,[],[]) end)
+	       | P_wild -> (match t with
+		   | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+		     let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+		     vec_concat_match wilds r_vals (*TODO need to add to bounds*)
+		   | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
+		     (false,[],[]) (*TODO see if can have some constraint bounds here*)
+		   | _ -> (false,[],[]) end)
+	       | _ -> (false,[],[]) end) (*TODO Need to support indexed here, skipping intermediate numbers but consumming r_vals *)
            | _ -> (false,[],[]) end) (true,[],vals) pats in
      if matched_p && ([] = remaining_vals) then (matched_p,bounds) else (false,[]) 
    | _ -> (false, []) 
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
index 7bbfebf9..cabe7dad 100644
--- a/src/test/pattern.sail
+++ b/src/test/pattern.sail
@@ -23,6 +23,11 @@ function nat main _ = {
     case 32 -> { x:= 128; }
   };
 
+  switch 0b010101 {
+    case (0b01:(bit[1]) _:0b101) -> n:= 42
+    case _ -> n:=0
+  };
+
   n := 3;
   switch n {
     case 0 -> { 21 }