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)

4 files changed, 129 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
diff --git a/test/coq/pass/irref.sail b/test/coq/pass/irref.sail
new file mode 100644
index 00000000..49ae4488
--- /dev/null
+++ b/test/coq/pass/irref.sail
@@ -0,0 +1,79 @@
+/* For checking that the rewriting pass to remove guards correctly notices
+   that irrefutable patterns (e.g, (_,_) ) subsume wildcards.  For best
+   results, check the test function evaluates to true. */
+
+default Order dec
+
+$include <prelude.sail>
+
+enum enumsingle = A
+enum enumdouble = B | C
+
+val f : (int,enumsingle, enumdouble) -> int
+
+function f(x,p,q) = {
+  let a : int = match (x,p) { (x,_) if x > 0 => 1, _ => 2 };
+  let b : int = match (x,p) { (x,A) if x > 0 => 1, _ => 2 };
+  let c : int = match (x,q) { (x,_) if x > 0 => 1, _ => 2 };
+  let d : int = match (x,q) { (x,B) if x > 0 => 1, _ => 2 };
+  a + b + c + d
+}
+
+/* FIXME
+val two : forall ('t : Type). 't -> int
+
+function two _ = 2
+
+val f' : (int,enumsingle, enumdouble) -> int
+
+function f'(x,p,q) = {
+  let a : int = match (x,p) { (x,_) if x > 0 => 1, z => two(z) };
+  let b : int = match (x,p) { (x,A) if x > 0 => 1, z => two(z) };
+  let c : int = match (x,q) { (x,_) if x > 0 => 1, z => two(z) };
+  let d : int = match (x,q) { (x,B) if x > 0 => 1, z => two(z) };
+  a + b + c + d
+}
+also commented out in test... */
+
+union unionsingle = { D : int }
+union uniondouble = { E : int, F : int }
+
+val g : (int,unionsingle) -> int
+
+function g(x,p) = {
+  let a : int = match (x,p) { (x,_) if x > 0 => 1, _ => 2};
+  let b : int = match (x,p) { (x,D(_)) if x > 0 => 1, _ => 2};
+  let c : int = match (x,p) { (x,D(5)) if x > 0 => 1, _ => 2};
+  a+b+c
+}
+
+val h : (int,uniondouble) -> int
+
+function h(x,p) = {
+  let a : int = match (x,p) { (x,_) if x > 0 => 1, _ => 2};
+  let b : int = match (x,p) { (x,E(_)) if x > 0 => 1, _ => 2};
+  let c : int = match (x,p) { (x,E(5)) if x > 0 => 1, _ => 2};
+  a + b + c
+}
+
+val test : unit -> bool
+
+function test () =
+  f(0,A,B) == 8 &
+  f(1,A,B) == 4 &
+  f(0,A,C) == 8 &
+  f(1,A,C) == 5 &
+/*  f'(0,A,B) == 8 &
+  f'(1,A,B) == 4 &
+  f'(0,A,C) == 8 &
+  f'(1,A,C) == 5 &*/
+  g(0,D(0)) == 6 &
+  g(0,D(5)) == 6 &
+  g(1,D(0)) == 4 &
+  g(1,D(5)) == 3 &
+  h(0,E(0)) == 6 &
+  h(0,E(5)) == 6 &
+  h(0,F(5)) == 6 &
+  h(1,E(0)) == 4 &
+  h(1,E(5)) == 3 &
+  h(1,F(5)) == 5