From 8ad54831653e20418977f4d63b7efe52e8b4ca31 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Wed, 2 Oct 2024 09:13:32 -0400
Subject: [PATCH 1/3] Add Eq deriving so that we can test the full editor

---
 src/haz3lcore/dune                    |  3 ++-
 src/haz3lcore/lang/Precedence.re      |  2 +-
 src/haz3lcore/lang/Sort.re            |  2 +-
 src/haz3lcore/tiles/Base.re           |  6 +++--
 src/haz3lcore/tiles/Grout.re          |  4 +--
 src/haz3lcore/tiles/Label.re          |  2 +-
 src/haz3lcore/tiles/Mold.re           |  2 +-
 src/haz3lcore/tiles/Nib.re            |  4 +--
 src/haz3lcore/tiles/Nibs.re           |  2 +-
 src/haz3lcore/tiles/Piece.re          |  2 +-
 src/haz3lcore/tiles/Secondary.re      |  5 ++--
 src/haz3lcore/tiles/Segment.re        |  2 +-
 src/haz3lcore/tiles/Token.re          |  2 +-
 src/haz3lcore/zipper/Ancestor.re      |  5 ++--
 src/haz3lcore/zipper/Ancestors.re     |  4 +--
 src/haz3lcore/zipper/Backpack.re      |  2 +-
 src/haz3lcore/zipper/Editor.re        |  7 +++---
 src/haz3lcore/zipper/Relatives.re     |  2 +-
 src/haz3lcore/zipper/Selection.re     |  6 ++---
 src/haz3lcore/zipper/Siblings.re      |  2 +-
 src/haz3lcore/zipper/Zipper.re        |  4 +--
 src/haz3lcore/zipper/ZipperBase.re    |  4 +--
 src/haz3lcore/zipper/action/Action.re | 36 +++++++++++++--------------
 src/util/Direction.re                 |  2 +-
 src/util/Point.re                     |  6 ++---
 src/util/dune                         |  3 ++-
 26 files changed, 64 insertions(+), 57 deletions(-)

diff --git a/src/haz3lcore/dune b/src/haz3lcore/dune
index a0d9770816..812c2a68d4 100644
--- a/src/haz3lcore/dune
+++ b/src/haz3lcore/dune
@@ -12,7 +12,8 @@
    js_of_ocaml-ppx
    ppx_let
    ppx_sexp_conv
