fix: remove filter vars in context inspector (#1541)

hazelgrove · Feb 24, 2025 · d55ff4a · d55ff4a
2 parents 882dfda + 250146c
commit d55ff4a
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 1 deletion.
diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re
@@ -175,5 +175,24 @@ let filter_duplicates = (ctx: t): t =>
      )
   |> (((ctx, _, _)) => List.rev(ctx));
 
+let filter_stepper_filter_variables = (ctx: t): t =>
+  ctx
+  |> List.fold_left(
+       (ctx, entry) => {
+         switch (entry) {
+         | VarEntry({name, _})
+         | ConstructorEntry({name, _})
+         | TVarEntry({name, _}) =>
+           if (String.starts_with(~prefix="$", name)) {
+             ctx;
+           } else {
+             [entry, ...ctx];
+           }
+         }
+       },
+       [],
+     )
+  |> List.rev;
+
 let shadows_typ = (ctx: t, name: string): bool =>
   Form.is_base_typ(name) || lookup_tvar(ctx, name) != None;
diff --git a/src/haz3lweb/view/ContextInspector.re b/src/haz3lweb/view/ContextInspector.re
@@ -56,13 +56,17 @@ let ctx_view = (~globals, ctx: Haz3lcore.Ctx.t): Node.t =>
     ~attrs=[clss(["context-inspector"])],
     List.map(
       context_entry_view(~globals),
-      ctx |> Haz3lcore.Ctx.filter_duplicates |> List.rev,
+      ctx
+      |> Haz3lcore.Ctx.filter_duplicates
+      |> Haz3lcore.Ctx.filter_stepper_filter_variables
+      |> List.rev,
     ),
   );
 
 let ctx_sorts_view = (~globals, ci: Haz3lcore.Statics.Info.t) =>
   Haz3lcore.Info.ctx_of(ci)
   |> Haz3lcore.Ctx.filter_duplicates
+  |> Haz3lcore.Ctx.filter_stepper_filter_variables
   |> List.rev
   |> List.map(context_entry_view(~globals));