diff options
| author | Brian Campbell | 2018-08-13 13:52:50 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-13 13:52:50 +0100 |
| commit | 3001c5dbdfbd060500df141d8112af5c1021f347 (patch) | |
| tree | b34d27886fb299f75a83319902dade337ea619db /src | |
| parent | 0de3a32ed759773bf1e8ff4460d21371c0a715e8 (diff) | |
Guarded clauses rewrite: variable patterns subsume enums
Prevents redundant clauses.
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 825073b4..aee57977 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) = | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2 | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) -> if id1 = id2 then Some [] - else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound && - Env.lookup_id aid2 (env_of_annot annot2) = Unbound - then Some [(id2,id1)] else None + else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound + then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound + then Some [(id2,id1)] + else Some [] + else None | P_id id1, _ -> if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2 |