From ed3bcc6331f87b6854f721241060b888e9e6dfd4 Mon Sep 17 00:00:00 2001
From: DavidFangWJ <2500097466@qq.com>
Date: Sat, 30 Sep 2023 17:00:58 -0400
Subject: [PATCH 01/10] Added a case `NotExhaustive` to `DHExp.t`.

---
 src/haz3lcore/dynamics/DH.re                 | 13 +++++++++++--
 src/haz3lcore/dynamics/Elaborator.re         |  1 +
 src/haz3lcore/dynamics/Evaluator.re          |  7 +++++++
 src/haz3lcore/dynamics/EvaluatorPost.re      |  9 ++++++++-
 src/haz3lcore/dynamics/Substitution.re       |  4 ++++
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re |  4 +++-
 6 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index 61d7483930..046ad778c2 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -36,6 +36,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | NotExhaustive(case)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -90,6 +91,7 @@ module rec DHExp: {
     | Cast(t, Typ.t, Typ.t)
     | FailedCast(t, Typ.t, Typ.t)
     | InvalidOperation(t, InvalidOperationError.t)
+    | NotExhaustive(case)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -130,6 +132,7 @@ module rec DHExp: {
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
     | InvalidOperation(_) => "InvalidOperation"
+    | NotExhaustive(_) => "NotExhaustive"
     };
 
   let mk_tuple: list(t) => t =
@@ -174,6 +177,10 @@ module rec DHExp: {
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
       )
+    | NotExhaustive(Case(a, rs, b)) =>
+      NotExhaustive(
+        Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
+      )
     | InconsistentBranches(u, i, Case(scrut, rules, n)) =>
       InconsistentBranches(
         u,
@@ -242,7 +249,8 @@ module rec DHExp: {
       fast_equal(d1, d2) && ty11 == ty12 && ty21 == ty22
     | (InvalidOperation(d1, reason1), InvalidOperation(d2, reason2)) =>
       fast_equal(d1, d2) && reason1 == reason2
-    | (ConsistentCase(case1), ConsistentCase(case2)) =>
+    | (ConsistentCase(case1), ConsistentCase(case2))
+    | (NotExhaustive(case1), NotExhaustive(case2)) =>
       fast_equal_case(case1, case2)
     /* We can group these all into a `_ => false` clause; separating
        these so that we get exhaustiveness checking. */
@@ -264,7 +272,8 @@ module rec DHExp: {
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)
-    | (ConsistentCase(_), _) => false
+    | (ConsistentCase(_), _)
+    | (NotExhaustive(_), _) => false
 
     /* Hole forms: when checking environments, only check that
        environment ID's are equal, don't check structural equality.
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 47e2d484c2..7f8e168b85 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/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(_)
+    | NotExhaustive(_)
     | InconsistentBranches(_)
     | Sequence(_)
     | Let(_)
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index 529ca04260..c95993467f 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -320,6 +320,7 @@ and matches_cast_Sum =
   | Tuple(_)
   | Prj(_)
   | ConsistentCase(_)
+  | NotExhaustive(_)
   | Sequence(_, _)
   | Closure(_)
   | TestLit(_)
@@ -409,6 +410,7 @@ and matches_cast_Tuple =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | NotExhaustive(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -544,6 +546,7 @@ and matches_cast_Cons =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
+  | NotExhaustive(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -988,6 +991,10 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
       Indet(Closure(env, InconsistentBranches(u, i, Case(d1, rules, n))))
       |> return
 
+    // TODO: Imitation of the last, may need to change as well.
+    | NotExhaustive(Case(d1, rules, n)) =>
+      Indet(Closure(env, NotExhaustive(Case(d1, rules, n)))) |> return
+
     | EmptyHole(u, i) => Indet(Closure(env, EmptyHole(u, i))) |> return
 
     | NonEmptyHole(reason, u, i, d1) =>
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 18d4ea2b44..4f76853748 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -150,6 +150,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | BoundVar(_)
   | Let(_)
   | ConsistentCase(_)
+  | NotExhaustive(_)
   | Fun(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -377,6 +378,11 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* rules' = pp_uneval_rules(env, rules);
     ConsistentCase(Case(scrut', rules', i)) |> return;
 
+  | NotExhaustive(Case(scrut, rules, i)) =>
+    let* scrut' = pp_uneval(env, scrut);
+    let* rules' = pp_uneval_rules(env, rules);
+    NotExhaustive(Case(scrut', rules', i)) |> return;
+
   /* Closures shouldn't exist inside other closures */
   | Closure(_) => raise(Exception(ClosureInsideClosure))
 
@@ -481,7 +487,8 @@ let rec track_children_of_hole =
       hii,
     )
 
-  | ConsistentCase(Case(scrut, rules, _)) =>
+  | ConsistentCase(Case(scrut, rules, _))
+  | NotExhaustive(Case(scrut, rules, _)) =>
     let hii =
       Util.TimeUtil.measure_time("track_children_of_hole(scrut)", true, () =>
         track_children_of_hole(hii, parent, scrut)
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 92f8cff0fe..780b992798 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/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));
+  | NotExhaustive(Case(d3, rules, n)) =>
+    let d3 = subst_var(d1, x, d3);
+    let rules = subst_var_rules(d1, x, rules);
+    NotExhaustive(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);
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index ead18ee4ff..20df10c486 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -66,6 +66,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | Let(_)
   | FixF(_)
   | ConsistentCase(_)
+  | NotExhaustive(_)
   | InconsistentBranches(_) => DHDoc_common.precedence_max
   | BinBoolOp(op, _, _) => precedence_bin_bool_op(op)
   | BinIntOp(op, _, _) => precedence_bin_int_op(op)
@@ -237,7 +238,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, _))
+      | NotExhaustive(Case(dscrut, drs, _)) => go_case(dscrut, drs)
       | Cast(d, _, _) =>
         let (doc, _) = go'(d);
         doc;

