1 files changed, 37 insertions, 3 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml
index aee57977..47c7e923 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4048,7 +4048,15 @@ let rewrite_defs_realise_mappings (Defs defs) =
    Assumes that guards, vector patterns, etc have been rewritten already,
    and the scattered functions have been merged.
    Will add escape effect where a default is needed, so effects will
-   need recalculated afterwards. *)
+   need recalculated afterwards.
+
+   Also detects and removes redundant wildcard patterns at the end of the match.
+   (We could do more, but this is sufficient to deal with the code generated by
+   the mappings rewrites.)
+
+   Note: if this naive implementation turns out to be too slow or buggy, we
+   could look at implementing Maranget JFP 17(3), 2007.
+ *)
 
 let opt_coq_warn_nonexhaustive = ref false
 
@@ -4266,12 +4274,38 @@ let process_pexp env =
      raise (Reporting_basic.err_unreachable l
               "Guarded pattern should have been rewritten away")
 
+(* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
+let check_cases process is_wild loc_of cases =
+  let rec aux rps acc = function
+    | [] -> acc, rps
+    | [p] when is_wild p && match rps with [] -> true | _ -> false ->
+      let () = Reporting_basic.print_err false false
+        (loc_of p) "Match checking" "Redundant wildcard clause" in
+      acc, []
+    | h::t -> aux (process rps h) (h::acc) t
+  in
+  let cases, rps = aux [RP_any] [] cases in
+  List.rev cases, rps
+
+let pexp_is_wild = function
+  | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true
+  | _ -> false
+
+let pexp_loc = function
+  | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l
+  | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l
+
+let funcl_is_wild = function
+  | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp
+
+let funcl_loc (FCL_aux (_,(l,_))) = l
+
 let rewrite_case (e,ann) =
   match e with
   | E_case (e1,cases) ->
      begin
      let env = env_of_annot ann in
-     let rps = List.fold_left (process_pexp env) [RP_any] cases in
+     let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in
      match rps with
      | [] -> E_aux (E_case (e1,cases),ann)
      | (example::_) ->
@@ -4299,7 +4333,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
   in
   let env = env_of_annot fcl_ann in
   let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in
-  let rps = List.fold_left process_funcl [RP_any] fcls in
+  let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in
   let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) ->
                                   FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann))
                 fcls in