Merge remote-tracking branch 'origin/dev' into syntax_playground

hazelgrove · Feb 25, 2025 · 4240da6 · 4240da6
2 parents 7867ed1 + 63e8228
commit 4240da6
Show file tree

Hide file tree

Showing 43 changed files with 1,805 additions and 732 deletions.
diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
@@ -119,7 +119,7 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
       switch (DHExp.term_of(d1)) {
       | Cast(d2, t3, {term: Unknown(_), _}) =>
         /* by canonical forms, d1' must be of the form d<ty'' -> ?> */
-        if (Typ.eq(t3, t2)) {
+        if (Typ.equal(t3, t2)) {
           Some
             (d2); // Rule ITCastSucceed
         } else {
@@ -159,7 +159,7 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
     | (Ground, NotGroundOrHole(_)) =>
       switch (DHExp.term_of(d1)) {
       | Cast(d2, t3, _) =>
-        if (Typ.eq(t3, t2)) {
+        if (Typ.equal(t3, t2)) {
           Some(d2);
         } else {
           None;
@@ -172,7 +172,7 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
 
     | (NotGroundOrHole(_), NotGroundOrHole(_)) =>
       /* they might be eq in this case, so remove cast if so */
-      if (Typ.eq(t1, t2)) {
+      if (Typ.equal(t1, t2)) {
         Some
           (d1); // Rule ITCastId
       } else {

diff --git a/src/haz3lcore/dynamics/Constraint.re b/src/haz3lcore/dynamics/Constraint.re
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -430,7 +430,7 @@ and matches_fun =
 }
 
 and matches_typ = (d: Typ.t, f: Typ.t) => {
-  Typ.eq(d, f);
+  Typ.equal(d, f);
 }
 
 and matches_utpat = (d: TPat.t, f: TPat.t): bool => {

diff --git a/src/haz3lcore/dynamics/Incon.re b/src/haz3lcore/dynamics/Incon.re
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
@@ -18,7 +18,7 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: DHPat.t): bool =>
     | Constructor(_) => false
     | Cast(y, _, _)
     | Parens(y) => binds_var(m, x, y)
-    | Var(y) => Var.eq(x, y)
+    | Var(y) => Var.equal(x, y)
     | TupLabel(_, dp) => binds_var(m, x, dp)
     | Tuple(dps) => dps |> List.exists(binds_var(m, x))
     | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
@@ -34,7 +34,7 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
   let (term, rewrap) = DHExp.unwrap(d2);
   switch (term) {
   | Var(y) =>
-    if (Var.eq(x, y)) {
+    if (Var.equal(x, y)) {
       d1;
     } else {
       d2;