Errored statuses showed up right

hazelgrove · Nov 1, 2024 · d163367 · d163367
1 parent 7c5abb5
commit d163367
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
@@ -533,8 +533,9 @@ let status_tpat = (ctx: Ctx.t, utpat: TPat.t): status_tpat =>
 /* Determines whether any term is in an error hole. */
 let is_error = (ci: t): bool => {
   switch (ci) {
-  | InfoExp({mode, self, ctx, _}) =>
-    switch (status_exp(ctx, mode, self)) {
+  | InfoExp({status, _}) =>
+    // TODO Confirm with disconcision that we can use the derived status
+    switch (status) {
     | InHole(_) => true
     | NotInHole(_) => false
     }

diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -828,7 +828,7 @@ and uexp_to_info_map =
 
         let (term, rewrap) = UExp.unwrap(uexp);
         let og_exp = Exp.fresh(term);
-        let (_, m) =
+        let (og_info, m) =
           uexp_to_info_map(
             ~ctx,
             ~mode=Mode.Ana(ana_ty),
@@ -841,8 +841,12 @@ and uexp_to_info_map =
           rewrap(
             Tuple([TupLabel(Label(l1) |> Exp.fresh, og_exp) |> Exp.fresh]),
           );
+        let (info, m) =
+          uexp_to_info_map(~ctx, ~mode, ~ancestors, fake_uexp, m);
 
-        uexp_to_info_map(~ctx, ~mode, ~ancestors, fake_uexp, m);
+        let info = {...info, status: og_info.status};
+
+        (info, add_info(fake_uexp.ids, InfoExp(info), m));
       };
     | _ => default_case()
     }