Check mapping completeness

Add basic mapdef completeness check, converting mpat to pat, then to gpat, and finally reusing the match checking logic

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;

src/lib/pattern_completeness.ml

@@ -953,4 +953,103 @@ module Make (C : Config) = struct
 
   let is_complete ?(keyword = "match") l ctx cases head_exp_typ =
     Option.is_some (is_complete_wildcarded ~keyword l ctx cases head_exp_typ)
+
+  let rec pat_of_mpat mpat =
+    match mpat with
+    | MP_aux (mpat_aux, l) ->
+        let res =
+          match mpat_aux with
+          | MP_lit lit -> P_lit lit
+          | MP_id id -> P_id id
+          | MP_app (id, mpat_list) -> P_app (id, List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector mpat_list -> P_vector (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector_concat mpat_list -> P_vector_concat (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector_subrange (id, l, r) -> P_vector_subrange (id, l, r)
+          | MP_tuple mpat_list -> P_tuple (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_list mpat_list -> P_list (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_cons (mpat1, mpat2) -> P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2)
+          | MP_string_append mpat_list -> P_string_append (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_typ (mp1, atyp) -> P_typ (atyp, pat_of_mpat mp1)
+          | MP_struct id_mpat_list ->
+              let fpl = List.map (fun (id, mpat) -> (id, pat_of_mpat mpat)) id_mpat_list in
+              P_struct (fpl, FP_no_wild)
+          | MP_as (mpat, id) -> (
+              match pat_of_mpat mpat with P_aux (pat, _id) -> pat
+            )
+        in
+        P_aux (res, l)
+
+  let is_complete_gpats ?(keyword = "match") l ctx have_guard gpats_matrix =
+    let res =
+      match matrix_is_complete l ctx gpats_matrix with
+      | Incomplete (unmatched :: _) ->
+          let guard_info = if have_guard then " by unguarded patterns" else "" in
+          Reporting.warn "Incomplete pattern match statement at" (shrink_loc keyword l)
+            ("The following expression is unmatched" ^ guard_info ^ ": "
+            ^ (string_of_exp unmatched |> Util.yellow |> Util.clear)
+            );
+          false
+      | Incomplete [] -> Reporting.unreachable l __POS__ "Got unmatched pattern matrix without witness" [@coverage off]
+      | Complete cinfo ->
+          (* let wildcarded_pats = List.map (fun (_, pat) -> insert_wildcards cinfo pat) pats in *)
+          List.iter
+            (fun (idx, _) ->
+              if IntSet.mem idx.num cinfo.redundant then
+                Reporting.warn "Redundant case" idx.loc "This match case is never used"
+            )
+            (rows_to_list gpats_matrix);
+          true
+      | Completeness_unknown -> false
+    in
+    res
+
+  let is_complete_mapcls_wildcarded ?(keyword = "match") l ctx mapcls typl typr =
+    let have_guard = false in
+    let rec lpat_of_mapcl mapcl left =
+      (* We don't consider guarded cases *)
+      let pat_of_mpexp = function
+        | MPat_aux (mpexp_aux, l) -> (
+            match mpexp_aux with MPat_when (mpat, exp) -> None | MPat_pat mpat -> Some (pat_of_mpat mpat)
+          )
+      in
+      let rec pexp_to_pat = function
+        | Pat_aux (Pat_exp ((P_aux (_, (l, _)) as pat), _), _) -> Some pat
+        | Pat_aux (Pat_when _, _) -> None
+      in
+      match mapcl with
+      | MCL_aux (mapcl_aux, _) ->
+          if left then (
+            match mapcl_aux with
+            | MCL_bidir (mpexp, _) -> pat_of_mpexp mpexp
+            | MCL_forwards pexp -> pexp_to_pat pexp
+            | MCL_backwards pexp -> None
+          )
+          else (
+            match mapcl_aux with
+            | MCL_bidir (_, mpexp) -> pat_of_mpexp mpexp
+            | MCL_forwards pexp -> None
+            | MCL_backwards pexp -> pexp_to_pat pexp
+          )
+    in
+    let rec opt_cases_to_pats from have_guard = function
+      | [] -> (have_guard, [])
+      | Some (P_aux (_, (l, _)) as pat) :: cases ->
+          let pat, from = number_pat from pat in
+          let have_guard, pats = opt_cases_to_pats from have_guard cases in
+          (have_guard, (l, pat) :: pats)
+      | _ :: cases -> opt_cases_to_pats from true cases
+    in
+    (* prepare left *)
+    let lpats = List.map (fun mapcl -> lpat_of_mapcl mapcl true) mapcls in
+    let _, lpats = opt_cases_to_pats 0 have_guard lpats in
+    let lmatrix =
+      Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typl) pat])) lpats)
+    in
+    (* prepare right *)
+    let rpats = List.map (fun mapcl -> lpat_of_mapcl mapcl false) mapcls in
+    let _, rpats = opt_cases_to_pats 0 have_guard rpats in
+    let rmatrix =
+      Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typr) pat])) rpats)
+    in
+    is_complete_gpats l ctx have_guard lmatrix && is_complete_gpats l ctx have_guard rmatrix
 end

