vlist: vertical list projector on splice sub-editors

Author: Negabinary

src/haz3lcore/pretty/ExpToSegment.re

@@ -1160,13 +1160,40 @@ let concat_segment =
 let (@) = (seg1: Segment.t, seg2: Segment.t): Segment.t =>
   concat_segment(~secondary=AutoFormat, seg1, seg2);
 
+/* Projector-construction hooks, injected by ProjectorInit at module
+ * initialization. ExpToSegment needs to construct projectors (folds,
+ * tables) while printing, but ProjectorInit needs ExpToSegment to print
+ * term-level init overrides, so ExpToSegment cannot depend on
+ * ProjectorInit directly. If the hooks are unregistered, projector
+ * construction degrades to a no-op (the plain syntax is used). */
+module ProjectorHooks = {
+  type t = {
+    init_or_noop:
+      (ProjectorCore.Kind.t, Base.segment, Any.t) => Base.segment,
+    init_or_noop_from_str:
+      (ProjectorCore.Kind.t, Base.segment, Any.t, string) => Base.segment,
+  };
+  let registered: ref(option(t)) = ref(None);
+  let register = (hooks: t): unit => registered := Some(hooks);
+  let init_or_noop = (kind, seg, any) =>
+    switch (registered^) {
+    | Some(hooks) => hooks.init_or_noop(kind, seg, any)
+    | None => seg
+    };
+  let init_or_noop_from_str = (kind, seg, any, str) =>
+    switch (registered^) {
+    | Some(hooks) => hooks.init_or_noop_from_str(kind, seg, any, str)
+    | None => seg
+    };
+};
+
 let fold_if = (condition, pieces) =>
   if (condition) {
     let wrapped =
       mk_form(~secondary=AutoFormat, ParensExp, Id.mk(), [pieces]);
     switch (MakeTerm.for_projection([wrapped])) {
     | None => failwith("ExpToSegment.fold_if")
-    | Some(any) => ProjectorInit.init_or_noop(Fold, pieces, any)
+    | Some(any) => ProjectorHooks.init_or_noop(Fold, pieces, any)
     };
   } else {
     pieces;
@@ -1182,7 +1209,7 @@ let fold_fun_if = (condition, f_name: string, pieces, exp) =>
         always_render: true,
       })
       |> Sexplib.Sexp.to_string;
