From 5bb445fcce7b184d0abeb8f152fad580630fc3bf Mon Sep 17 00:00:00 2001
From: Haoxiang Fei <fettes@umich.edu>
Date: Mon, 23 Dec 2024 22:46:34 +0800
Subject: [PATCH] fix statics

---
 src/haz3lcore/dynamics/EvalCtx.re       |  3 +--
 src/haz3lcore/dynamics/FilterMatcher.re | 16 +++++++++++---
 src/haz3lcore/statics/Statics.re        | 16 +++++++-------
 src/haz3lschool/Exercise.re             | 29 ++++++++++++-------------
 4 files changed, 36 insertions(+), 28 deletions(-)

diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
index 218165f5e..7aea68053 100644
--- a/src/haz3lcore/dynamics/EvalCtx.re
+++ b/src/haz3lcore/dynamics/EvalCtx.re
@@ -121,8 +121,7 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
       ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
     | MultiHole(ctx, (ld, rd)) =>
       let d = compose(ctx, d);
-      MultiHole(ListUtil.rev_concat(ld, [TermBase.Exp(d), ...rd]))
-      |> wrap;
+      MultiHole(ListUtil.rev_concat(ld, [TermBase.Exp(d), ...rd])) |> wrap;
     | Let1(dp, ctx, d2) =>
       let d = compose(ctx, d);
       Let(dp, d, d2) |> wrap;
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 390fc3765..4d90f79b7 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -203,7 +203,7 @@ let rec matches_exp =
     | (Deferral(_), _) => false
 
     | (Filter(da, dp, dd), Filter(fa, fp, fd)) =>
-      da == fa && matches_exp(dp, fp) && matches_exp(dd, fd)
+      da == fa && matches_exp(dd, fd)
     | (Filter(_), _) => false
 
     | (Bool(dv), Bool(fv)) => dv == fv
@@ -234,8 +234,18 @@ let rec matches_exp =
       | (_, EmptyHole) => matches_exp(d, f)
       | _ =>
         let id = alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4));
-        let d' = DHExp.ty_subst((Var(id) : TermBase.typ_term) |> IdTagged.fresh, dpat, d);
-        let f' = DHExp.ty_subst((Var(id) : TermBase.typ_term) |> IdTagged.fresh, fpat, f);
+        let d' =
+          DHExp.ty_subst(
+            (Var(id): TermBase.typ_term) |> IdTagged.fresh,
+            dpat,
+            d,
+          );
+        let f' =
+          DHExp.ty_subst(
+            (Var(id): TermBase.typ_term) |> IdTagged.fresh,
+            fpat,
+            f,
+          );
         matches_exp(d', f');
       }
     | (TypFun(_), _) => false
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 8710a5683..a2e29b4df 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -337,17 +337,17 @@ and uexp_to_info_map =
       let go = go'(~ctx);
       switch (pat.term) {
       | Ap(_, fn, arg) =>
-        let fn_mode =
-          Mode.of_ap(ctx, Ana(Filter |> Typ.temp), UExp.ctr_name(fn));
+        let self_ty = Unknown(Internal) |> Typ.temp;
+        let fn_mode = Mode.of_ap(ctx, Ana(self_ty), UExp.ctr_name(fn));
         let (fn, m) =
           go'(~ctx=Builtins.filter_keyword_ctx_init, ~mode=fn_mode, fn, m);
-        let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
+        let (ty_in, _) = Typ.matched_arrow(ctx, fn.ty);
         let (arg, m) = go(~mode=Ana(ty_in), arg, m, ~is_in_filter=true);
-        let self: Self.t =
-          Id.is_nullary_ap_flag(arg.term.ids)
-          && !Typ.is_consistent(ctx, ty_in, Prod([]) |> Typ.temp)
-            ? BadTrivAp(ty_in) : Just(ty_out);
-        add(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m);
+        add(
+          ~self=Just(self_ty),
+          ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]),
+          m,
+        );
       | _ =>
         go'(
           ~ctx=Builtins.filter_keyword_ctx_init,
diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re
index 05274e938..2b2d0706d 100644
--- a/src/haz3lschool/Exercise.re
+++ b/src/haz3lschool/Exercise.re
@@ -568,21 +568,20 @@ module F = (ExerciseEnv: ExerciseEnv) => {
     hidden_tests: 'a,
   };
 
-  let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t =>
-    {
-      term:
-        Filter(
-          Some(FilterAction.(act, One)),
-          {
-            term: Constructor("$e", Unknown(Internal) |> Typ.temp),
-            copied: false,
-            ids: [Id.mk()],
-          },
-          term,
-        ),
-      copied: false,
-      ids: [Id.mk()],
-    };
+  let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => {
+    term:
+      Filter(
+        Some(FilterAction.(act, One)),
+        {
+          term: Constructor("$e", Unknown(Internal) |> Typ.temp),
+          copied: false,
+          ids: [Id.mk()],
+        },
+        term,
+      ),
+    copied: false,
+    ids: [Id.mk()],
+  };
 
   let term_of = (editor: Editor.t): UExp.t =>
     MakeTerm.from_zip_for_sem(editor.state.zipper).term;