src/lib/pattern_completeness.mli

@@ -93,4 +93,5 @@ module Make (C : Config) : sig
   val is_complete_funcls_wildcarded :
     ?keyword:string -> Parse_ast.l -> ctx -> C.t funcl list -> typ -> C.t funcl list option
   val is_complete : ?keyword:string -> Parse_ast.l -> ctx -> C.t pexp list -> typ -> bool
+  val is_complete_mapcls_wildcarded : ?keyword:string -> Parse_ast.l -> ctx -> C.t mapcl list -> typ -> typ -> bool
 end

src/lib/type_check.ml

@@ -4566,6 +4566,12 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls)
     env
   )
 
+let check_mapdef_completeness l env mapcls typl typr =
+  let ctx = pattern_completeness_ctx env in
+  match PC.is_complete_mapcls_wildcarded l ctx mapcls typl typr with
+  | true -> add_def_attribute (gen_loc l) "complete" None
+  | false -> add_def_attribute (gen_loc l) "incomplete" None
+
 let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _))) =
   typ_print (lazy ("\nChecking mapping " ^ string_of_id id));
   let inline_tannot =
@@ -4582,11 +4588,11 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l,
         (Some vs_l, quant, typ)
     | None, None -> typ_error l "Mapping does not have any declared type"
   in
-  begin
+  let typl, typr =
     match typ with
-    | Typ_aux (Typ_bidir (_, _), _) -> ()
+    | Typ_aux (Typ_bidir (l, r), _) -> (l, r)
     | _ -> typ_error l "Mapping type must be a bi-directional mapping"
-  end;
+  in
   (* If we have a val spec, then the mapping itself shouldn't be marked as private *)
   let fix_body_visibility =
     match (have_val_spec, def_annot.visibility) with
@@ -4607,7 +4613,16 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l,
   in
   let mapcl_env = Env.add_typquant l quant env in
   let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in
-  let def_annot = fix_body_visibility def_annot in
+
+  let update_attr =
+    if
+      Option.is_some (get_def_attribute "complete" def_annot)
+      || Option.is_some (get_def_attribute "incomplete" def_annot)
+    then fun attrs -> attrs
+    else check_mapdef_completeness l env mapcls typl typr
+  in
+
+  let def_annot = fix_body_visibility (update_attr def_annot) in
   let env = Env.define_val_spec id env in
   ( vs_def @ [DEF_aux (DEF_mapdef (MD_aux (MD_mapping (id, empty_tannot_opt, mapcls), (l, empty_tannot))), def_annot)],
     env

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)

test/pattern_completeness/warn_mapping.expect

@@ -0,0 +1,6 @@
+Warning: Incomplete pattern match statement at warn_mapping.sail:15.0-5:
+15 |mapping bool_rev3 : bool <-> bool2 = {
+   |^---^
+   | 
+The following expression is unmatched: struct { field = false }
+

test/pattern_completeness/warn_mapping.sail

@@ -0,0 +1,18 @@
+struct bool2 = {
+    field: bool,
+}
+
+mapping bool_rev : bool <-> bool2 = {
+   true <-> struct { field = true },
+   false <->  struct{ field = false },
+}
+
+mapping bool_rev2 : bool <-> bool2 = {
+   true <-> struct { field = false },
+   false <->  struct{ field = true },
+}
+
+mapping bool_rev3 : bool <-> bool2 = {
+   true <-> struct { field = true },
+   false <->  struct{ field = true },
+}

test/pattern_completeness/warn_mapping_l.expect

@@ -0,0 +1,6 @@
+Warning: Incomplete pattern match statement at warn_mapping_l.sail:1.0-5:
+1 |mapping m : bool <-> int = {
+  |^---^
+  | 
+The following expression is unmatched: false
+

test/pattern_completeness/warn_mapping_l.sail

@@ -0,0 +1,3 @@
+mapping m : bool <-> int = {
+   forwards true => 1,
+}

test/pattern_completeness/warn_mapping_r.expect

@@ -0,0 +1,12 @@
+Warning: Deprecated warn_mapping_r.sail:2.3-12:
+2 |   true => 1,
+  |   ^-------^
+  | 
+Single direction mapping clause should be prefixed by a direction, either forwards or backwards
+
+Warning: Incomplete pattern match statement at warn_mapping_r.sail:1.0-5:
+1 |mapping m : bool <-> int = {
+  |^---^
+  | 
+The following expression is unmatched: false
+

test/pattern_completeness/warn_mapping_r.sail

@@ -0,0 +1,4 @@
+mapping m : bool <-> int = {
+   true => 1,
+   backwards 2 => false,
+}