fix statics

hazelgrove · Dec 23, 2024 · 5bb445f · 5bb445f
1 parent f131925
commit 5bb445f
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 28 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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;