From eea6aad95e966c7f8b5491beb2f848664d9510f4 Mon Sep 17 00:00:00 2001
From: Haoxiang Fei <tonyfettes@tonyfettes.com>
Date: Mon, 23 Oct 2023 20:13:21 +0800
Subject: [PATCH 1/3] Remove EnvIdGen, use Uuidm instead

---
 src/haz3lcore/dynamics/DH.re                | 28 ++++++-----------
 src/haz3lcore/dynamics/EnvironmentId.re     | 11 +------
 src/haz3lcore/dynamics/EnvironmentId.rei    | 30 +-----------------
 src/haz3lcore/dynamics/EnvironmentIdGen.re  |  9 ------
 src/haz3lcore/dynamics/EnvironmentIdGen.rei | 19 ------------
 src/haz3lcore/dynamics/EnvironmentIdMap.re  |  2 +-
 src/haz3lcore/dynamics/EnvironmentIdMap.rei |  2 +-
 src/haz3lcore/dynamics/Evaluator.re         | 20 ++++++------
 src/haz3lcore/dynamics/EvaluatorMonad.re    |  4 ---
 src/haz3lcore/dynamics/EvaluatorMonad.rei   | 15 ---------
 src/haz3lcore/dynamics/EvaluatorPost.re     | 34 ++++++---------------
 src/haz3lcore/dynamics/EvaluatorPost.rei    |  4 +--
 src/haz3lcore/dynamics/EvaluatorState.re    | 14 +--------
 src/haz3lcore/dynamics/EvaluatorState.rei   | 16 ----------
 14 files changed, 36 insertions(+), 172 deletions(-)
 delete mode 100644 src/haz3lcore/dynamics/EnvironmentIdGen.re
 delete mode 100644 src/haz3lcore/dynamics/EnvironmentIdGen.rei

