Case expression redundancy checking (#1124)

src/haz3lcore/dynamics/Elaborator.re

@@ -302,6 +302,13 @@ let rec dhexp_of_uexp =
 and dhpat_of_upat = (m: Statics.Map.t, upat: Term.UPat.t): option(DHPat.t) => {
   switch (Id.Map.find_opt(Term.UPat.rep_id(upat), m)) {
   | Some(InfoPat({mode, self, ctx, _})) =>
+    // NOTE: for the current implementation, redundancy is considered a static error
+    // but not a runtime error.
+    let self =
+      switch (self) {
+      | Redundant(self) => self
+      | _ => self
+      };
     let err_status = Info.status_pat(ctx, mode, self);
     let maybe_reason: option(ErrStatus.HoleReason.t) =
       switch (err_status) {

src/haz3lcore/statics/Info.re

@@ -72,6 +72,7 @@ type error_exp =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error_pat =
   | ExpectedConstructor /* Only construtors can be applied */
+  | Redundant(option(error_pat))
   | Common(error_common);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -351,8 +352,20 @@ let rec status_common =
     InHole(Inconsistent(Internal(Typ.of_source(tys))))
   };
 
-let status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
+let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
   switch (mode, self) {
+  | (_, Redundant(self)) =>
+    let additional_err =
+      switch (status_pat(ctx, mode, self)) {
+      | InHole(Common(Inconsistent(Internal(_) | Expectation(_))) as err)
+      | InHole(Common(NoType(_)) as err) => Some(err)
+      | NotInHole(_) => None
+      | InHole(Common(Inconsistent(WithArrow(_))))
+      | InHole(ExpectedConstructor | Redundant(_)) =>
+        // ExpectedConstructor cannot be a reason to hole-wrap the entire pattern
+        failwith("InHole(Redundant(impossible_err))")
+      };
+    InHole(Redundant(additional_err));
   | (Syn | Ana(_), Common(self_pat))
   | (SynFun, Common(IsConstructor(_) as self_pat)) =>
     /* Little bit of a hack. Anything other than a bound ctr will, in
@@ -489,11 +502,18 @@ let fixed_typ_ok: ok_pat => Typ.t =
   | Ana(Consistent({join, _})) => join
   | Ana(InternallyInconsistent({ana, _})) => ana;
 
-let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t =>
+let fixed_typ_pat = (ctx, mode: Mode.t, self: Self.pat): Typ.t => {
+  // TODO: get rid of unwrapping (probably by changing the implementation of error_exp.Redundant)
+  let self =
+    switch (self) {
+    | Redundant(self) => self
+    | _ => self
+    };
   switch (status_pat(ctx, mode, self)) {
   | InHole(_) => Unknown(Internal)
   | NotInHole(ok) => fixed_typ_ok(ok)
   };
+};
 
 let fixed_constraint_pat =
     (ctx, mode: Mode.t, self: Self.pat, constraint_: Constraint.t)

src/haz3lcore/statics/Self.re

@@ -46,6 +46,7 @@ type exp =
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type pat =
+  | Redundant(pat)
   | Common(t);
 
 let join_of = (j: join_type, ty: Typ.t): Typ.t =>
@@ -74,9 +75,10 @@ let typ_of_exp: (Ctx.t, exp) => option(Typ.t) =
     | InexhaustiveMatch(_) => None
     | Common(self) => typ_of(ctx, self);
 
-let typ_of_pat: (Ctx.t, pat) => option(Typ.t) =
+let rec typ_of_pat: (Ctx.t, pat) => option(Typ.t) =
   ctx =>
     fun
+    | Redundant(pat) => typ_of_pat(ctx, pat)
     | Common(self) => typ_of(ctx, self);
 
 /* The self of a var depends on the ctx; if the

src/haz3lcore/statics/Statics.re

@@ -366,7 +366,6 @@ and uexp_to_info_map =
           ps,
           m,
         );
-      let p_constraints = List.map(Info.pat_constraint, ps');
       let p_ctxs = List.map(Info.pat_ctx, ps');
       let (es, m) =
         List.fold_left2(
@@ -379,25 +378,44 @@ and uexp_to_info_map =
       let e_co_ctxs =
         List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es));
       /* Add co-ctxs to patterns */
-      let (_, m) =
-        map_m(
-          ((p, co_ctx)) =>
-            go_pat(
-              ~is_synswitch=false,
-              ~co_ctx,
-              ~mode=Mode.Ana(scrut.ty),
-              p,
-            ),
+      let (m, final_constraint) =
+        List.fold_left(
+          ((m, acc_constraint), (p, co_ctx)) => {
+            let (p, m) =
+              go_pat(
+                ~is_synswitch=false,
+                ~co_ctx,
+                ~mode=Mode.Ana(scrut.ty),
+                p,
+                m,
+              );
+            let p_constraint = Info.pat_constraint(p);
+            if (!Incon.is_redundant(p_constraint, acc_constraint)) {
+              (m, Constraint.Or(p_constraint, acc_constraint));
+            } else {
+              let info =
+                Info.derived_pat(
+                  ~upat=p.term,
+                  ~ctx=p.ctx,
+                  ~co_ctx=p.co_ctx,
+                  ~mode=p.mode,
+                  ~ancestors=p.ancestors,
+                  ~self=Redundant(p.self),
+                  // Mark patterns as redundant at the top level
+                  // because redundancy doesn't make sense in a smaller context
+                  ~constraint_=p_constraint,
+                );
+              (
+                // Override the info for the single upat
+                add_info(p.term.ids, InfoPat(info), m),
+                acc_constraint // Redundant patterns are ignored
+              );
+            };
+          },
+          (m, Constraint.Falsity),
           List.combine(ps, e_co_ctxs),
-          m,
         );
-      (
-        es,
-        e_co_ctxs,
-        branch_ids,
-        Constraint.or_constraints(p_constraints),
-        m,
-      );
+      (es, e_co_ctxs, branch_ids, final_constraint, m);
     };
     let (es, e_co_ctxs, branch_ids, final_constraint, m) =
       rules_to_info_map(rules, m);

src/haz3lweb/view/CursorInspector.re

@@ -183,9 +183,15 @@ let rec exp_view = (cls: Term.Cls.t, status: Info.status_exp) =>
   | NotInHole(ok) => div_ok(common_ok_view(cls, ok))
   };
 
-let pat_view = (cls: Term.Cls.t, status: Info.status_pat) =>
+let rec pat_view = (cls: Term.Cls.t, status: Info.status_pat) =>
   switch (status) {
   | InHole(ExpectedConstructor) => div_err([text("Expected a constructor")])
+  | InHole(Redundant(additional_err)) =>
+    switch (additional_err) {
+    | None => div_err([text("Pattern is redundant")])
+    | Some(err) =>
+      div_err([pat_view(cls, InHole(err)), text("; pattern is redundant")])
+    }
   | InHole(Common(error)) => div_err(common_err_view(cls, error))
   | NotInHole(ok) => div_ok(common_ok_view(cls, ok))
   };