From 074546396100f5ace111d456e3ee2c76440bc662 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 12:18:11 -0400
Subject: [PATCH 02/10] Init

---
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 2dc53757b5..ac241cd6f0 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -93,6 +93,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,

From 190faa21a3ee4c4e6464bf73969d28f5b30873a1 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 12:46:26 -0400
Subject: [PATCH 03/10] Revert, part I

---
 Makefile                         |  2 +-
 src/haz3lcore/statics/Statics.re |  5 +----
 src/haz3lcore/statics/TypBase.re | 23 +++--------------------
 src/haz3lcore/tiles/Id.re        | 13 +------------
 src/haz3lschool/Grading.re       |  5 ++++-
 5 files changed, 10 insertions(+), 38 deletions(-)

diff --git a/Makefile b/Makefile
index c73daaee27..cc409caf68 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ release: setup-instructor
 	dune build @src/fmt --auto-promote src --profile release
 
 release-student: setup-student
-	dune build @src/fmt --auto-promote src --profile dev
+	dune build @src/fmt --auto-promote src --profile release
 
 echo-html-dir:
 	@echo "$(HTML_DIR)"
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index fb54e723dc..f5962cce77 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -306,10 +306,7 @@ and uexp_to_info_map =
         let ty_pre = UTyp.to_typ(Ctx.extend_dummy_tvar(ctx, name), utyp);
         switch (utyp.term) {
         | Sum(_) when List.mem(name, Typ.free_vars(ty_pre)) =>
-          /* NOTE: When debugging type system issues it may be beneficial to
-             use a different name than the alias for the recursive parameter */
-          //let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
-          let ty_rec = Typ.Rec(name, ty_pre);
+          let ty_rec = Typ.Rec("α", Typ.subst(Var("α"), name, ty_pre));
           let ctx_def =
             Ctx.extend_alias(ctx, name, UTPat.rep_id(typat), ty_rec);
           (ty_rec, ctx_def, ctx_def);
diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re
index 3f614145ab..8ba6577410 100644
--- a/src/haz3lcore/statics/TypBase.re
+++ b/src/haz3lcore/statics/TypBase.re
@@ -393,28 +393,11 @@ module rec Typ: {
     | Sum(sm) => Some(sm)
     | Rec(_) =>
       /* Note: We must unroll here to get right ctr types;
-         otherwise the rec parameter will leak. However, seeing
-         as substitution is too expensive to be used here, we
-         currently making the optimization that, since all
-         recursive types are type alises which use the alias name
-         as the recursive parameter, and type aliases cannot be
-         shadowed, it is safe to simply remove the Rec constructor,
-         provided we haven't escaped the context in which the alias
-         is bound. If either of the above assumptions become invalid,
-         the below code will be incorrect! */
-      let ty =
-        switch (ty) {
-        | Rec(x, ty_body) =>
-          switch (Ctx.lookup_alias(ctx, x)) {
-          | None => unroll(ty)
-          | Some(_) => ty_body
-          }
-        | _ => ty
-        };
-      switch (ty) {
+         otherwise the rec parameter will leak */
+      switch (unroll(ty)) {
       | Sum(sm) => Some(sm)
       | _ => None
-      };
+      }
     | _ => None
     };
   };
diff --git a/src/haz3lcore/tiles/Id.re b/src/haz3lcore/tiles/Id.re
index 00fcb693b7..388087cc11 100644
--- a/src/haz3lcore/tiles/Id.re
+++ b/src/haz3lcore/tiles/Id.re
@@ -126,20 +126,9 @@ type t = Uuidm.t;
 let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init());
 
 let compare: (t, t) => int = Uuidm.compare;
+let pp: (Format.formatter, t) => unit = Uuidm.pp;
 let to_string: (~upper: bool=?, t) => string = Uuidm.to_string;
 let of_string: (~pos: int=?, string) => option(t) = Uuidm.of_string;
