Merge branch 'syntax_playground' into syntax_factory

src/haz3lcore/pretty/ExpToSegment.re

@@ -258,7 +258,7 @@ let rec parenthesize =
     Ap(
       Forward,
       parenthesize(e1) |> paren_assoc_at(Precedence.ap),
-      parenthesize(e2) |> paren_at(Precedence.min),
+      parenthesize(~already_paren=true, e2) |> paren_at(Precedence.min),
     )
     |> rewrap
   | Ap(Reverse, e1, e2) =>
@@ -458,6 +458,7 @@ and parenthesize_typ =
     |> rewrap
   | List(t) =>
     List(parenthesize_typ(t) |> paren_typ_at(Precedence.min)) |> rewrap
+  | Prod([]) => typ
   | Prod(ts) =>
     let inner =
       Prod(

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;

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));
 

test/Test_ExpToSegment.re

@@ -32,12 +32,27 @@ let exp_to_segment =
 let zipper_parse = (s: string) =>
   Option.map(Printer.seg_of_zip, Printer.zipper_of_string(s));
 
+let exp_to_segment_settings: ExpToSegment.Settings.t = {
+  inline: true,
+  fold_case_clauses: false,
+  fold_fn_bodies: false,
+  hide_fixpoints: false,
+  fold_cast_types: false,
+  show_filters: true,
+};
 let equivalent_to_make_term = (serialized: string) => {
   switch (Printer.zipper_of_string(serialized)) {
   | None => Alcotest.fail("Failed to parse term")
   | Some(zb) =>
     let exp = MakeTerm.from_zip_for_sem(zb).term;
-    let seg = Printer.seg_of_zip(zb);
+    let seg =
+      ExpToSegment.exp_to_segment(~settings=exp_to_segment_settings, exp);
+    check(
+      string,
+      "Make term print equivalent: " ++ serialized,
+      serialized,
+      Printer.of_segment(~holes=Some("?"), seg),
+    );
     check(
       segment,
       "Make term equivalent: " ++ serialized,
@@ -47,30 +62,8 @@ let equivalent_to_make_term = (serialized: string) => {
   };
 };
 
-let mk_form = (form_name: Form.compound_form): Piece.t => {
-  let form: Form.t = Form.get(form_name);
-
-  Tile({
-    id: Id.invalid,
-    label: form.label,
-    mold: form.mold,
-    shards: [0],
-    children: [],
-  });
-};
-
 let segmentize =
-  ExpToSegment.exp_to_segment(
-    ~settings={
-      inline: true,
-      fold_case_clauses: false,
-      fold_fn_bodies: false,
-      hide_fixpoints: false,
-      fold_cast_types: false,
-      show_filters: true,
-    },
-    _,
-  );
+  ExpToSegment.exp_to_segment(~settings=exp_to_segment_settings, _);
 
 let tests = (
   "ExpToSegment",
@@ -350,5 +343,22 @@ let tests = (
         );
       },
     ),
+    test_case("Unit type", `Quick, () => {
+      check(
+        string,
+        "Unit type",
+        "()",
+        Printer.of_segment(
+          ~holes=Some("?"),
+          ExpToSegment.typ_to_segment(
+            ~settings=exp_to_segment_settings,
+            Typ.temp(Prod([])),
+          ),
+        ),
+      )
+    }),
+    test_case("Function call", `Quick, () => {
+      equivalent_to_make_term("a(1, 2)")
+    }),
   ],
 );