diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 39 | ||||
| -rw-r--r-- | src/test/pattern.sail | 5 |
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 } |