-let pp: (Format.formatter, t) => unit =
-  (f, id) =>
-    Format.fprintf(
-      f,
-      "Option.get(Haz3lcore.Id.of_string(\"%s\"))",
-      to_string(id),
-    );
-let show = id =>
-  Format.sprintf(
-    "Option.get(Haz3lcore.Id.of_string(\"%s\"))",
-    to_string(id),
-  );
 
 [@deriving (sexp, yojson)]
 type binding('v) = (t, 'v);
diff --git a/src/haz3lschool/Grading.re b/src/haz3lschool/Grading.re
index 507fe5c507..33301f0d69 100644
--- a/src/haz3lschool/Grading.re
+++ b/src/haz3lschool/Grading.re
@@ -171,7 +171,10 @@ module F = (ExerciseEnv: Exercise.ExerciseEnv) => {
     };
 
     let mk = (~your_impl: Editor.t, ~tests: syntax_tests): t => {
-      let user_impl_term = EditorUtil.stitch([your_impl]);
+      let user_impl_term =
+        Util.TimeUtil.measure_time("user_impl_term_syntax", true, () =>
+          EditorUtil.stitch([your_impl])
+        );
 
       let predicates = List.map(((_, p)) => p, tests);
       let hints = List.map(((h, _)) => h, tests);

From 98162512607f53d2c9b5648f1a3ce873424e5190 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 12:57:30 -0400
Subject: [PATCH 04/10] Revert Exercise.re

---
 src/haz3lschool/Exercise.re | 187 ++++++++++++++++--------------------
 1 file changed, 81 insertions(+), 106 deletions(-)

diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index 6d58feecf6..2076a8ef7e 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -557,10 +557,6 @@ module F = (ExerciseEnv: ExerciseEnv) => {
 
   // # Stitching
 
-  module TermItem = {
-    type t = TermBase.UExp.t;
-  };
-
   module StaticsItem = {
     type t = {
       term: TermBase.UExp.t,
@@ -578,68 +574,92 @@ module F = (ExerciseEnv: ExerciseEnv) => {
     hidden_tests: 'a,
   };
 
-  let stitch_term = ({eds, _}: state): stitched(TermItem.t) => {
-    let instructor =
+  type stitched_statics = stitched(StaticsItem.t);
+
+  /* Multiple stitchings are needed for each exercise
+     (see comments in the stitched type above)
+     Stitching is necessary to concatenate terms
+     from different editors, which are then typechecked. */
+  let stitch_static = ({eds, _}: state): stitched_statics => {
+    let test_validation_term =
+      Util.TimeUtil.measure_time("test_validation_term", true, () =>
+        EditorUtil.stitch([
+          eds.prelude,
+          eds.correct_impl,
+          eds.your_tests.tests,
+        ])
+      );
+    let test_validation_map =
+      Util.TimeUtil.measure_time("test_validation_map", true, () =>
+        Statics.mk_map(test_validation_term)
+      );
+    let test_validation =
+      StaticsItem.{term: test_validation_term, info_map: test_validation_map};
+
+    let user_impl_term =
+      Util.TimeUtil.measure_time("user_impl_term", true, () =>
+        EditorUtil.stitch([eds.prelude, eds.your_impl])
+      );
+    let user_impl_map =
+      Util.TimeUtil.measure_time("user_impl_map", true, () =>
+        Statics.mk_map(user_impl_term)
+      );
+    let user_impl =
+      StaticsItem.{term: user_impl_term, info_map: user_impl_map};
+
+    let user_tests_term =
+      Util.TimeUtil.measure_time("user_tests_term", true, () =>
+        EditorUtil.stitch([eds.prelude, eds.your_impl, eds.your_tests.tests])
+      );
+    let user_tests_map =
+      Util.TimeUtil.measure_time("user_tests_map", true, () =>
+        Statics.mk_map(user_tests_term)
+      );
+    let user_tests =
+      StaticsItem.{term: user_tests_term, info_map: user_tests_map};
+
+    // let prelude_term = EditorUtil.stitch([eds.prelude]);
+    // let prelude_map = Statics.mk_map(prelude_term);
+    // let prelude = StaticsItem.{term: prelude_term, info_map: prelude_map};
+
+    let instructor_term =
       EditorUtil.stitch([
         eds.prelude,
         eds.correct_impl,
         eds.hidden_tests.tests,
       ]);
-    {
-      test_validation:
-        EditorUtil.stitch([
-          eds.prelude,
-          eds.correct_impl,
-          eds.your_tests.tests,
-        ]),
-      user_impl: EditorUtil.stitch([eds.prelude, eds.your_impl]),
-      user_tests:
-        EditorUtil.stitch([eds.prelude, eds.your_impl, eds.your_tests.tests]),
-      prelude: instructor, // works as long as you don't shadow anything in the prelude
-      instructor,
-      hidden_bugs:
-        List.map(
-          ({impl, _}) => {
-            EditorUtil.stitch([eds.prelude, impl, eds.your_tests.tests])
-          },
-          eds.hidden_bugs,
-        ),
-      hidden_tests:
-        EditorUtil.stitch([
-          eds.prelude,
-          eds.your_impl,
-          eds.hidden_tests.tests,
-        ]),
-    };
-  };
-  let stitch_term = Core.Memo.general(stitch_term);
+    let instructor_info_map = Statics.mk_map(instructor_term);
+    let instructor =
+      StaticsItem.{term: instructor_term, info_map: instructor_info_map};
 
-  type stitched_statics = stitched(StaticsItem.t);
+    let hidden_bugs =
+      List.map(
+        ({impl, _}) => {
+          let term =
+            EditorUtil.stitch([eds.prelude, impl, eds.your_tests.tests]);
+          let info_map = Statics.mk_map(term);
+          StaticsItem.{term, info_map};
+        },
+        eds.hidden_bugs,
+      );
 
-  /* Multiple stitchings are needed for each exercise
-     (see comments in the stitched type above)
+    let hidden_tests_term =
+      EditorUtil.stitch([eds.prelude, eds.your_impl, eds.hidden_tests.tests]);
+    let hidden_tests_map = Statics.mk_map(hidden_tests_term);
+    let hidden_tests =
+      StaticsItem.{term: hidden_tests_term, info_map: hidden_tests_map};
 
-     Stitching is necessary to concatenate terms
-     from different editors, which are then typechecked. */
-  let stitch_static = (t: stitched(TermItem.t)): stitched_statics => {
-    let mk = (term): StaticsItem.t => {
-      term,
-      info_map: Statics.mk_map(term),
-    };
-    let instructor = mk(t.instructor);
     {
-      test_validation: mk(t.test_validation),
-      user_impl: mk(t.user_impl),
-      user_tests: mk(t.user_tests),
+      test_validation,
+      user_impl,
+      user_tests,
       prelude: instructor, // works as long as you don't shadow anything in the prelude
       instructor,
-      hidden_bugs: List.map(mk, t.hidden_bugs),
-      hidden_tests: mk(t.hidden_tests),
+      hidden_bugs,
+      hidden_tests,
     };
   };
 
-  let stitch_static = Core.Memo.general(stitch_static);
-
   let test_validation_key = "test_validation";
   let user_impl_key = "user_impl";
   let user_tests_key = "user_tests";
@@ -658,16 +678,13 @@ module F = (ExerciseEnv: ExerciseEnv) => {
         hidden_bugs,
         hidden_tests,
       } =
-        stitch_static(stitch_term(state));
+        Util.TimeUtil.measure_time("stitch_static2", true, () =>
+          stitch_static(state)
+        );
       [
         (
           test_validation_key,
-          {
-            Interface.elaborate(
-              test_validation.info_map,
-              test_validation.term,
-            );
-          },
+          Interface.elaborate(test_validation.info_map, test_validation.term),
         ),
         (
           user_impl_key,
@@ -683,9 +700,7 @@ module F = (ExerciseEnv: ExerciseEnv) => {
         ),
         (
           hidden_tests_key,
-          {
-            Interface.elaborate(hidden_tests.info_map, hidden_tests.term);
-          },
+          Interface.elaborate(hidden_tests.info_map, hidden_tests.term),
         ),
       ]
       @ (
@@ -705,47 +720,8 @@ module F = (ExerciseEnv: ExerciseEnv) => {
       info_map: Statics.Map.t,
       simple_result: ModelResult.simple,
     };
-    let empty: t = {
-      term: {
-        term: Tuple([]),
-        ids: [Id.mk()],
-      },
-      info_map: Id.Map.empty,
-      simple_result: None,
-    };
-    let statics_only = ({term, info_map}: StaticsItem.t): t => {
-      {term, info_map, simple_result: None};
-    };
   };
 
-  let empty_dynamics_with_statics = (state: state): stitched(DynamicsItem.t) => {
-    let t = stitch_static(stitch_term(state));
-    {
-      test_validation: DynamicsItem.statics_only(t.test_validation),
-      user_impl: DynamicsItem.statics_only(t.user_impl),
-      user_tests: DynamicsItem.statics_only(t.user_tests),
-      instructor: DynamicsItem.statics_only(t.instructor),
-      prelude: DynamicsItem.statics_only(t.prelude),
-      hidden_bugs: List.map(DynamicsItem.statics_only, t.hidden_bugs),
-      hidden_tests: DynamicsItem.statics_only(t.hidden_tests),
-    };
-  };
-
-  let empty_dynamics = (state: state): stitched(DynamicsItem.t) => {
-    {
-      test_validation: DynamicsItem.empty,
-      user_impl: DynamicsItem.empty,
-      user_tests: DynamicsItem.empty,
-      instructor: DynamicsItem.empty,
-      prelude: DynamicsItem.empty,
-      hidden_bugs:
-        List.init(List.length(state.eds.hidden_bugs), _ =>
-          DynamicsItem.empty
-        ),
-      hidden_tests: DynamicsItem.empty,
-    };
-  };
-  let empty_dynamics = Core.Memo.general(empty_dynamics);
   /* Given the evaluation results, collects the
      relevant information for producing dynamic
      feedback*/
@@ -761,28 +737,27 @@ module F = (ExerciseEnv: ExerciseEnv) => {
       hidden_bugs,
       hidden_tests,
     } =
-      stitch_static(stitch_term(state));
+      Util.TimeUtil.measure_time("stitch_static1", true, () =>
+        stitch_static(state)
+      );
     let simple_result_of = key =>
       switch (results) {
       | None => None
       | Some(results) =>
         ModelResult.get_simple(ModelResults.lookup(results, key))
       };
-
     let test_validation =
       DynamicsItem.{
         term: test_validation.term,
         info_map: test_validation.info_map,
         simple_result: simple_result_of(test_validation_key),
       };
-
     let user_impl =
       DynamicsItem.{
         term: user_impl.term,
         info_map: user_impl.info_map,
         simple_result: simple_result_of(user_impl_key),
       };
-
     let user_tests =
       DynamicsItem.{
         term: user_tests.term,
@@ -817,6 +792,7 @@ module F = (ExerciseEnv: ExerciseEnv) => {
         info_map: hidden_tests.info_map,
         simple_result: simple_result_of(hidden_tests_key),
       };
+
     {
       test_validation,
       user_impl,
@@ -827,7 +803,6 @@ module F = (ExerciseEnv: ExerciseEnv) => {
       hidden_tests,
     };
   };
-  let stitch_dynamic = Core.Memo.general(stitch_dynamic);
 
   let focus = (state: state, stitched_dynamics: stitched(DynamicsItem.t)) => {
     let {pos, eds} = state;

From d9d68a61b80ca1cffaf3b63fd6687ece5132b8b2 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 12:57:58 -0400
Subject: [PATCH 05/10] Update Exercise.re

---
 src/haz3lschool/Exercise.re | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index 2076a8ef7e..268e39b233 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -578,6 +578,7 @@ module F = (ExerciseEnv: ExerciseEnv) => {
 
   /* Multiple stitchings are needed for each exercise
      (see comments in the stitched type above)
+
      Stitching is necessary to concatenate terms
      from different editors, which are then typechecked. */
   let stitch_static = ({eds, _}: state): stitched_statics => {

From 42069c5e1e400fe4733063fd78bd7bf28fddc8f9 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 13:00:40 -0400
Subject: [PATCH 06/10] Revert, part II

---
 src/haz3lweb/Grading.re | 9 ++-------
 src/haz3lweb/Update.re  | 5 ++---
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/src/haz3lweb/Grading.re b/src/haz3lweb/Grading.re
index dd69186e82..bc053887d1 100644
--- a/src/haz3lweb/Grading.re
+++ b/src/haz3lweb/Grading.re
@@ -389,12 +389,7 @@ module ImplGradingReport = {
 
   let individual_reports = (~inject, ~report) => {
     switch (report.test_results) {
-    | Some(test_results)
-        when
-          List.length(test_results.test_map)
-          == List.length(report.hinted_results) =>
-      /* NOTE: This condition will be false when evaluation crashes,
-       * for example due to a stack overflow, which may occur in normal operation  */
+    | Some(test_results) =>
       div(
         report.hinted_results
         |> List.mapi((i, (status, hint)) =>
@@ -407,7 +402,7 @@ module ImplGradingReport = {
              )
            ),
       )
-    | _ => div([])
+    | None => div([])
     };
   };
 
diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re
index 3709fbd956..1780d7bb9b 100644
--- a/src/haz3lweb/Update.re
+++ b/src/haz3lweb/Update.re
@@ -191,8 +191,7 @@ let switch_exercise_editor =
   | Scratch(_) => None
   | Exercise(m, specs, exercise) =>
     let exercise = Exercise.switch_editor(~pos, instructor_mode, ~exercise);
-    //Note: now saving after each edit (delayed by 1 second) so no need to save here
-    //Store.Exercise.save_exercise(exercise, ~instructor_mode);
+    Store.Exercise.save_exercise(exercise, ~instructor_mode);
     Some(Exercise(m, specs, exercise));
   };
 
@@ -271,7 +270,7 @@ let apply =
       let instructor_mode = model.settings.instructor_mode;
       switch (switch_exercise_editor(model.editors, ~pos, ~instructor_mode)) {
       | None => Error(FailedToSwitch)
-      | Some(editors) => Ok({...model, editors})
+      | Some(editors) => Model.save_and_return({...model, editors})
       };
     | SetMode(mode) =>
       let model = update_settings(Mode(mode), model);

From 6db5d247b558cf6163cb8ad0c34787dee939b2e5 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 14:11:15 -0400
Subject: [PATCH 07/10] Renamed NotExhaustive to InexhaustiveCase and corrected
 its behavior

---
 src/haz3lcore/dynamics/DH.re                 | 26 +++++++++++---------
 src/haz3lcore/dynamics/Elaborator.re         |  6 ++++-
 src/haz3lcore/dynamics/Evaluator.re          | 13 +++++-----
 src/haz3lcore/dynamics/EvaluatorPost.re      | 20 ++++++++-------
 src/haz3lcore/dynamics/Substitution.re       |  4 +--
 src/haz3lweb/view/dhcode/DHCode.re           |  1 +
 src/haz3lweb/view/dhcode/layout/DHAnnot.re   |  1 +
 src/haz3lweb/view/dhcode/layout/DHAnnot.rei  |  1 +
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re |  7 +++---
 9 files changed, 46 insertions(+), 33 deletions(-)

diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index 046ad778c2..6150787d74 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -33,10 +33,10 @@ 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)
-    | NotExhaustive(case)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -88,10 +88,10 @@ 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)
-    | NotExhaustive(case)
   and case =
     | Case(t, list(rule), int)
   and rule =
@@ -128,11 +128,11 @@ module rec DHExp: {
     | Prj(_) => "Prj"
     | Constructor(_) => "Constructor"
     | ConsistentCase(_) => "ConsistentCase"
+    | InexhaustiveCase(_, _, _) => "InexhaustiveCase"
     | InconsistentBranches(_, _, _) => "InconsistentBranches"
     | Cast(_, _, _) => "Cast"
     | FailedCast(_, _, _) => "FailedCast"
     | InvalidOperation(_) => "InvalidOperation"
-    | NotExhaustive(_) => "NotExhaustive"
     };
 
   let mk_tuple: list(t) => t =
@@ -177,9 +177,11 @@ module rec DHExp: {
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
       )
-    | NotExhaustive(Case(a, rs, b)) =>
-      NotExhaustive(
-        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(
@@ -249,8 +251,7 @@ module rec DHExp: {
       fast_equal(d1, d2) && ty11 == ty12 && ty21 == ty22
     | (InvalidOperation(d1, reason1), InvalidOperation(d2, reason2)) =>
       fast_equal(d1, d2) && reason1 == reason2
-    | (ConsistentCase(case1), ConsistentCase(case2))
-    | (NotExhaustive(case1), NotExhaustive(case2)) =>
+    | (ConsistentCase(case1), ConsistentCase(case2)) =>
       fast_equal_case(case1, case2)
     /* We can group these all into a `_ => false` clause; separating
        these so that we get exhaustiveness checking. */
@@ -272,8 +273,7 @@ module rec DHExp: {
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)
-    | (ConsistentCase(_), _)
-    | (NotExhaustive(_), _) => false
+    | (ConsistentCase(_), _) => false
 
     /* Hole forms: when checking environments, only check that
        environment ID's are equal, don't check structural equality.
@@ -293,7 +293,8 @@ 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(_), _)
@@ -301,7 +302,8 @@ module rec DHExp: {
     | (FreeVar(_), _)
     | (InvalidText(_), _)
     | (Closure(_), _)
-    | (InconsistentBranches(_), _) => false
+    | (InconsistentBranches(_), _)
+    | (InexhaustiveCase(_), _) => false
     };
   }
   and fast_equal_case = (Case(d1, rules1, i1), Case(d2, rules2, i2)) => {
diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index f2ac07e3b5..a397ef7e4b 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -69,7 +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(_)
-    | NotExhaustive(_)
+    | InexhaustiveCase(_)
     | InconsistentBranches(_)
     | Sequence(_)
     | Let(_)
@@ -272,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)
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index c95993467f..3efea0f886 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -304,6 +304,7 @@ and matches_cast_Sum =
   | BinFloatOp(_)
   | BinStringOp(_)
   | InconsistentBranches(_)
+  | InexhaustiveCase(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
   | FailedCast(_, _, _)
@@ -320,7 +321,6 @@ and matches_cast_Sum =
   | Tuple(_)
   | Prj(_)
   | ConsistentCase(_)
-  | NotExhaustive(_)
   | Sequence(_, _)
   | Closure(_)
   | TestLit(_)
@@ -410,7 +410,7 @@ and matches_cast_Tuple =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
-  | NotExhaustive(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -546,7 +546,7 @@ and matches_cast_Cons =
   | Prj(_) => DoesNotMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
-  | NotExhaustive(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => IndetMatch
   | EmptyHole(_) => IndetMatch
   | NonEmptyHole(_) => IndetMatch
@@ -991,9 +991,10 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
       Indet(Closure(env, InconsistentBranches(u, i, Case(d1, rules, n))))
       |> return
 
-    // TODO: Imitation of the last, may need to change as well.
-    | NotExhaustive(Case(d1, rules, n)) =>
-      Indet(Closure(env, NotExhaustive(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
 
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 4f76853748..157fcc96e5 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -150,7 +150,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | BoundVar(_)
   | Let(_)
   | ConsistentCase(_)
-  | NotExhaustive(_)
+  | InexhaustiveCase(_)
   | Fun(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -378,11 +378,6 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* rules' = pp_uneval_rules(env, rules);
     ConsistentCase(Case(scrut', rules', i)) |> return;
 
-  | NotExhaustive(Case(scrut, rules, i)) =>
-    let* scrut' = pp_uneval(env, scrut);
-    let* rules' = pp_uneval_rules(env, rules);
-    NotExhaustive(Case(scrut', rules', i)) |> return;
-
   /* Closures shouldn't exist inside other closures */
   | Closure(_) => raise(Exception(ClosureInsideClosure))
 
@@ -418,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 =
@@ -487,8 +489,7 @@ let rec track_children_of_hole =
       hii,
     )
 
-  | ConsistentCase(Case(scrut, rules, _))
-  | NotExhaustive(Case(scrut, rules, _)) =>
+  | ConsistentCase(Case(scrut, rules, _)) =>
     let hii =
       Util.TimeUtil.measure_time("track_children_of_hole(scrut)", true, () =>
         track_children_of_hole(hii, parent, scrut)
@@ -508,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);
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 780b992798..45acf7caf2 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -89,10 +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));
-  | NotExhaustive(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);
-    NotExhaustive(Case(d3, rules, n));
+    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);
diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re
index 52e9b0bdbd..7c0de89b5e 100644
--- a/src/haz3lweb/view/dhcode/DHCode.re
+++ b/src/haz3lweb/view/dhcode/DHCode.re
@@ -77,6 +77,7 @@ let view_of_layout = (~font_metrics: FontMetrics.t, l: DHLayout.t): Node.t => {
                ([with_cls("exception", txt)], ds)
              | NonEmptyHole(_)
              | InconsistentBranches(_)
+             | InexhaustiveCase(_)
              | Invalid(_) =>
                let offset = start.col - indent;
                let decoration =
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.re b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
index 83893613e4..97a71fb2b9 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.re
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
@@ -12,6 +12,7 @@ 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
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
index 3ff0d8ef48..474528202e 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
@@ -11,6 +11,7 @@ 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
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 2f67d9aeca..02379d4d4c 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -66,7 +66,7 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => {
   | Let(_)
   | FixF(_)
   | ConsistentCase(_)
-  | NotExhaustive(_)
+  | InexhaustiveCase(_)
   | InconsistentBranches(_) => DHDoc_common.precedence_max
   | BinBoolOp(op, _, _) => precedence_bin_bool_op(op)
   | BinIntOp(op, _, _) => precedence_bin_int_op(op)
@@ -175,6 +175,8 @@ let rec mk =
       | 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)))
+      | InexhaustiveCase(u, i, Case(dscrut, drs, _)) =>
+        go_case(dscrut, drs) |> annot(DHAnnot.InexhaustiveCase((u, i)))
       | BoundVar(x) => text(x)
       | Constructor(name) => DHDoc_common.mk_ConstructorLit(name)
       | BoolLit(b) => DHDoc_common.mk_BoolLit(b)
@@ -238,8 +240,7 @@ 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, _))
-      | NotExhaustive(Case(dscrut, drs, _)) => go_case(dscrut, drs)
+      | ConsistentCase(Case(dscrut, drs, _)) => go_case(dscrut, drs)
       | Cast(d, _, _) =>
         let (doc, _) = go'(d);
         doc;

From f53c5c5b6943ed8053b053aa16ade38f92423792 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 14:21:56 -0400
Subject: [PATCH 08/10] Reverted InvalidOperationError.re

---
 src/haz3lcore/dynamics/InvalidOperationError.re | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/haz3lcore/dynamics/InvalidOperationError.re b/src/haz3lcore/dynamics/InvalidOperationError.re
index ce8c94e888..3a6e31c35f 100644
--- a/src/haz3lcore/dynamics/InvalidOperationError.re
+++ b/src/haz3lcore/dynamics/InvalidOperationError.re
@@ -5,6 +5,8 @@ type t =
   | DivideByZero
   | NegativeExponent
   | OutOfFuel
+  //  | InvalidIntOfString
+  //  | InvalidFloatOfString
   | InvalidProjection;
 
 let err_msg = (err: t): string =>
@@ -14,5 +16,7 @@ let err_msg = (err: t): string =>
   | DivideByZero => "Error: Divide by Zero"
   | NegativeExponent => "Error: Negative Exponent in Integer Exponentiation (Consider using **.)"
   | OutOfFuel => "Error: Out of Fuel"
+  //  | InvalidIntOfString => "Error: Invalid String to Int Conversion"
+  //  | InvalidFloatOfString => "Error: Invalid String to Float Conversion"
   | InvalidProjection => "Error: Invalid Projection"
   };

From 5ddd220efb14d4c720e845cab3aae2a1fe907916 Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 21:19:41 -0400
Subject: [PATCH 09/10] Crossing out unmatched patterns, part I

---
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 48 +++++++++++++-------
 1 file changed, 32 insertions(+), 16 deletions(-)

diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 3336617a43..2592a77a5f 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -124,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 {
@@ -139,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],
           ]),
         );
