In guarded pattern rewriting, irrefutable patterns subsume wildcards

Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)

3 files changed, 50 insertions, 0 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 1696c727..214ca571 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1007,6 +1007,40 @@ let remove_wildcards pre (P_aux (_,(l,_)) as pat) =
         | (p,annot) -> P_aux (p,annot) }
     pat
 
+let rec is_irrefutable_pattern (P_aux (p,ann)) =
+  match p with
+  | P_lit (L_aux (L_unit,_))
+  | P_wild
+    -> true
+  | P_lit _ -> false
+  | P_as (p1,_)
+  | P_typ (_,p1)
+    -> is_irrefutable_pattern p1
+  | P_id id -> begin
+    match Env.lookup_id id (env_of_annot ann) with
+    | Local _ | Unbound -> true
+    | Register _ -> false (* should be impossible, anyway *)
+    | Enum enum ->
+       match enum with
+       | Typ_aux (Typ_id enum_id,_) ->
+          List.length (Env.get_enum enum_id (env_of_annot ann)) <= 1
+       | _ -> false (* should be impossible, anyway *)
+  end
+  | P_var (p1,_) -> is_irrefutable_pattern p1
+  | P_app (f,args) ->
+     Env.is_singleton_union_constructor f (env_of_annot ann) &&
+       List.for_all is_irrefutable_pattern args
+  | P_record (fps,_) ->
+     List.for_all (fun (FP_aux (FP_Fpat (_,p),_)) -> is_irrefutable_pattern p) fps
+  | P_vector ps
+  | P_vector_concat ps
+  | P_tup ps
+  | P_list ps
+    -> List.for_all is_irrefutable_pattern ps
+  | P_cons (p1,p2) -> is_irrefutable_pattern p1 && is_irrefutable_pattern p2
+  | P_string_append ps
+    -> List.for_all is_irrefutable_pattern ps
+
 (* Check if one pattern subsumes the other, and if so, calculate a
    substitution of variables that are used in the same position.
    TODO: Check somewhere that there are no variable clashes (the same variable
@@ -1057,6 +1091,7 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
     (match subsumes_pat pat1 pat2, subsumes_pat pats1 pats2 with
     | Some substs1, Some substs2 -> Some (substs1 @ substs2)
     | _ -> None)
+  | _, P_wild -> if is_irrefutable_pattern pat1 then Some [] else None
   | _ -> None
 and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
   if id1 = id2 then subsumes_pat pat1 pat2 else None
diff --git a/src/type_check.ml b/src/type_check.ml
index c8920685..fec146a0 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -369,6 +369,7 @@ module Env : sig
   val get_val_spec : id -> t -> typquant * typ
   val get_val_spec_orig : id -> t -> typquant * typ
   val is_union_constructor : id -> t -> bool
+  val is_singleton_union_constructor : id -> t -> bool
   val is_mapping : id -> t -> bool
   val add_record : id -> typquant -> (typ * id) list -> t -> t
   val is_record : id -> t -> bool
@@ -906,6 +907,16 @@ end = struct
     let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in
     List.exists (is_ctor id) type_unions
 
+  let is_singleton_union_constructor id env =
+    let is_ctor id (Tu_aux (tu, _)) = match tu with
+      | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true
+      | _ -> false
+    in
+    let type_unions = List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants) in
+    match List.find (List.exists (is_ctor id)) type_unions with
+    | l -> List.length l = 1
+    | exception Not_found -> false
+
   let is_mapping id env = Bindings.mem id env.mappings
 
   let add_enum id ids env =
diff --git a/src/type_check.mli b/src/type_check.mli
index bcd4eb8b..62fd846e 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -164,6 +164,10 @@ module Env : sig
 
   val is_union_constructor : id -> t -> bool
 
+  (** Check if the id is both a constructor, and the only constructor of that
+      type. *)
+  val is_singleton_union_constructor : id -> t -> bool
+
   val is_mapping : id -> t -> bool
 
   val is_register : id -> t -> bool