From 3f72c712cfefe454e1c51a6cdfa019f67aca86c2 Mon Sep 17 00:00:00 2001
From: Matt Keenan <negabinary@gmail.com>
Date: Tue, 26 Nov 2024 11:39:34 -0500
Subject: [PATCH] New ids on early lookup

---
 src/haz3lcore/statics/Term.re | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 761b05acac..5677278b67 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -573,6 +573,18 @@ module Exp = {
       };
     };
 
+  let (replace_all_ids, replace_all_ids_typ) = {
+    let f:
+      'a.
+      (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
+     =
+      (continue, exp) => {...exp, ids: [Id.mk()]} |> continue;
+    (
+      map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
+      Typ.map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
+    );
+  };
+
   let rec substitute_closures =
           (
             env: Environment.t,
@@ -588,7 +600,9 @@ module Exp = {
           | Var(x) =>
             switch (Environment.lookup(env, x)) {
             | Some(e) =>
-              e |> substitute_closures(env, old_bound_vars, new_bound_vars)
+              e
+              |> replace_all_ids
+              |> substitute_closures(env, old_bound_vars, new_bound_vars)
             | None =>
               Var(
                 List.mem(x, old_bound_vars)