diff options
| -rw-r--r-- | src/rewrites.ml | 40 |
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 |