-    ProjectorInit.init_or_noop_from_str(Fold, pieces, Exp(exp), str);
+    ProjectorHooks.init_or_noop_from_str(Fold, pieces, Exp(exp), str);
   | `Text =>
     let name =
       if (String.length(f_name) >= 2) {
@@ -1205,7 +1232,7 @@ let project_table_if = (should_project, pieces) =>
   if (should_project) {
     switch (MakeTerm.for_projection([pieces])) {
     | None => [pieces]
-    | Some(any) => ProjectorInit.init_or_noop(Table, [pieces], any)
+    | Some(any) => ProjectorHooks.init_or_noop(Table, [pieces], any)
     };
   } else {
     [pieces];

src/haz3lcore/projectors/ProjectorBase.re

@@ -108,6 +108,17 @@ type info = {
 /* A projector-reported error, e.g. "can't render as table" */
 type error = {message: string};
 
+/* A replacement for the projector's underlying syntax, returned by
+ * [init]. Projectors that transform their syntax at projection time
+ * should prefer [Term]: provide the desired term (e.g. list items
+ * wrapped in splices) and the framework prints it to a segment,
+ * exactly as SetTerm does for later edits. [Syntax] is the escape
+ * hatch for projectors that need piece-level control. */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type init_override =
+  | Term(Any.t)
+  | Syntax(Base.segment);
+
 module View = {
   /* A projector has an inline view, which replaces the underlying
    * syntax. Optionally, it may have an overlay view, which is shown
@@ -215,15 +226,16 @@ module type Projector = {
   /* Init should return None if the projector doesn't want
    * to handle the provided term. Otherwise, it should
    * return the desired initial state of the model, along with
-   * an optional replacement syntax. [init] receives the original
-   * [Base.segment] the user selected (in addition to the parsed
-   * term); when [Some(seg)] is returned as the second component,
-   * the projector's stored syntax is set to [seg] instead of the
-   * selected segment. This lets projectors transform their
-   * underlying syntax at init time (e.g. to wrap list items in
-   * splices). Return [None] for the second component to keep the
-   * selected syntax unchanged. */
-  let init: (Any.t, Base.segment) => option((model, option(Base.segment)));
+   * an optional replacement for the underlying syntax. [init]
+   * receives the original [Base.segment] the user selected (in
+   * addition to the parsed term). When the second component is
+   * [Some(Term(t))], the framework prints [t] and stores the result
+   * as the projector's syntax (the same path SetTerm uses); this is
+   * the preferred way to transform the underlying syntax at init
+   * time (e.g. to wrap list items in splices). [Some(Syntax(seg))]
+   * installs [seg] directly for projectors that need piece-level
+   * control. Return [None] to keep the selected syntax unchanged. */
+  let init: (Any.t, Base.segment) => option((model, option(init_override)));
   /* Does this projector have some notion of internal
    * positions, whose handling should override the editor
    * caret & keyboard handlers? If so, provide handlers

src/haz3lcore/projectors/ProjectorInit.re

@@ -17,20 +17,44 @@ let to_module = (kind: ProjectorCore.Kind.t): (module Cooked) =>
   | Card => (module Cook(CardProj.M))
   | Table => (module Cook(TableProj.M))
   | Csv => (module Cook(CSVProjector.M))
+  | VList => (module Cook(VListProj.M))
+  };
+
+/* Printer for Term init overrides, injected by ProjectorPerform at
+ * module initialization. Resolving a Term override requires
+ * ExpToSegment, but this module cannot depend on ExpToSegment: it is
+ * reachable from ExpToSegment via MakeTerm -> ... -> Refractors ->
+ * ProjectorInit. ProjectorPerform sits above both and registers the
+ * real printer (the same conversion SetTerm uses, reusing splices
+ * from the original syntax by id). If unregistered, Term overrides
+ * degrade to keeping the selected syntax. */
+let term_printer:
+  ref((~original_syntax: Base.segment, Language.Any.t) => Base.segment) =
+  ref((~original_syntax, _term) => original_syntax);
+
+/* Resolve an init-returned syntax override against the selected
+ * syntax: Term overrides are printed to a segment, Syntax overrides
+ * are installed directly, and None keeps the selection. */
+let resolve_override =
+    (syntax: syntax, override: option(init_override)): syntax =>
+  switch (override) {
+  | None => syntax
+  | Some(Syntax(seg)) => seg
+  | Some(Term(term)) => term_printer^(~original_syntax=syntax, term)
   };
 
 /* Construct a Projector piece wrapping the given syntax segment.
- * The projector's [init] may optionally return a replacement segment
- * (e.g. to wrap list items in splices); if so, the stored syntax is
- * set to that replacement instead of [syntax]. */
+ * The projector's [init] may optionally return a replacement for the
+ * underlying syntax (e.g. to wrap list items in splices); see
+ * ProjectorBase.init_override. */
 let init =
     (kind: ProjectorCore.Kind.t, syntax: syntax, any: Language.Any.t)
     : option(Base.piece) => {
   let (module P) = to_module(kind);
   switch (P.init(any, syntax)) {
   | None => None
   | Some((model, override)) =>
-    let syntax = Option.value(override, ~default=syntax);
+    let syntax = resolve_override(syntax, override);
     Some(Projector(ProjectorCore.mk(kind, syntax, model)));
   };
 };
@@ -57,7 +81,8 @@ let init_or_noop_from_str =
   switch (P.init(any, syntax)) {
   | None => syntax
   | Some((_, override)) =>
-    let syntax = Option.value(override, ~default=syntax);
+    let syntax = resolve_override(syntax, override);
     [Projector(ProjectorCore.mk(kind, syntax, model_str))];
   };
 };
+

src/haz3lcore/projectors/ProjectorPerform.re

@@ -49,7 +49,7 @@ let init =
     let* elab_exp =
       Language.Exp.find_by_id(Language.Exp.rep_id(exp), elaborated);
     let+ (model_str, override) = P.init(Exp(elab_exp), seg);
-    let syntax = Option.value(override, ~default=seg);
+    let syntax = ProjectorInit.resolve_override(seg, override);
     Base.Projector(ProjectorCore.mk(kind, syntax, model_str));
   | (None, _) => None
   };
@@ -115,6 +115,21 @@ let term_to_segment =
     term,
   );
 
+/* Wire up the cyclic-dependency injection points (see the comments at
+ * the registries for why they exist). This module sits above both
+ * ExpToSegment and ProjectorInit, so it can hand each the pieces of
+ * the other it needs. Runs as a module-initialization side effect at
+ * program startup. */
+ExpToSegment.ProjectorHooks.register({
+  init_or_noop: ProjectorInit.init_or_noop,
+  init_or_noop_from_str: ProjectorInit.init_or_noop_from_str,
+});
+ProjectorInit.term_printer :=
+  (
+    (~original_syntax, term) =>
+      term_to_segment(~original_syntax, ~preserve_splices=true, term)
+  );
+
 let update_piece =
     (f: Base.projector => Base.projector, id: Id.t, piece: Base.piece)
     : Base.segment =>

src/haz3lcore/projectors/implementations/FoldProj.re

@@ -30,7 +30,8 @@ module M: Projector = {
   type action =
     | Toggle;
 
-  let init = (_, _) => Some((default, None: option(Base.segment)));
+  let init = (_, _) =>
+    Some((default, None: option(ProjectorBase.init_override)));
 
   let focusable = Focusable.non;
   let dynamics = false;

src/haz3lcore/projectors/implementations/ProbeProj.re

@@ -1482,7 +1482,7 @@ module M: Projector = {
   type action = a;
 
   let init = (any: Any.t, _) => {
-    let none_seg: option(Base.segment) = None;
+    let none_seg: option(ProjectorBase.init_override) = None;
     switch (any) {
     | Exp(_)
     | Pat(_) => Some(({active_renderer: None}, none_seg))

src/haz3lcore/projectors/implementations/TypeProj.re

@@ -35,7 +35,7 @@ module M: Projector = {
     | ToggleDisplay;
 
   let init = (any: Any.t, _) => {
-    let none_seg: option(Base.segment) = None;
+    let none_seg: option(ProjectorBase.init_override) = None;
     switch (any) {
     | Exp(_)
     | Pat(_) => Some((Expected, none_seg))