From 5d0629d153dacd276a27629e9127297a8b310a0d Mon Sep 17 00:00:00 2001
From: Matt Keenan <negabinary@gmail.com>
Date: Fri, 15 Nov 2024 11:21:32 -0500
Subject: [PATCH] Fix failed cast ids

---
 src/haz3lcore/lang/term/Typ.re                | 14 ++++++++++++++
 src/haz3lcore/statics/TermBase.re             |  3 ++-
 src/haz3lweb/app/editors/result/EvalResult.re |  4 +++-
 src/haz3lweb/app/editors/result/Stepper.re    | 10 +++++++---
 4 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re
index 0d068dcfcb..f433440701 100644
--- a/src/haz3lcore/lang/term/Typ.re
+++ b/src/haz3lcore/lang/term/Typ.re
@@ -43,6 +43,20 @@ let all_ids_temp = {
   map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f);
 };
 
+let (replace_temp, replace_temp_exp) = {
+  let f:
+    'a.
+    (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
+   =
+    (continue, exp) =>
+      {...exp, ids: exp.ids == [Id.invalid] ? [Id.mk()] : exp.ids}
+      |> continue;
+  (
+    map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
+    TermBase.Exp.map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
+  );
+};
+
 let hole = (tms: list(TermBase.Any.t)) =>
   switch (tms) {
   | [] => Unknown(Hole(EmptyHole))
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 432209da0b..a8e522c255 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -288,7 +288,8 @@ and Exp: {
         | Undefined => term
         | MultiHole(things) => MultiHole(List.map(any_map_term, things))
         | DynamicErrorHole(e, err) => DynamicErrorHole(exp_map_term(e), err)
-        | FailedCast(e, t1, t2) => FailedCast(exp_map_term(e), t1, t2)
+        | FailedCast(e, t1, t2) =>
+          FailedCast(exp_map_term(e), typ_map_term(t1), typ_map_term(t2))
         | ListLit(ts) => ListLit(List.map(exp_map_term, ts))
         | Fun(p, e, env, f) =>
           Fun(pat_map_term(p), exp_map_term(e), env, f)
diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re
index c8b59e2f3a..7271553c54 100644
--- a/src/haz3lweb/app/editors/result/EvalResult.re
+++ b/src/haz3lweb/app/editors/result/EvalResult.re
@@ -147,7 +147,9 @@ module Update = {
               NewValue(
                 Haz3lcore.ProgramResult.map(
                   ({result: r, state: s}: Haz3lcore.ProgramResult.inner) => {
-                    let exp = Haz3lcore.ProgramResult.Result.unbox(r);
+                    let exp =
+                      Haz3lcore.ProgramResult.Result.unbox(r)
+                      |> Haz3lcore.DHExp.replace_all_ids;
                     (exp, s);
                   },
                   update,
diff --git a/src/haz3lweb/app/editors/result/Stepper.re b/src/haz3lweb/app/editors/result/Stepper.re
index e2abfc8af5..f289ae8971 100644
--- a/src/haz3lweb/app/editors/result/Stepper.re
+++ b/src/haz3lweb/app/editors/result/Stepper.re
@@ -88,6 +88,7 @@ module Model = {
 module Update = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
+    // int here should include hidden steps
     | StepperEditor(int, StepperEditor.Update.t)
     | StepForward(int)
     | StepBackward;
@@ -204,7 +205,8 @@ module Update = {
                }
              )
         );
-      let next_expr = EvalCtx.compose(b.step.ctx, next_expr);
+      let next_expr =
+        EvalCtx.compose(b.step.ctx, next_expr) |> Typ.replace_temp_exp;
       let editor = CodeWithStatics.Model.mk_from_exp(~settings, next_expr);
       let next_steps = calc_next_steps(settings, next_expr, next_state);
       (
@@ -291,6 +293,7 @@ module Update = {
             |> {
               let.calc elab = elab
               and.calc settings = settings;
+              let elab = elab |> Typ.replace_temp_exp;
               let editor = CodeWithStatics.Model.mk_from_exp(~settings, elab);
               let next_steps =
                 calc_next_steps(settings, elab, EvaluatorState.init);
@@ -404,11 +407,12 @@ module View = {
       stepper.history
       |> Aba.aba_triples
       |> (settings.core.evaluation.stepper_history ? x => x : (_ => []))
+      |> List.mapi((i, x) => (i, x))
       |> (
         settings.core.evaluation.show_hidden_steps
-          ? x => x : List.filter(((_, b: Model.b, _)) => !b.hidden)
+          ? x => x : List.filter(((_, (_, b: Model.b, _))) => !b.hidden)
       )
-      |> List.mapi((i, (_, b: Model.b, a: Model.a)) =>
+      |> List.map(((i, (_, b: Model.b, a: Model.a))) =>
            switch (a) {
            | Calculated(a) =>
              [