summaryrefslogtreecommitdiff
path: root/test/typecheck
diff options
context:
space:
mode:
authorThomas Bauereiss2018-01-31 17:56:53 +0000
committerThomas Bauereiss2018-01-31 17:56:53 +0000
commit0e42ceae97d254a4ce51c67463828af9b04157a4 (patch)
tree7a1779d13387ca2b61b697935d04376652c1bb97 /test/typecheck
parent24e3aa017b25be6eaf68bab1718ffa4bdcb1a44a (diff)
Fix bug in bitvector pattern rewriting
Make rewriter look into P_typ patterns instead of throwing them away.
Diffstat (limited to 'test/typecheck')
-rw-r--r--test/typecheck/pass/decode_patterns.sail3
1 files changed, 3 insertions, 0 deletions
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