From 1ba9e2e845eec81083d591764cb9570fc1b0598c Mon Sep 17 00:00:00 2001
From: Jiezhong Yang <pigumar@umich.edu>
Date: Sat, 4 May 2024 13:36:23 -0400
Subject: [PATCH] Revert "add Mode.of_constraint"

This reverts commit b3510ee982899b6d4b14f2b3ebd0cfd74ea6c09c.
---
 src/haz3lcore/statics/Info.re    |  6 +++++-
 src/haz3lcore/statics/Mode.re    |  6 ------
 src/haz3lcore/statics/Statics.re | 21 ++++++++-------------
 3 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re
index b71de65ccf..43acfb0e10 100644
--- a/src/haz3lcore/statics/Info.re
+++ b/src/haz3lcore/statics/Info.re
@@ -575,7 +575,11 @@ let derived_pat =
   let cls = Cls.Pat(UPat.cls_of_term(upat.term));
   let status = status_pat(ctx, mode, self);
   let ty = fixed_typ_pat(ctx, mode, self);
-  let constraint_mode = Mode.of_constraint(mode, constraint_ty);
+  let constraint_mode =
+    switch (constraint_ty) {
+    | None => mode
+    | Some(ty) => Ana(ty)
+    };
   let constraint_ =
     fixed_constraint_pat(upat, ctx, constraint_mode, self, constraint_);
   {
diff --git a/src/haz3lcore/statics/Mode.re b/src/haz3lcore/statics/Mode.re
index c0d2f65429..f1e3550091 100644
--- a/src/haz3lcore/statics/Mode.re
+++ b/src/haz3lcore/statics/Mode.re
@@ -127,9 +127,3 @@ let of_deferred_ap_args = (length: int, ty_ins: list(Typ.t)): list(t) =>
       ? ty_ins : List.init(length, _ => Typ.Unknown(Internal))
   )
   |> List.map(ty => Ana(ty));
-
-let of_constraint = (mode: t, constraint_ty: option(Typ.t)): t =>
-  switch (constraint_ty) {
-  | None => mode
-  | Some(ty) => Ana(ty)
-  };
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index c161b55086..0bfac2a762 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -485,7 +485,6 @@ and uexp_to_info_map =
                   // Mark patterns as redundant at the top level
                   // because redundancy doesn't make sense in a smaller context
                   ~constraint_=p_constraint,
-                  ~constraint_ty=Some(constraint_ty),
                 );
               (
                 // Override the info for the single upat
@@ -680,24 +679,20 @@ and upat_to_info_map =
     add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
   | Constructor(ctr) =>
     let self = Self.of_ctr(ctx, ctr);
-    let constraint_mode = Mode.of_constraint(mode, constraint_ty);
-    atomic(self, Constraint.of_ctr(ctx, constraint_mode, ctr, self));
+    atomic(self, Constraint.of_ctr(ctx, mode, ctr, self));
   | Ap(fn, arg) =>
     let ctr = UPat.ctr_name(fn);
     let fn_mode = Mode.of_ap(ctx, mode, ctr);
     let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m);
     let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
     let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m);
-    let constraint_mode = Mode.of_constraint(mode, constraint_ty);
-    let constraint_ =
-      Constraint.of_ap(
-        ctx,
-        constraint_mode,
-        ctr,
-        arg.constraint_,
-        Some(ty_out),
-      );
-    add(~self=Just(ty_out), ~ctx=arg.ctx, ~constraint_, m);
+    add(
+      ~self=Just(ty_out),
+      ~ctx=arg.ctx,
+      ~constraint_=
+        Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)),
+      m,
+    );
   | TypeAnn(p, ann) =>
     let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m);
     let (p, m) = go(~ctx, ~mode=Ana(ann.ty), p, m);