From 4567b1f2fcdbf6eb58b677ff25679c45734e1182 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Mon, 6 May 2024 18:37:04 +0100 Subject: [PATCH] Make sure P_vector_subrange ids are returned by check_pattern_duplicates --- src/lib/type_check.ml | 2 +- src/lib/type_error.mli | 1 + test/typecheck/pass/vector_subrange_mapping.sail | 11 +++++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 test/typecheck/pass/vector_subrange_mapping.sail diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 913675a00..6f2fbd696 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -1600,7 +1600,7 @@ let check_pattern_duplicates env pat = Err_other "Regular binding is here" ) ) - | None -> () + | None -> ids := Bindings.add subrange_id (Pattern_singleton l) !ids ) !subrange_ids; !ids diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli index e348892c1..1aed09883 100644 --- a/src/lib/type_error.mli +++ b/src/lib/type_error.mli @@ -119,6 +119,7 @@ val analyze_unresolved_quant : val string_of_type_error : type_error -> string * string option +(** Convert a type error into a general purpose error from the Reporting file *) val to_reporting_exn : Parse_ast.l -> type_error -> exn val check_defs : Type_check.Env.t -> uannot Ast.def list -> Type_check.tannot Ast.def list * Type_check.Env.t diff --git a/test/typecheck/pass/vector_subrange_mapping.sail b/test/typecheck/pass/vector_subrange_mapping.sail new file mode 100644 index 000000000..06d454d96 --- /dev/null +++ b/test/typecheck/pass/vector_subrange_mapping.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +union Foo = { + Bar : bits(32) +} + +mapping baz : Foo <-> bits(32) = { + Bar(imm) <-> imm[31 .. 16] @ imm[15 .. 0] +}