From 78a0c43a9c7b41d728f0b6c7d5acccb9b786852e Mon Sep 17 00:00:00 2001
From: trdthg <trdthg@gmail.com>
Date: Sat, 27 Jul 2024 11:07:19 +0800
Subject: [PATCH] Add mapping compleness check test case

---
 src/lib/effects.ml                         |  4 +++-
 test/pattern_completeness/mapping_let.sail | 10 ++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test/pattern_completeness/mapping_let.sail

diff --git a/src/lib/effects.ml b/src/lib/effects.ml
index e61bff383..4485b26fc 100644
--- a/src/lib/effects.ml
+++ b/src/lib/effects.ml
@@ -218,7 +218,9 @@ let infer_def_direct_effects asserts_termination def =
               effects := EffectSet.add IncompleteMatch !effects
         | None -> Reporting.unreachable l __POS__ "Empty funcls in infer_def_direct_effects"
       end
-    | DEF_aux (DEF_mapdef _, _) -> effects := EffectSet.add IncompleteMatch !effects
+    | DEF_aux (DEF_mapdef _, def_annot) ->
+        if Option.is_some (get_def_attribute "incomplete" def_annot) then
+          effects := EffectSet.add IncompleteMatch !effects
     | DEF_aux (DEF_scattered _, _) -> effects := EffectSet.add Scattered !effects
     | _ -> ()
   end;
diff --git a/test/pattern_completeness/mapping_let.sail b/test/pattern_completeness/mapping_let.sail
new file mode 100644
index 000000000..680035862
--- /dev/null
+++ b/test/pattern_completeness/mapping_let.sail
@@ -0,0 +1,10 @@
+struct bool2 = {
+    field: bool,
+}
+
+mapping m : bool <-> bool2 = {
+   true <-> struct { field = true },
+   false <->  struct{ field = false },
+}
+
+let a = m(true)