diff --git a/src/haz3lcore/dynamics/DH.re b/src/haz3lcore/dynamics/DH.re
index 61d7483930..b2d0a2bd17 100644
--- a/src/haz3lcore/dynamics/DH.re
+++ b/src/haz3lcore/dynamics/DH.re
@@ -333,33 +333,25 @@ and ClosureEnvironment: {
 
   let to_list: t => list((Var.t, DHExp.t));
 
-  let of_environment:
-    (Environment.t, EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let of_environment: Environment.t => t;
 
   let id_equal: (t, t) => bool;
 
-  let empty: EnvironmentIdGen.t => (t, EnvironmentIdGen.t);
+  let empty: t;
   let is_empty: t => bool;
   let length: t => int;
 
   let lookup: (t, Var.t) => option(DHExp.t);
   let contains: (t, Var.t) => bool;
-  let update:
-    (Environment.t => Environment.t, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let update: (Environment.t => Environment.t, t) => t;
   let update_keep_id: (Environment.t => Environment.t, t) => t;
-  let extend:
-    (t, (Var.t, DHExp.t), EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let extend: (t, (Var.t, DHExp.t)) => t;
   let extend_keep_id: (t, (Var.t, DHExp.t)) => t;
-  let union: (t, t, EnvironmentIdGen.t) => (t, EnvironmentIdGen.t);
+  let union: (t, t) => t;
   let union_keep_id: (t, t) => t;
-  let map:
-    (((Var.t, DHExp.t)) => DHExp.t, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let map: (((Var.t, DHExp.t)) => DHExp.t, t) => t;
   let map_keep_id: (((Var.t, DHExp.t)) => DHExp.t, t) => t;
-  let filter:
-    (((Var.t, DHExp.t)) => bool, t, EnvironmentIdGen.t) =>
-    (t, EnvironmentIdGen.t);
+  let filter: (((Var.t, DHExp.t)) => bool, t) => t;
   let filter_keep_id: (((Var.t, DHExp.t)) => bool, t) => t;
   let fold: (((Var.t, DHExp.t), 'b) => 'b, 'b, t) => 'b;
 
@@ -386,9 +378,9 @@ and ClosureEnvironment: {
 
   let to_list = env => env |> map_of |> Environment.to_listo;
 
-  let of_environment = (map, eig) => {
-    let (ei, eig) = EnvironmentIdGen.next(eig);
-    (wrap(ei, map), eig);
+  let of_environment = map => {
+    let ei = Id.mk();
+    wrap(ei, map);
   };
 
   /* Equals only needs to check environment id's (faster than structural equality
diff --git a/src/haz3lcore/dynamics/EnvironmentId.re b/src/haz3lcore/dynamics/EnvironmentId.re
index ddd33aa426..5f6be7cd46 100644
--- a/src/haz3lcore/dynamics/EnvironmentId.re
+++ b/src/haz3lcore/dynamics/EnvironmentId.re
@@ -1,10 +1 @@
-open Sexplib.Std;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = int;
-
-let init = 0;
-let equal = (==);
-
-let invalid = (-1);
-let is_invalid = equal(invalid);
+include Id;
diff --git a/src/haz3lcore/dynamics/EnvironmentId.rei b/src/haz3lcore/dynamics/EnvironmentId.rei
index db5c755074..e7d316dd0a 100644
--- a/src/haz3lcore/dynamics/EnvironmentId.rei
+++ b/src/haz3lcore/dynamics/EnvironmentId.rei
@@ -1,29 +1 @@
-/**
-  Identifier for environments.
- */
-
-/**
-  The type for identifiers.
- */
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = int;
-
-/**
-  [init] is the initial identifier.
- */
-let init: t;
-
-/**
-  [equal ei ei'] is true if and only if [ei] and [ei'] are equal.
- */
-let equal: (t, t) => bool;
-
-/**
-  [invalid] is an invalid identifier.
- */
-let invalid: t;
-
-/**
-  [is_invalid ei] is [equal invalid ei].
- */
-let is_invalid: t => bool;
+include (module type of Id);
diff --git a/src/haz3lcore/dynamics/EnvironmentIdGen.re b/src/haz3lcore/dynamics/EnvironmentIdGen.re
deleted file mode 100644
index 109c5fbd3c..0000000000
--- a/src/haz3lcore/dynamics/EnvironmentIdGen.re
+++ /dev/null
@@ -1,9 +0,0 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = EnvironmentId.t;
-
-let init = EnvironmentId.init;
-
-let next = id => {
-  let id = id + 1;
-  (id, id);
-};
diff --git a/src/haz3lcore/dynamics/EnvironmentIdGen.rei b/src/haz3lcore/dynamics/EnvironmentIdGen.rei
deleted file mode 100644
index 35d12017e5..0000000000
--- a/src/haz3lcore/dynamics/EnvironmentIdGen.rei
+++ /dev/null
@@ -1,19 +0,0 @@
-/**
-  Generator for {!type:EnvironmentId.t}.
- */
-
-/**
-  The type for the {!type:EnvironmentId.t} generator.
- */
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t;
-
-/**
-  [init] is the initial generator.
- */
-let init: t;
-
-/**
-  [next eig] is [(ei, eig')] where [ei] is the next generated identifier.
- */
-let next: t => (EnvironmentId.t, t);
diff --git a/src/haz3lcore/dynamics/EnvironmentIdMap.re b/src/haz3lcore/dynamics/EnvironmentIdMap.re
index fbb0fdb0ca..932d7b1316 100644
--- a/src/haz3lcore/dynamics/EnvironmentIdMap.re
+++ b/src/haz3lcore/dynamics/EnvironmentIdMap.re
@@ -1 +1 @@
-include Util.IntMap;
+include Id.Map;
diff --git a/src/haz3lcore/dynamics/EnvironmentIdMap.rei b/src/haz3lcore/dynamics/EnvironmentIdMap.rei
index 3064a6ddda..d5194bbcf2 100644
--- a/src/haz3lcore/dynamics/EnvironmentIdMap.rei
+++ b/src/haz3lcore/dynamics/EnvironmentIdMap.rei
@@ -2,4 +2,4 @@
 
    Used in HoleInstanceInfo_.re
    */
-include (module type of Util.IntMap);
+include (module type of Id.Map);
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index 529ca04260..cc9d2525df 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -662,13 +662,13 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
         | IndetMatch
         | DoesNotMatch => Indet(Closure(env, Let(dp, d1, d2))) |> return
         | Matches(env') =>
-          let* env = evaluate_extend_env(env', env);
+          let env = evaluate_extend_env(env', env);
           evaluate(env, d2);
         }
       };
 
     | FixF(f, _, d') =>
-      let* env' = evaluate_extend_env(Environment.singleton((f, d)), env);
+      let env' = evaluate_extend_env(Environment.singleton((f, d)), env);
       evaluate(env', d');
 
     | Fun(_) => BoxedValue(Closure(env, d)) |> return
@@ -694,7 +694,7 @@ let rec evaluate: (ClosureEnvironment.t, DHExp.t) => m(EvaluatorResult.t) =
           | Matches(env') =>
             // evaluate a closure: extend the closure environment with the
             // new bindings introduced by the function application.
-            let* env = evaluate_extend_env(env', closure_env);
+            let env = evaluate_extend_env(env', closure_env);
             evaluate(env, d3);
           }
         };
@@ -1158,7 +1158,7 @@ and eval_rule =
       |> return;
     | Matches(env') =>
       // extend environment with new bindings introduced
-      let* env = evaluate_extend_env(env', env);
+      let env = evaluate_extend_env(env', env);
       evaluate(env, d);
     // by the rule and evaluate the expression.
     | DoesNotMatch =>
@@ -1172,10 +1172,11 @@ and eval_rule =
  */
 and evaluate_extend_env =
     (new_bindings: Environment.t, to_extend: ClosureEnvironment.t)
-    : m(ClosureEnvironment.t) => {
-  let map =
-    Environment.union(new_bindings, ClosureEnvironment.map_of(to_extend));
-  map |> ClosureEnvironment.of_environment |> with_eig;
+    : ClosureEnvironment.t => {
+  to_extend
+  |> ClosureEnvironment.map_of
+  |> Environment.union(new_bindings)
+  |> ClosureEnvironment.of_environment;
 }
 
 /**
@@ -1274,7 +1275,6 @@ and evaluate_test_eq =
 
 let evaluate = (env, d) => {
   let es = EvaluatorState.init;
-  let (env, es) =
-    es |> EvaluatorState.with_eig(ClosureEnvironment.of_environment(env));
+  let env = ClosureEnvironment.of_environment(env);
   evaluate(env, d, es);
 };
diff --git a/src/haz3lcore/dynamics/EvaluatorMonad.re b/src/haz3lcore/dynamics/EvaluatorMonad.re
index 42989f65dc..0e00017966 100644
--- a/src/haz3lcore/dynamics/EvaluatorMonad.re
+++ b/src/haz3lcore/dynamics/EvaluatorMonad.re
@@ -2,10 +2,6 @@ include Util.StateMonad.Make(EvaluatorState);
 
 open Syntax;
 
-let get_eig = get >>| EvaluatorState.get_eig;
-let put_eig = eig => modify(EvaluatorState.put_eig(eig));
-let with_eig = f => modify'(EvaluatorState.with_eig(f));
-
 let take_step = get >>= (state => put(EvaluatorState.take_step(state)));
 
 let add_test = (id, report) =>
diff --git a/src/haz3lcore/dynamics/EvaluatorMonad.rei b/src/haz3lcore/dynamics/EvaluatorMonad.rei
index 262a899b6e..1de6dc4c00 100644
--- a/src/haz3lcore/dynamics/EvaluatorMonad.rei
+++ b/src/haz3lcore/dynamics/EvaluatorMonad.rei
@@ -4,21 +4,6 @@
 
 include Util.StateMonad.S with type state = EvaluatorState.t;
 
-/**
-  See {!val:EvaluatorState.get_eig}.
- */
-let get_eig: t(EnvironmentIdGen.t);
-
-/**
-  See {!val:EvaluatorState.put_eig}.
- */
-let put_eig: EnvironmentIdGen.t => t(unit);
-
-/**
-  See {!val:EvaluatorState.with_eig}.
- */
-let with_eig: (EnvironmentIdGen.t => ('a, EnvironmentIdGen.t)) => t('a);
-
 /**
   See {!val:EvaluatorState.take_step}
  */
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.re b/src/haz3lcore/dynamics/EvaluatorPost.re
index 18d4ea2b44..01aef79d29 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.re
+++ b/src/haz3lcore/dynamics/EvaluatorPost.re
@@ -1,31 +1,19 @@
 module PpMonad = {
   include Util.StateMonad.Make({
     [@deriving sexp]
-    type t = (
-      EnvironmentIdMap.t(ClosureEnvironment.t),
-      HoleInstanceInfo_.t,
-      EnvironmentIdGen.t,
-    );
+    type t = (EnvironmentIdMap.t(ClosureEnvironment.t), HoleInstanceInfo_.t);
   });
 
   open Syntax;
 
-  let get_pe = get >>| (((pe, _, _)) => pe);
+  let get_pe = get >>| (((pe, _)) => pe);
   let pe_add = (ei, env) =>
-    modify(((pe, hii, eig)) =>
-      (pe |> EnvironmentIdMap.add(ei, env), hii, eig)
-    );
+    modify(((pe, hii)) => (pe |> EnvironmentIdMap.add(ei, env), hii));
 
   let hii_add_instance = (u, env) =>
-    modify'(((pe, hii, eig)) => {
+    modify'(((pe, hii)) => {
       let (hii, i) = HoleInstanceInfo_.add_instance(hii, u, env);
-      (i, (pe, hii, eig));
-    });
-
-  let with_eig = f =>
-    modify'(((pe, hii, eig)) => {
-      let (x, eig) = f(eig);
-      (x, (pe, hii, eig));
+      (i, (pe, hii));
     });
 };
 
@@ -242,7 +230,7 @@ and pp_eval_env = (env: ClosureEnvironment.t): m(ClosureEnvironment.t) => {
                  FixF(f, ty, d1);
                | d => pp_eval(d)
                };
-             with_eig(ClosureEnvironment.extend(env', (x, d')));
+             ClosureEnvironment.extend(env', (x, d')) |> return;
            },
            Environment.empty |> ClosureEnvironment.wrap(ei) |> return,
          );
@@ -551,13 +539,11 @@ let track_children = (hii: HoleInstanceInfo.t): HoleInstanceInfo.t =>
     hii,
   );
 
-let postprocess =
-    (d: DHExp.t, eig: EnvironmentIdGen.t)
-    : ((HoleInstanceInfo.t, DHExp.t), EnvironmentIdGen.t) => {
+let postprocess = (d: DHExp.t): (HoleInstanceInfo.t, DHExp.t) => {
   /* Substitution and hole numbering postprocessing */
-  let ((_, hii, eig), d) =
+  let ((_, hii), d) =
     Util.TimeUtil.measure_time("pp_eval", true, () =>
-      pp_eval(d, (EnvironmentIdMap.empty, HoleInstanceInfo_.empty, eig))
+      pp_eval(d, (EnvironmentIdMap.empty, HoleInstanceInfo_.empty))
     );
 
   /* Build hole instance info. */
@@ -591,5 +577,5 @@ let postprocess =
     );
 
   /* Perform hole parent tracking. */
-  ((hii, d), eig);
+  (hii, d);
 };
diff --git a/src/haz3lcore/dynamics/EvaluatorPost.rei b/src/haz3lcore/dynamics/EvaluatorPost.rei
index 4a18dd3470..97df603897 100644
--- a/src/haz3lcore/dynamics/EvaluatorPost.rei
+++ b/src/haz3lcore/dynamics/EvaluatorPost.rei
@@ -68,6 +68,4 @@ exception Exception(error);
 
   See also HoleInstanceInfo.rei/HoleInstanceInfo_.rei.
  */
-let postprocess:
-  (DHExp.t, EnvironmentIdGen.t) =>
-  ((HoleInstanceInfo.t, DHExp.t), EnvironmentIdGen.t);
+let postprocess: DHExp.t => (HoleInstanceInfo.t, DHExp.t);
diff --git a/src/haz3lcore/dynamics/EvaluatorState.re b/src/haz3lcore/dynamics/EvaluatorState.re
index c2bff80641..7de699c61c 100644
--- a/src/haz3lcore/dynamics/EvaluatorState.re
+++ b/src/haz3lcore/dynamics/EvaluatorState.re
@@ -1,22 +1,10 @@
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = {
-  eig: EnvironmentIdGen.t,
   stats: EvaluatorStats.t,
   tests: TestMap.t,
 };
 
-let init = {
-  eig: EnvironmentIdGen.init,
-  stats: EvaluatorStats.initial,
-  tests: TestMap.empty,
-};
-
-let get_eig = ({eig, _}) => eig;
-let put_eig = (eig, es) => {...es, eig};
-let with_eig = (f, es) => {
-  let (x, eig) = es |> get_eig |> f;
-  (x, es |> put_eig(eig));
-};
+let init = {stats: EvaluatorStats.initial, tests: TestMap.empty};
 
 let take_step = ({stats, _} as es) => {
   ...es,
diff --git a/src/haz3lcore/dynamics/EvaluatorState.rei b/src/haz3lcore/dynamics/EvaluatorState.rei
index 3774c7e718..2593d7e326 100644
--- a/src/haz3lcore/dynamics/EvaluatorState.rei
+++ b/src/haz3lcore/dynamics/EvaluatorState.rei
@@ -16,22 +16,6 @@ type t;
  */
 let init: t;
 
-/**
-  [get_eig es] is current environment id generator.
- */
-let get_eig: t => EnvironmentIdGen.t;
-
-/**
-  [put_eig eig es] is [es] with the environment id generator [eig].
- */
-let put_eig: (EnvironmentIdGen.t, t) => t;
-
-/**
-  [with_eig f es] calls [f] with the current environment id generator, updating
-  [es] afterwards.
- */
-let with_eig: (EnvironmentIdGen.t => ('a, EnvironmentIdGen.t), t) => ('a, t);
-
 /**
   [take_step es] is [es] with the updated step count.
  */

From d3fe0569ac7ce7605d963071a7148c1569685b25 Mon Sep 17 00:00:00 2001
From: disconcision <me@andrewblinn.com>
Date: Thu, 26 Oct 2023 15:26:06 -0400
Subject: [PATCH 2/3] fix dhexp error hole formatting

---
 src/haz3lweb/www/style.css | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/haz3lweb/www/style.css b/src/haz3lweb/www/style.css
index 6a646dc172..a8ea7bcae0 100644
--- a/src/haz3lweb/www/style.css
+++ b/src/haz3lweb/www/style.css
@@ -1517,6 +1517,7 @@ svg.expandable path {
 }
 
 .result {
+  padding-top: 0.1em;
   min-height: 1.6em;
   width: 100%;
   overflow-y: hidden;
@@ -1548,8 +1549,6 @@ svg.expandable path {
 
 .DHCode svg.err-hole {
   fill: #d001;
-  transform: scaleY(0.8);
-  /* HACK(andrew) */
   stroke-dasharray: 1, 1;
   stroke: var(--err-color);
   stroke-width: 1.2px;

From a01f617c44cbc5481228b667c43720e7d84b2a15 Mon Sep 17 00:00:00 2001
From: Matt <ruiz2357m@gmail.com>
Date: Sun, 5 Nov 2023 14:06:59 -0500
Subject: [PATCH 3/3] FixF type fix

---
 src/haz3lcore/dynamics/Elaborator.re | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index 47e2d484c2..637fa5f8da 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -206,14 +206,14 @@ let rec dhexp_of_uexp =
         let* dp = dhpat_of_upat(m, p);
         let* ddef = dhexp_of_uexp(m, def);
         let* dbody = dhexp_of_uexp(m, body);
-        let+ ty_body = fixed_exp_typ(m, body);
+        let+ ty = fixed_pat_typ(m, p);
         switch (Term.UPat.get_recursive_bindings(p)) {
         | None =>
           /* not recursive */
           DHExp.Let(dp, add_name(Term.UPat.get_var(p), ddef), dbody)
         | Some([f]) =>
           /* simple recursion */
-          Let(dp, FixF(f, ty_body, add_name(Some(f), ddef)), dbody)
+          Let(dp, FixF(f, ty, add_name(Some(f), ddef)), dbody)
         | Some(fs) =>
           /* mutual recursion */
           let ddef =
@@ -235,7 +235,7 @@ let rec dhexp_of_uexp =
                  },
                  (0, ddef),
                );
-          Let(dp, FixF(self_id, ty_body, substituted_def), dbody);
+          Let(dp, FixF(self_id, ty, substituted_def), dbody);
         };
       | Ap(fn, arg) =>
         let* c_fn = dhexp_of_uexp(m, fn);