diff options
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/decode_patterns.sail | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 074ad60f..6d0fa832 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1214,6 +1214,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = | Some (l,i,j,lits) -> Some (l,i,idx,lits @ [e]) | None -> Some (l,idx,idx,[e])) in collect current' (guards, dls) idx' ps' + | P_aux (P_typ (typ, pat'), _) -> + collect current (guards, dls) idx (pat' :: ps') | P_aux (P_as (pat',id), (l,annot)) -> let dl = letbind_bit_exp rootid l t idx id in collect current (guards, dls @ [dl]) idx (pat' :: ps') diff --git a/test/typecheck/pass/decode_patterns.sail b/test/typecheck/pass/decode_patterns.sail index 486634b8..d8b17f5b 100644 --- a/test/typecheck/pass/decode_patterns.sail +++ b/test/typecheck/pass/decode_patterns.sail @@ -11,6 +11,9 @@ overload operator == = {eq_anything} val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) +val vector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. + (bits('n), atom('m)) -> bit + val decode : vector(16, dec, bit) -> unit scattered function decode |