-   ppx_deriving.show)))
+   ppx_deriving.show
+   ppx_deriving.eq)))
 
 (env
  (dev
diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re
index 7d72b66404..23bbc9466f 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -3,7 +3,7 @@ open Util;
 /**
  * higher precedence means lower int representation
  */
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = int;
 
 let max: t = 0;
diff --git a/src/haz3lcore/lang/Sort.re b/src/haz3lcore/lang/Sort.re
index 2b66c3282b..c75225e476 100644
--- a/src/haz3lcore/lang/Sort.re
+++ b/src/haz3lcore/lang/Sort.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t =
   | Any
   | Nul
diff --git a/src/haz3lcore/tiles/Base.re b/src/haz3lcore/tiles/Base.re
index 8c127d83ba..0482defc2c 100644
--- a/src/haz3lcore/tiles/Base.re
+++ b/src/haz3lcore/tiles/Base.re
@@ -3,7 +3,7 @@ open Util;
 /* The different kinds of projector. New projectors
  * types need to be registered here in order to be
  * able to create and update their instances */
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type kind =
   | Fold
   | Info
@@ -12,7 +12,7 @@ type kind =
   | SliderF
   | TextArea;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type segment = list(piece)
 and piece =
   | Tile(tile)
@@ -25,6 +25,7 @@ and tile = {
   // - length(shards) <= length(label)
   // - length(shards) == length(children) + 1
   // - sort(shards) == shards
+  [@equal (_, _) => true]
   id: Id.t,
   label: Label.t,
   mold: Mold.t,
@@ -32,6 +33,7 @@ and tile = {
   children: list(segment),
 }
 and projector = {
+  [@equal (_, _) => true]
   id: Id.t,
   kind,
   syntax: piece,
diff --git a/src/haz3lcore/tiles/Grout.re b/src/haz3lcore/tiles/Grout.re
index 496de68f10..9223b293be 100644
--- a/src/haz3lcore/tiles/Grout.re
+++ b/src/haz3lcore/tiles/Grout.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type shape =
   | Convex
   | Concave;
@@ -10,7 +10,7 @@ type t = {
   id: Id.t,
   shape,
 };
-
+let equal = (a: t, b: t) => a.shape == b.shape;
 let id = g => g.id;
 
 let shapes = g =>
diff --git a/src/haz3lcore/tiles/Label.re b/src/haz3lcore/tiles/Label.re
index e26eeaa5a8..f47994764a 100644
--- a/src/haz3lcore/tiles/Label.re
+++ b/src/haz3lcore/tiles/Label.re
@@ -1,6 +1,6 @@
 open Util;
 
 /* A label is the textual expression of a form's delimiters */
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = list(Token.t);
 exception Empty_label;
diff --git a/src/haz3lcore/tiles/Mold.re b/src/haz3lcore/tiles/Mold.re
index 743fcb0d18..a40dba0017 100644
--- a/src/haz3lcore/tiles/Mold.re
+++ b/src/haz3lcore/tiles/Mold.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   out: Sort.t,
   in_: list(Sort.t),
diff --git a/src/haz3lcore/tiles/Nib.re b/src/haz3lcore/tiles/Nib.re
index 863ea9bd9f..81c2f2ed65 100644
--- a/src/haz3lcore/tiles/Nib.re
+++ b/src/haz3lcore/tiles/Nib.re
@@ -1,7 +1,7 @@
 open Util;
 
 module Shape = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type t =
     | Convex
     | Concave(Precedence.t);
@@ -45,7 +45,7 @@ module Shape = {
     };
 };
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   shape: Shape.t,
   sort: Sort.t,
diff --git a/src/haz3lcore/tiles/Nibs.re b/src/haz3lcore/tiles/Nibs.re
index 0c4225a279..88df87de86 100644
--- a/src/haz3lcore/tiles/Nibs.re
+++ b/src/haz3lcore/tiles/Nibs.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = (Nib.t, Nib.t);
 
 [@deriving show]
diff --git a/src/haz3lcore/tiles/Piece.re b/src/haz3lcore/tiles/Piece.re
index fc6207a979..bade3f9a6f 100644
--- a/src/haz3lcore/tiles/Piece.re
+++ b/src/haz3lcore/tiles/Piece.re
@@ -1,6 +1,6 @@
 include Base;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = piece;
 
 let secondary = w => Secondary(w);
diff --git a/src/haz3lcore/tiles/Secondary.re b/src/haz3lcore/tiles/Secondary.re
index c973469254..d075363fa1 100644
--- a/src/haz3lcore/tiles/Secondary.re
+++ b/src/haz3lcore/tiles/Secondary.re
@@ -1,11 +1,11 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type cls =
   | Whitespace
   | Comment;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type secondary_content =
   | Whitespace(string)
   | Comment(string);
@@ -16,6 +16,7 @@ type t = {
   content: secondary_content,
 };
 
+let equal = (a: t, b: t) => a.content == b.content;
 let cls_of = (s: t): cls =>
   switch (s.content) {
   | Whitespace(_) => Whitespace
diff --git a/src/haz3lcore/tiles/Segment.re b/src/haz3lcore/tiles/Segment.re
index de8689f08a..463c4c643f 100644
--- a/src/haz3lcore/tiles/Segment.re
+++ b/src/haz3lcore/tiles/Segment.re
@@ -2,7 +2,7 @@ open Util;
 
 exception Empty_segment;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = Base.segment;
 
 let empty = [];
diff --git a/src/haz3lcore/tiles/Token.re b/src/haz3lcore/tiles/Token.re
index 8b68de1eb3..33df2d7203 100644
--- a/src/haz3lcore/tiles/Token.re
+++ b/src/haz3lcore/tiles/Token.re
@@ -1,7 +1,7 @@
 open Util;
 
 // make an enum
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = string;
 
 module Index = {
diff --git a/src/haz3lcore/zipper/Ancestor.re b/src/haz3lcore/zipper/Ancestor.re
index 498b18b93e..9ae42e30e8 100644
--- a/src/haz3lcore/zipper/Ancestor.re
+++ b/src/haz3lcore/zipper/Ancestor.re
@@ -2,11 +2,12 @@ open Util;
 
 exception Empty_shard_affix;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type step = int;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
+  [@equal (_, _) => true]
   id: Id.t,
   label: Label.t,
   mold: Mold.t,
diff --git a/src/haz3lcore/zipper/Ancestors.re b/src/haz3lcore/zipper/Ancestors.re
index 2acc7d0838..0cf137da54 100644
--- a/src/haz3lcore/zipper/Ancestors.re
+++ b/src/haz3lcore/zipper/Ancestors.re
@@ -1,9 +1,9 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type generation = (Ancestor.t, Siblings.t);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = list(generation);
 
 let empty = [];
diff --git a/src/haz3lcore/zipper/Backpack.re b/src/haz3lcore/zipper/Backpack.re
index b704e36721..ac45789c9c 100644
--- a/src/haz3lcore/zipper/Backpack.re
+++ b/src/haz3lcore/zipper/Backpack.re
@@ -203,7 +203,7 @@ module ShardInfo = {
   };
 };
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = list(Selection.t);
 
 let empty = [];
diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re
index bdb3e014cc..82476919d9 100644
--- a/src/haz3lcore/zipper/Editor.re
+++ b/src/haz3lcore/zipper/Editor.re
@@ -140,6 +140,7 @@ module State = {
     meta: Meta.t,
   };
 
+  let equal = (a: t, b: t) => Zipper.equal(a.zipper, b.zipper);
   let init = (zipper, ~settings: CoreSettings.t) => {
     zipper,
     meta: Meta.init(zipper, ~settings),
@@ -152,9 +153,9 @@ module State = {
 };
 
 module History = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type affix = list((Action.t, State.t));
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type t = (affix, affix);
 
   let empty = ([], []);
@@ -165,7 +166,7 @@ module History = {
   );
 };
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   state: State.t,
   history: History.t,
diff --git a/src/haz3lcore/zipper/Relatives.re b/src/haz3lcore/zipper/Relatives.re
index 251cdbc4e9..65cf81c324 100644
--- a/src/haz3lcore/zipper/Relatives.re
+++ b/src/haz3lcore/zipper/Relatives.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   siblings: Siblings.t,
   ancestors: Ancestors.t,
diff --git a/src/haz3lcore/zipper/Selection.re b/src/haz3lcore/zipper/Selection.re
index 92d6509fb8..4d119ebd8b 100644
--- a/src/haz3lcore/zipper/Selection.re
+++ b/src/haz3lcore/zipper/Selection.re
@@ -1,16 +1,16 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type buffer =
   //| Parsed
   | Unparsed;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type mode =
   | Normal
   | Buffer(buffer);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   focus: Direction.t,
   content: Segment.t,
diff --git a/src/haz3lcore/zipper/Siblings.re b/src/haz3lcore/zipper/Siblings.re
index 332b63f8df..78d4f17966 100644
--- a/src/haz3lcore/zipper/Siblings.re
+++ b/src/haz3lcore/zipper/Siblings.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = (Segment.t, Segment.t);
 
 let empty = Segment.(empty, empty);
diff --git a/src/haz3lcore/zipper/Zipper.re b/src/haz3lcore/zipper/Zipper.re
index f87fb964e6..7f4fd9d799 100644
--- a/src/haz3lcore/zipper/Zipper.re
+++ b/src/haz3lcore/zipper/Zipper.re
@@ -15,13 +15,13 @@ let init: unit => t =
 
 let next_blank = _ => Id.mk();
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type chunkiness =
   | ByChar
   | MonoByChar
   | ByToken;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type planar =
   | Up
   | Down
diff --git a/src/haz3lcore/zipper/ZipperBase.re b/src/haz3lcore/zipper/ZipperBase.re
index cb6311a4b8..ae73d999c3 100644
--- a/src/haz3lcore/zipper/ZipperBase.re
+++ b/src/haz3lcore/zipper/ZipperBase.re
@@ -1,7 +1,7 @@
 open Util;
 
 module Caret = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type t =
     | Outer
     | Inner(int, int);
@@ -19,7 +19,7 @@ module Caret = {
 };
 
 // assuming single backpack, shards may appear in selection, backpack, or siblings
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   selection: Selection.t,
   backpack: Backpack.t,
diff --git a/src/haz3lcore/zipper/action/Action.re b/src/haz3lcore/zipper/action/Action.re
index 85b24be4f1..be0cacf004 100644
--- a/src/haz3lcore/zipper/action/Action.re
+++ b/src/haz3lcore/zipper/action/Action.re
@@ -2,7 +2,7 @@ open Util;
 
 open Zipper;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type piece_goal =
   | Grout;
 
@@ -14,28 +14,28 @@ let of_piece_goal =
       | _ => false
     );
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type goal =
   | Point(Point.t)
   | Piece(piece_goal, Direction.t);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type move =
   | Extreme(planar)
   | Local(planar)
   | Goal(goal);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type jump_target =
-  | TileId(Id.t)
+  | TileId([@equal (_, _) => true] Id.t)
   | BindingSiteOfIndicatedVar;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type rel =
   | Current
-  | Id(Id.t, Direction.t);
+  | Id([@equal (_, _) => true] Id.t, Direction.t);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type select =
   | All
   | Resize(move)
@@ -47,27 +47,27 @@ type select =
  * projectors,as distinguished from external_action,
  * which defines the actions available internally to all projectors,
  * and from each projector's own internal action type */
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type project =
   | SetIndicated(Base.kind) /* Project syntax at caret */
   | ToggleIndicated(Base.kind) /* Un/Project syntax at caret */
-  | Remove(Id.t) /* Remove projector at Id */
-  | SetSyntax(Id.t, Piece.t) /* Set underlying syntax */
-  | SetModel(Id.t, string) /* Set serialized projector model */
-  | Focus(Id.t, option(Util.Direction.t)) /* Pass control to projector */
-  | Escape(Id.t, Direction.t); /* Pass control to parent editor */
+  | Remove([@equal (_, _) => true] Id.t) /* Remove projector at Id */
+  | SetSyntax([@equal (_, _) => true] Id.t, Piece.t) /* Set underlying syntax */
+  | SetModel([@equal (_, _) => true] Id.t, string) /* Set serialized projector model */
+  | Focus([@equal (_, _) => true] Id.t, option(Util.Direction.t)) /* Pass control to projector */
+  | Escape([@equal (_, _) => true] Id.t, Direction.t); /* Pass control to parent editor */
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type agent =
   | TyDi;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type buffer =
   | Set(agent)
   | Clear
   | Accept;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t =
   | Reparse
   | Buffer(buffer)
@@ -87,7 +87,7 @@ type t =
   | Put_down;
 
 module Failure = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type t =
     | Cant_move
     | Cant_insert
diff --git a/src/util/Direction.re b/src/util/Direction.re
index b59b7faac0..7b611423ad 100644
--- a/src/util/Direction.re
+++ b/src/util/Direction.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t =
   | Left
   | Right;
diff --git a/src/util/Point.re b/src/util/Point.re
index 6a8f80b698..cc2249c41d 100644
--- a/src/util/Point.re
+++ b/src/util/Point.re
@@ -1,12 +1,12 @@
 open Sexplib.Std;
 open Ppx_yojson_conv_lib.Yojson_conv;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type row = int;
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type col = int;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = {
   row,
   col,
diff --git a/src/util/dune b/src/util/dune
index f50e6ac0f7..e4b5712916 100644
--- a/src/util/dune
+++ b/src/util/dune
@@ -11,7 +11,8 @@
    ppx_let
    ppx_sexp_conv
    ppx_deriving.show
-   bonsai.ppx_bonsai)))
+   bonsai.ppx_bonsai
+   ppx_deriving.eq)))
 
 (env
  (dev

From 4ef6a65b98fbb69ec0d372c5e7819ef75cb833c3 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Wed, 20 Nov 2024 17:04:24 -0500
Subject: [PATCH 2/3] Add more equality

---
 src/haz3lcore/dynamics/FilterAction.re        |  6 +++---
 .../dynamics/InvalidOperationError.re         |  2 +-
 src/haz3lcore/dynamics/VarBstMap.re           |  7 ++++++-
 src/haz3lcore/dynamics/VarBstMap.rei          |  2 ++
 src/haz3lcore/lang/Operators.re               | 20 +++++++++----------
 src/haz3lcore/lang/term/IdTagged.re           |  2 ++
 src/haz3lcore/statics/Var.re                  |  2 +-
 src/haz3lcore/tiles/Id.re                     |  1 +
 8 files changed, 26 insertions(+), 16 deletions(-)

diff --git a/src/haz3lcore/dynamics/FilterAction.re b/src/haz3lcore/dynamics/FilterAction.re
index 6a4dce5ca3..e176847b84 100644
--- a/src/haz3lcore/dynamics/FilterAction.re
+++ b/src/haz3lcore/dynamics/FilterAction.re
@@ -1,14 +1,14 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type action =
   | Step
   | Eval;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type count =
   | One
   | All;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = (action, count);
 
 let string_of_t = v => {
diff --git a/src/haz3lcore/dynamics/InvalidOperationError.re b/src/haz3lcore/dynamics/InvalidOperationError.re
index b317e64254..41bf053a6f 100644
--- a/src/haz3lcore/dynamics/InvalidOperationError.re
+++ b/src/haz3lcore/dynamics/InvalidOperationError.re
@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t =
   | InvalidOfString
   | IndexOutOfBounds
diff --git a/src/haz3lcore/dynamics/VarBstMap.re b/src/haz3lcore/dynamics/VarBstMap.re
index 2952690388..89a6787014 100644
--- a/src/haz3lcore/dynamics/VarBstMap.re
+++ b/src/haz3lcore/dynamics/VarBstMap.re
@@ -29,7 +29,7 @@ module Inner = {
 };
 
 module VarBstMap0 = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
+  [@deriving (show({with_path: false}), sexp, yojson, eq)]
   type t_('a) = Inner.t('a);
 
   let empty = Inner.empty;
@@ -61,6 +61,8 @@ module VarBstMap0 = {
   let to_list = ctx => ctx |> Inner.to_seq |> List.of_seq;
 
   let of_list = bindings => bindings |> List.to_seq |> Inner.of_seq;
+
+  let equal = Inner.equal;
 };
 
 module Ordered = {
@@ -206,6 +208,9 @@ module Ordered = {
   let without_keys = (keys, m) => {
     filterk(((s, _)) => !List.exists(x => x == s, keys), m);
   };
+
+  let equal_t_ = (cmp, m1, m2) =>
+    VarBstMap0.equal(cmp, m1.map, m2.map) && m1.rev_order == m2.rev_order;
 };
 
 include VarBstMap0;
diff --git a/src/haz3lcore/dynamics/VarBstMap.rei b/src/haz3lcore/dynamics/VarBstMap.rei
index 36a3a20659..01e1b24ad2 100644
--- a/src/haz3lcore/dynamics/VarBstMap.rei
+++ b/src/haz3lcore/dynamics/VarBstMap.rei
@@ -174,4 +174,6 @@ module Ordered: {
     [without_keys] removes all entires with the given keys from the map
    */
   let without_keys: (list(Var.t), t_('a)) => t_('a);
+
+  let equal_t_: (('a, 'a) => bool, t_('a), t_('a)) => bool;
 };
diff --git a/src/haz3lcore/lang/Operators.re b/src/haz3lcore/lang/Operators.re
index aa8842b72b..eda4adcc9c 100644
--- a/src/haz3lcore/lang/Operators.re
+++ b/src/haz3lcore/lang/Operators.re
@@ -1,21 +1,21 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_un_bool =
   | Not;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_un_meta =
   | Unquote;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_un_int =
   | Minus;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_bin_bool =
   | And
   | Or;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_bin_int =
   | Plus
   | Minus
@@ -29,7 +29,7 @@ type op_bin_int =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_bin_float =
   | Plus
   | Minus
@@ -43,25 +43,25 @@ type op_bin_float =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_bin_string =
   | Concat
   | Equals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_un =
   | Meta(op_un_meta)
   | Int(op_un_int)
   | Bool(op_un_bool);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type op_bin =
   | Int(op_bin_int)
   | Float(op_bin_float)
   | Bool(op_bin_bool)
   | String(op_bin_string);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type ap_direction =
   | Forward
   | Reverse;
diff --git a/src/haz3lcore/lang/term/IdTagged.re b/src/haz3lcore/lang/term/IdTagged.re
index 3812b0e83f..d701d14de1 100644
--- a/src/haz3lcore/lang/term/IdTagged.re
+++ b/src/haz3lcore/lang/term/IdTagged.re
@@ -14,6 +14,8 @@ type t('a) = {
   term: 'a,
 };
 
+// TODO This fully ignores ids for equality
+let equal = (eq, a, b) => eq(a.term, b.term);
 // To be used if you want to remove the id from the debug output
 // let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit =
 //   (fmt_a, formatter, ta) => {
diff --git a/src/haz3lcore/statics/Var.re b/src/haz3lcore/statics/Var.re
index 68c3d9d1b3..c52558d0ec 100644
--- a/src/haz3lcore/statics/Var.re
+++ b/src/haz3lcore/statics/Var.re
@@ -1,6 +1,6 @@
 open Util;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type t = string;
 
 let eq = String.equal;
diff --git a/src/haz3lcore/tiles/Id.re b/src/haz3lcore/tiles/Id.re
index 5046dd63c5..ac80856592 100644
--- a/src/haz3lcore/tiles/Id.re
+++ b/src/haz3lcore/tiles/Id.re
@@ -58,6 +58,7 @@ let t_of_yojson: Yojson.Safe.t => Uuidm.t =
 
 type t = Uuidm.t;
 
+let equal: (t, t) => bool = (==);
 let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init());
 
 let compare: (t, t) => int = Uuidm.compare;

From 9efc22b51222dd0106a89aba79e766ac45185ab1 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Wed, 20 Nov 2024 17:05:31 -0500
Subject: [PATCH 3/3] Add equality to termbase types

---
 src/haz3lcore/statics/TermBase.re | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index 02bd8400d4..48b8dfd97d 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -2,7 +2,7 @@ open Util;
 
 let continue = x => x;
 let stop = (_, x) => x;
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type deferral_position_t =
   | InAp
   | OutsideAp;
@@ -46,7 +46,7 @@ type deferral_position_t =
      the id of the closure.
  */
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, eq)]
 type any_t =
   | Exp(exp_t)
   | Pat(pat_t)