Dynamic layout for inexhaustive case/indeterminately match case

src/haz3lcore/dynamics/DH.re

@@ -33,6 +33,7 @@ module rec DHExp: {
     | Prj(t, int)
     | Constructor(string)
     | ConsistentCase(case)
+    | InexhaustiveCase(MetaVar.t, HoleInstanceId.t, case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
@@ -87,6 +88,7 @@ module rec DHExp: {
     | Prj(t, int)
     | Constructor(string)
     | ConsistentCase(case)
+    | InexhaustiveCase(MetaVar.t, HoleInstanceId.t, case)
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
@@ -126,6 +128,7 @@ module rec DHExp: {
     | Prj(_) => "Prj"
     | Constructor(_) => "Constructor"
     | ConsistentCase(_) => "ConsistentCase"
+    | InexhaustiveCase(_, _, _) => "InexhaustiveCase"
     | InconsistentBranches(_, _, _) => "InconsistentBranches"
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
@@ -174,6 +177,12 @@ module rec DHExp: {
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
       )
+    | InexhaustiveCase(u, i, Case(scrut, rules, n)) =>
+      InexhaustiveCase(
+        u,
+        i,
+        Case(strip_casts(scrut), List.map(strip_casts_rule, rules), n),
+      )
     | InconsistentBranches(u, i, Case(scrut, rules, n)) =>
       InconsistentBranches(
         u,
@@ -284,15 +293,17 @@ module rec DHExp: {
     | (
         InconsistentBranches(u1, i1, case1),
         InconsistentBranches(u2, i2, case2),
-      ) =>
+      )
+    | (InexhaustiveCase(u1, i1, case1), InexhaustiveCase(u2, i2, case2)) =>
       u1 == u2 && i1 == i2 && fast_equal_case(case1, case2)
     | (EmptyHole(_), _)
     | (NonEmptyHole(_), _)
     | (ExpandingKeyword(_), _)
     | (FreeVar(_), _)
     | (InvalidText(_), _)
     | (Closure(_), _)
-    | (InconsistentBranches(_), _) => false
+    | (InconsistentBranches(_), _)
+    | (InexhaustiveCase(_), _) => false
     };
   }
   and fast_equal_case = (Case(d1, rules1, i1), Case(d2, rules2, i2)) => {

src/haz3lcore/dynamics/Elaborator.re

@@ -69,6 +69,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
       }
     /* Forms with special ana rules but no particular typing requirements */
     | ConsistentCase(_)
+    | InexhaustiveCase(_)
     | InconsistentBranches(_)
     | Sequence(_)
     | Let(_)
@@ -271,7 +272,11 @@ let rec dhexp_of_uexp =
         | InHole(
             InexhaustiveMatch(Some(Common(Inconsistent(Internal(_))))),
           ) =>
+          // TODO: review
+          // If multiple errors are associated with a case expression,
+          // DHExp.InconsistentBranches is prioritized.
           DHExp.InconsistentBranches(id, 0, d)
+        | InHole(InexhaustiveMatch(_)) => DHExp.InexhaustiveCase(id, 0, d)
         | _ => ConsistentCase(d)
         };
       | TyAlias(_, _, e) => dhexp_of_uexp(m, e)

src/haz3lcore/dynamics/Evaluator.re

@@ -304,6 +304,7 @@ and matches_cast_Sum =
   | BinFloatOp(_)
   | BinStringOp(_)
   | InconsistentBranches(_)
+  | InexhaustiveCase(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
   | FailedCast(_, _, _)
@@ -409,6 +410,7 @@ and matches_cast_Tuple =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -544,6 +546,7 @@ and matches_cast_Cons =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -988,6 +991,11 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
       Indet(Closure(env, InconsistentBranches(u, i, Case(d1, rules, n))))
       |> return
 
+    | InexhaustiveCase(u, i, Case(d1, rules, n)) =>
+      //TODO: revisit this, consider some kind of dynamic casting
+      Indet(Closure(env, InexhaustiveCase(u, i, Case(d1, rules, n))))
+      |> return
+
     | EmptyHole(u, i) => Indet(Closure(env, EmptyHole(u, i))) |> return
 
     | NonEmptyHole(reason, u, i, d1) =>

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -150,6 +150,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | BoundVar(_)
   | Let(_)
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | Fun(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -412,6 +413,13 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* i = hii_add_instance(u, env);
     Closure(env, InconsistentBranches(u, i, Case(scrut, rules, case_i)))
     |> return;
+
+  | InexhaustiveCase(u, _, Case(scrut, rules, case_i)) =>
+    let* scrut = pp_uneval(env, scrut);
+    let* rules = pp_uneval_rules(env, rules);
+    let* i = hii_add_instance(u, env);
+    Closure(env, InexhaustiveCase(u, i, Case(scrut, rules, case_i)))
+    |> return;
   }
 
 and pp_uneval_rules =
@@ -501,7 +509,8 @@ let rec track_children_of_hole =
   | NonEmptyHole(_, u, i, d) =>
     let hii = track_children_of_hole(hii, parent, d);
     hii |> HoleInstanceInfo.add_parent((u, i), parent);
-  | InconsistentBranches(u, i, Case(scrut, rules, _)) =>
+  | InconsistentBranches(u, i, Case(scrut, rules, _))
+  | InexhaustiveCase(u, i, Case(scrut, rules, _)) =>
     let hii = track_children_of_hole(hii, parent, scrut);
     let hii = track_children_of_hole_rules(hii, parent, rules);
     hii |> HoleInstanceInfo.add_parent((u, i), parent);

src/haz3lcore/dynamics/Substitution.re

@@ -89,6 +89,10 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);
     ConsistentCase(Case(d3, rules, n));
+  | InexhaustiveCase(u, i, Case(d3, rules, n)) =>
+    let d3 = subst_var(d1, x, d3);
+    let rules = subst_var_rules(d1, x, rules);
+    InexhaustiveCase(u, i, Case(d3, rules, n));
   | InconsistentBranches(u, i, Case(d3, rules, n)) =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);

src/haz3lweb/view/dhcode/DHCode.re

@@ -72,11 +72,16 @@ let view_of_layout = (~font_metrics: FontMetrics.t, l: DHLayout.t): Node.t => {
                  ds,
                )
              | VarHole(_) => ([with_cls("InVarHole", txt)], ds)
+             | MismatchedRuleDecoration => (
+                 [with_cls("MismatchedRuleDecoration", txt)],
+                 ds,
+               )
              | Invalid((_, (-666))) =>
                /* Evaluation and Elaboration exceptions */
                ([with_cls("exception", txt)], ds)
              | NonEmptyHole(_)
              | InconsistentBranches(_)
+             | InexhaustiveCase(_)
              | Invalid(_) =>
                let offset = start.col - indent;
                let decoration =

src/haz3lweb/view/dhcode/layout/DHAnnot.re

@@ -12,8 +12,10 @@ type t =
   | NonEmptyHole(ErrStatus.HoleReason.t, HoleInstance.t)
   | VarHole(VarErrStatus.HoleReason.t, HoleInstance.t)
   | InconsistentBranches(HoleInstance.t)
+  | InexhaustiveCase(HoleInstance.t)
   | Invalid(HoleInstance.t)
   | FailedCastDelim
   | FailedCastDecoration
   | CastDecoration
-  | OperationError(InvalidOperationError.t);
+  | OperationError(InvalidOperationError.t)
+  | MismatchedRuleDecoration;

src/haz3lweb/view/dhcode/layout/DHAnnot.rei

@@ -11,8 +11,10 @@ type t =
   | NonEmptyHole(ErrStatus.HoleReason.t, HoleInstance.t)
   | VarHole(VarErrStatus.HoleReason.t, HoleInstance.t)
   | InconsistentBranches(HoleInstance.t)
+  | InexhaustiveCase(HoleInstance.t)
   | Invalid(HoleInstance.t)
   | FailedCastDelim
   | FailedCastDecoration
   | CastDecoration
-  | OperationError(InvalidOperationError.t);
+  | OperationError(InvalidOperationError.t)
+  | MismatchedRuleDecoration;

src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re

@@ -66,6 +66,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | Let(_)
   | FixF(_)
   | ConsistentCase(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => DHDoc_common.precedence_max
   | BinBoolOp(op, _, _) => precedence_bin_bool_op(op)
   | BinIntOp(op, _, _) => precedence_bin_int_op(op)
@@ -93,6 +94,7 @@ let mk_bin_float_op = (op: TermBase.UExp.op_bin_float): DHDoc.t =>
 let mk_bin_string_op = (op: TermBase.UExp.op_bin_string): DHDoc.t =>
   Doc.text(TermBase.UExp.string_op_to_string(op));
 
+// DHExp is annotated here
 let rec mk =
         (
           ~settings: Settings.Evaluation.t,
@@ -122,7 +124,7 @@ let rec mk =
           : (DHDoc.t, option(Typ.t)) => {
     open Doc;
     let go' = go(~enforce_inline);
-    let go_case = (dscrut, drs) =>
+    let go_case = (dscrut, drs, current_rule_index) =>
       if (enforce_inline) {
         fail();
       } else {
@@ -137,7 +139,15 @@ let rec mk =
         vseps(
           List.concat([
             [hcat(DHDoc_common.Delim.open_Case, scrut_doc)],
-            drs |> List.map(mk_rule(~settings, ~selected_hole_instance)),
+            drs
+            |> List.mapi((i, rule) =>
+                 mk_rule(
+                   ~settings,
+                   ~selected_hole_instance,
+                   ~crossed_out=i < current_rule_index,
+                   rule,
+                 )
+               ),
             [DHDoc_common.Delim.close_Case],
           ]),
         );
@@ -173,7 +183,10 @@ let rec mk =
         text(x) |> annot(DHAnnot.VarHole(Free, (u, i)))
       | InvalidText(u, i, t) => DHDoc_common.mk_InvalidText(t, (u, i))
       | InconsistentBranches(u, i, Case(dscrut, drs, _)) =>
-        go_case(dscrut, drs) |> annot(DHAnnot.InconsistentBranches((u, i)))
+        go_case(dscrut, drs, 0)
+        |> annot(DHAnnot.InconsistentBranches((u, i)))
+      | InexhaustiveCase(u, i, Case(dscrut, drs, _)) =>
+        go_case(dscrut, drs, 0) |> annot(DHAnnot.InexhaustiveCase((u, i)))
       | BoundVar(x) => text(x)
       | Constructor(name) => DHDoc_common.mk_ConstructorLit(name)
       | BoolLit(b) => DHDoc_common.mk_BoolLit(b)
@@ -237,7 +250,8 @@ let rec mk =
       | Tuple(ds) =>
         DHDoc_common.mk_Tuple(ds |> List.map(d => mk_cast(go'(d))))
       | Prj(d, n) => DHDoc_common.mk_Prj(mk_cast(go'(d)), n)
-      | ConsistentCase(Case(dscrut, drs, _)) => go_case(dscrut, drs)
+      | ConsistentCase(Case(dscrut, drs, current_rule_index)) =>
+        go_case(dscrut, drs, current_rule_index)
       | Cast(d, _, _) =>
         let (doc, _) = go'(d);
         doc;
@@ -369,7 +383,12 @@ let rec mk =
   mk_cast(go(~parenthesize, ~enforce_inline, d));
 }
 and mk_rule =
-    (~settings, ~selected_hole_instance, Rule(dp, dclause): DHExp.rule)
+    (
+      ~settings,
+      ~selected_hole_instance,
+      ~crossed_out,
+      Rule(dp, dclause): DHExp.rule,
+    )
     : DHDoc.t => {
   open Doc;
   let mk' = mk(~settings, ~selected_hole_instance);
@@ -384,7 +403,8 @@ and mk_rule =
           ]),
         ])
       : hcat(space(), hidden_clause);
-  hcats([
+  // temporary name
+  let r = [
     DHDoc_common.Delim.bar_Rule,
     DHDoc_Pat.mk(dp)
     |> DHDoc_common.pad_child(
@@ -393,5 +413,8 @@ and mk_rule =
        ),
     DHDoc_common.Delim.arrow_Rule,
     clause_doc,
-  ]);
+  ];
+  let r =
+    crossed_out ? List.map(annot(DHAnnot.MismatchedRuleDecoration), r) : r;
+  hcats(r);
 };

src/haz3lweb/www/style.css

@@ -1562,6 +1562,11 @@ svg.expandable path {
   color: var(--err-color)
 }
 
+.DHCode .MismatchedRuleDecoration {
+  text-decoration: line-through;
+  opacity: 0.5;
+}
+
 .DHCode .EmptyHole {
   background-color: #ac9a6a;
   border-radius: 0.2em;