Add mapping compleness check test case

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;

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)