@@ -175,9 +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) |> annot(DHAnnot.InexhaustiveCase((u, i)))
+        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)
@@ -241,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;
@@ -373,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);
@@ -388,14 +403,15 @@ and mk_rule =
           ]),
         ])
       : hcat(space(), hidden_clause);
-  hcats([
-    DHDoc_common.Delim.bar_Rule,
-    DHDoc_Pat.mk(dp)
-    |> DHDoc_common.pad_child(
-         ~inline_padding=(space(), space()),
-         ~enforce_inline=false,
-       ),
-    DHDoc_common.Delim.arrow_Rule,
-    clause_doc,
-  ]);
+  hcats(
+    [
+      DHDoc_common.Delim.bar_Rule,
+      DHDoc_Pat.mk(dp)
+      |> DHDoc_common.pad_child(
+           ~inline_padding=(space(), space()),
+           ~enforce_inline=false,
+         ),
+    ]
+    @ (crossed_out ? [] : [DHDoc_common.Delim.arrow_Rule, clause_doc]),
+  );
 };

From a7d169327028caa4e5a81b97ad2f6e230367432f Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sun, 22 Oct 2023 21:52:01 -0400
Subject: [PATCH 10/10] Crossing out unmatched patterns, part II

---
 src/haz3lweb/view/dhcode/DHCode.re           |  4 ++++
 src/haz3lweb/view/dhcode/layout/DHAnnot.re   |  3 ++-
 src/haz3lweb/view/dhcode/layout/DHAnnot.rei  |  3 ++-
 src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 25 +++++++++++---------
 src/haz3lweb/www/style.css                   |  5 ++++
 5 files changed, 27 insertions(+), 13 deletions(-)

diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re
index 7c0de89b5e..8fd43e4856 100644
--- a/src/haz3lweb/view/dhcode/DHCode.re
+++ b/src/haz3lweb/view/dhcode/DHCode.re
@@ -72,6 +72,10 @@ 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)
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.re b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
index 97a71fb2b9..e9ea84969c 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.re
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.re
@@ -17,4 +17,5 @@ type t =
   | FailedCastDelim
   | FailedCastDecoration
   | CastDecoration
-  | OperationError(InvalidOperationError.t);
+  | OperationError(InvalidOperationError.t)
+  | MismatchedRuleDecoration;
diff --git a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
index 474528202e..e433ab0dce 100644
--- a/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
+++ b/src/haz3lweb/view/dhcode/layout/DHAnnot.rei
@@ -16,4 +16,5 @@ type t =
   | FailedCastDelim
   | FailedCastDecoration
   | CastDecoration
-  | OperationError(InvalidOperationError.t);
+  | OperationError(InvalidOperationError.t)
+  | MismatchedRuleDecoration;
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index 2592a77a5f..72a2ae227b 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -403,15 +403,18 @@ and mk_rule =
           ]),
         ])
       : hcat(space(), hidden_clause);
-  hcats(
-    [
-      DHDoc_common.Delim.bar_Rule,
-      DHDoc_Pat.mk(dp)
-      |> DHDoc_common.pad_child(
-           ~inline_padding=(space(), space()),
-           ~enforce_inline=false,
-         ),
-    ]
-    @ (crossed_out ? [] : [DHDoc_common.Delim.arrow_Rule, clause_doc]),
-  );
+  // temporary name
+  let r = [
+    DHDoc_common.Delim.bar_Rule,
+    DHDoc_Pat.mk(dp)
+    |> DHDoc_common.pad_child(
+         ~inline_padding=(space(), space()),
+         ~enforce_inline=false,
+       ),
+    DHDoc_common.Delim.arrow_Rule,
+    clause_doc,
+  ];
+  let r =
+    crossed_out ? List.map(annot(DHAnnot.MismatchedRuleDecoration), r) : r;
+  hcats(r);
 };
diff --git a/src/haz3lweb/www/style.css b/src/haz3lweb/www/style.css
index 6a646dc172..e398143f51 100644
--- a/src/haz3lweb/www/style.css
+++ b/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;