Merge branch 'dev' into patchwork

Author: disconcision

src/haz3lcore/lang/MakeTerm.re

@@ -886,11 +886,37 @@ and unsorted = (sort: Sort.t, skel: Skel.t, seg: Segment.t): unsorted => {
     switch (p) {
     | Secondary(_)
     | Grout(_) => []
-    | Projector({syntax, _} as pr) =>
+    | Projector({id, kind, model, syntax} as pr) =>
       let _ = log_projector(pr);
       let sort = Piece.sort(syntax) |> fst;
       let seg = Piece.unparenthesize(syntax);
-      [go_s(sort, Segment.skel(seg), seg)];
+      let inner = go_s(sort, Segment.skel(seg), seg);
+      /* Construct Projector term with proper annotation, preserving
+       * projector metadata (kind, model) in the term for round-tripping */
+      let projector_data: Grammar.projector_data = {
+        kind,
+        model,
+      };
+      let wrapped =
+        switch (inner) {
+        | Grammar.Exp(e) =>
+          Grammar.Exp({
+            term: Projector(projector_data, e),
+            annotation: IdTagged.IdTag.mk([id], get_secondary([id])),
+          })
+        | Grammar.Pat(p) =>
+          Grammar.Pat({
+            term: Projector(projector_data, p),
+            annotation: IdTagged.IdTag.mk([id], get_secondary([id])),
+          })
+        | Grammar.Typ(t) =>
+          Grammar.Typ({
+            term: Projector(projector_data, t),
+            annotation: IdTagged.IdTag.mk([id], get_secondary([id])),
+          })
+        | _ => inner
+        };
+      [wrapped];
     | Tile({mold, shards, children, _}) =>
       Aba.aba_triples(Aba.mk(shards, children))
       |> List.map(((l, kid, r)) => {

src/haz3lcore/pretty/ExpToSegment.re

@@ -120,6 +120,7 @@ let rec external_precedence = (exp: Exp.t): Precedence.t => {
 
   // Same goes for forms which are already surrounded
   | Parens(_)
+  | Projector(_)
   | ListLit(_)
   | Test(_)
   | HintedTest(_)
@@ -175,7 +176,8 @@ let external_precedence_pat = (dp: Pat.t) =>
 
   // Same goes for forms which are already surrounded
   | ListLit(_)
-  | Parens(_) => Precedence.max
+  | Parens(_)
+  | Projector(_) => Precedence.max
 
   // Other forms
   | Cons(_) => Precedence.cons
@@ -203,6 +205,7 @@ let external_precedence_typ = (tp: Typ.t) =>
   | ProdExtension(_) => Precedence.ap
   // Same goes for forms which are already surrounded
   | Parens(_)
+  | Projector(_)
   | ProofOf(_)
   | List(_) => Precedence.max
 
@@ -508,6 +511,8 @@ let rec parenthesize =
   | Parens(e) =>
     Parens(parenthesize(~already_paren=true, e) |> paren_at(Precedence.min))
     |> rewrap
+  | Projector(data, e) =>
+    Projector(data, parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
   | Cons(e1, e2) =>
     Cons(
       parenthesize(e1) |> paren_at(Precedence.cons),
@@ -598,6 +603,9 @@ and parenthesize_pat =
       |> paren_pat_at(Precedence.min),
     )
     |> rewrap
+  | Projector(data, p) =>
+    Projector(data, parenthesize_pat(p) |> paren_pat_at(Precedence.min))
+    |> rewrap
   | Cons(p1, p2) =>
     Cons(
       parenthesize_pat(p1) |> paren_pat_at(Precedence.cons),
@@ -675,6 +683,9 @@ and parenthesize_typ =
       |> paren_typ_at(Precedence.min),
     )
     |> rewrap
+  | Projector(data, t) =>
+    Projector(data, parenthesize_typ(t) |> paren_typ_at(Precedence.min))
+    |> rewrap
   | List(t) =>
     List(parenthesize_typ(t) |> paren_typ_at(Precedence.min)) |> rewrap
   | Prod([]) => typ
@@ -1508,6 +1519,14 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let id = exp |> Exp.rep_id;
     let+ e = go(e);
     wrap(exp, [mk_form(ParensExp, id, [e])]);
+  | Projector({kind, model}, e) =>
+    let id = exp |> Exp.rep_id;
+    let+ inner_seg = go(e);
+    let syntax = Segment.parenthesize(inner_seg);
+    wrap(
+      exp,
+      [Piece.Projector(ProjectorCore.mk(~id, kind, syntax, model))],
+    );
   | Cons(e1, e2) =>
     // TODO: Add optional newlines
     let id = exp |> Exp.rep_id;
@@ -1710,6 +1729,14 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
     let id = pat |> Pat.rep_id;
     let+ p = go(p);
     wrap(pat, [mk_form(ParensPat, id, [p])]);
+  | Projector({kind, model}, p) =>
+    let id = pat |> Pat.rep_id;
+    let+ inner_seg = go(p);
+    let syntax = Segment.parenthesize(inner_seg);
+    wrap(
+      pat,
+      [Piece.Projector(ProjectorCore.mk(~id, kind, syntax, model))],
+    );
   | MultiHole(es) =>
     let+ es = es |> List.map(any_to_pretty(~settings: Settings.t)) |> all;
     /* Use IDs from the term for grout pieces, like Tuple uses for commas. */
@@ -1943,6 +1970,14 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
     let id = typ |> Typ.rep_id;
     let+ t = go(t);
     wrap(typ, [mk_form(ParensTyp, id, [t])]);
+  | Projector({kind, model}, t) =>
+    let id = typ |> Typ.rep_id;
+    let+ inner_seg = go(t);
+    let syntax = Segment.parenthesize(inner_seg);
+    wrap(
+      typ,
+      [Piece.Projector(ProjectorCore.mk(~id, kind, syntax, model))],
+    );
   | Rec(tp, t) =>
     let id = typ |> Typ.rep_id;
     let+ tp = tpat_to_pretty(~settings: Settings.t, tp)

src/haz3lcore/projectors/ProjectorCore.re

@@ -12,77 +12,9 @@ open Util;
  * ProjectorInfo depends on ProjectorBase but not on ProjectorInit
  * (to avoid cyclical dependencies due to MakeTerm and ExpToSegment) */
 
-module Kind = {
-  /* The different kinds of projector. New projector
-   * types need to be registered here in order to be
-   * able to create and update their instances */
-  [@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
-  type t =
-    | Fold
-    | Probe
-    | Statics
-    | Checkbox
-    | Slider
-    | SliderF
-    | Card
-    | Livelit
-    | TextArea
-    | Csv;
-
-  let livelit_projectors: list(t) = [
-    Checkbox,
-    Slider,
-    SliderF,
-    TextArea,
-    Csv, /* Competes with Card for empty list */
-    Card, /* Competes with Csv for empty list */
-    Livelit,
-  ];
-
-  /* Note: Probe intentionally excluded - probes use separate action path */
-  let projectors: list(t) = livelit_projectors @ [Fold];
-
-  /* Refractors are like probes - additive decorations, not syntax-replacing */
-  let refractors: list(t) = [Probe, Statics];
-  let is_refractor = (kind: t) => List.mem(kind, refractors);
-
-  /* A friendly name for each projector. This is used
-   * both for identifying a projector in the CSS and for
-   * selecting projectors in the projector panel menu */
-  let name = (p: t): string =>
-    switch (p) {
-    | Fold => "fold"
-    | Probe => "probe"
-    | Statics => "statics"
-    | Checkbox => "check"
-    | Slider => "slider"
-    | SliderF => "sliderf"
-    | Card => "card"
-    | Livelit => "livelit"
-    | TextArea => "text"
-    | Csv => "csv"
-    };
-
-  /* This must be updated and kept 1-to-1 with the above
-   * name function in order to be able to select the
-   * projector in the projector panel menu */
-  let of_name = (p: string): t =>
-    switch (p) {
-    | "fold" => Fold
-    | "probe" => Probe
-    | "statics" => Statics
-    | "check" => Checkbox
-    | "slider" => Slider
-    | "sliderf" => SliderF
-    | "text" => TextArea
-    | "livelit" => Livelit
-    | "card" => Card
-    | "csv" => Csv
-    | _ => failwith("Unknown projector kind")
-    };
-
-  let is_name = str => List.mem(str, List.map(name, all));
-};
+/* Kind is now defined in src/language/ProjectorKind.re to allow
+ * sharing with Grammar.re (which is in the language library) */
+module Kind = Language.ProjectorKind;
 
 /* Projectors in syntax */
 [@deriving (show({with_path: false}), sexp, yojson, eq)]

src/haz3lcore/tiles/Segment.re

@@ -836,11 +836,59 @@ module SecondaryCollection = {
     | _ => None
     };
 
-  /* Recursively collect secondary from a segment (for compound tile children) */
-  let rec collect_from_seg = (child_seg: t, acc: secondary_map): secondary_map =>
+  /* Collect secondary from a segment by directly walking through pieces.
+     This handles segments with embedded Secondary pieces (like projector children)
+     where skel() would throw Input_contains_secondary. */
+  let rec collect_from_seg_direct =
+          (seg: t, acc: secondary_map): secondary_map => {
+    /* Find all non-secondary pieces and collect their before/after secondary */
+    let rec find_pieces = (idx, pieces_acc) =>
+      if (idx >= List.length(seg)) {
+        List.rev(pieces_acc);
+      } else {
+        switch (List.nth(seg, idx)) {
+        | Piece.Secondary(_) => find_pieces(idx + 1, pieces_acc)
+        | _ =>
+          find_pieces(idx + 1, [(idx, List.nth(seg, idx)), ...pieces_acc])
+        };
+      };
+
+    let pieces = find_pieces(0, []);
+    List.fold_left(
+      (acc, (idx, piece)) => {
+        let before = collect_before(seg, idx);
+        let after = collect_after(seg, idx);
+        switch (piece) {
+        | Piece.Tile({id, children, _}) =>
+          /* Add secondary for this tile and recurse into children */
+          let acc = Id.Map.add(id, (before, after), acc);
+          List.fold_left(
+            (acc, child_seg) => collect_from_seg(child_seg, acc),
+            acc,
+            children,
+          );
+        | Piece.Projector({id, syntax, _}) =>
+          /* Add secondary for projector and recurse into its content */
+          let acc = Id.Map.add(id, (before, after), acc);
+          let inner_seg = Piece.unparenthesize(syntax);
+          collect_from_seg(inner_seg, acc);
+        | Piece.Grout({id, _}) => Id.Map.add(id, (before, after), acc)
+        | _ => acc
+        };
+      },
+      acc,
+      pieces,
+    );
+  }
+
+  /* Recursively collect secondary from a segment (for compound tile children).
+     Falls back to direct collection when the segment contains Secondary pieces. */
+  and collect_from_seg = (child_seg: t, acc: secondary_map): secondary_map =>
     try(collect_from_skel(child_seg, skel(child_seg), acc)) {
-    | Skel.Nonconvex_segment
-    | Skel.Input_contains_secondary => acc
+    | Skel.Nonconvex_segment => acc
+    | Skel.Input_contains_secondary =>
+      /* Segment has embedded Secondary pieces, use direct collection */
+      collect_from_seg_direct(child_seg, acc)
     }
   /* Recursively collect secondary for all terms in the skeleton.
 
@@ -900,6 +948,11 @@ module SecondaryCollection = {
               acc,
               children,
             )
+          | Some(Piece.Projector({syntax, _})) =>
+            /* Projectors wrap their content in parentheses. Extract the inner
+               segment and recursively collect secondary from it. */
+            let inner_seg = Piece.unparenthesize(syntax);
+            collect_from_seg(inner_seg, acc);
           | _ => acc
           },
         acc,

src/haz3lcore/zipper/action/Triggers.re

@@ -55,9 +55,6 @@ let expand_projector = (z: t): option(t) => {
       ...rest,
     ]
       when Token.is_projector_invoke(name) =>
-    /* Trim only need because of grout/whitespace transmutation when syntax is hole */
-    let syntax =
-      syntax |> Segment.trim_secondary(Right) |> Segment.trim_secondary(Left);
     let+ piece = invoked_projector(name, syntax);
     Zipper.update_siblings(
       ((_, r)) => ([piece, ...rest] |> List.rev, r),

src/language/ProjectorKind.re

@@ -0,0 +1,74 @@
+/* Projector kinds shared between Grammar.re and ProjectorCore.re.
+ * This module exists to break the dependency cycle between
+ * the language and haz3lcore libraries. */
+
+/* The different kinds of projector. New projector
+ * types need to be registered here in order to be
+ * able to create and update their instances */
+[@deriving (show({with_path: false}), sexp, yojson, eq, enumerate)]
+type t =
+  | Fold
+  | Probe
+  | Statics
+  | Checkbox
+  | Slider
+  | SliderF
+  | Card
+  | Livelit
+  | TextArea
+  | Csv;
+
+let livelit_projectors: list(t) = [
+  Csv, /* Competes with Card for empty list */
+  Card, /* Competes with Csv for empty list */
+  Checkbox,
+  Slider,
+  SliderF,
+  TextArea,
+  Card,
+  Livelit,
+];
+
+/* Note: Probe intentionally excluded - probes use separate action path */
+let projectors: list(t) = livelit_projectors @ [Fold];
+
+/* Refractors are like probes - additive decorations, not syntax-replacing */
+let refractors: list(t) = [Probe, Statics];
+let is_refractor = (kind: t) => List.mem(kind, refractors);
+
+/* A friendly name for each projector. This is used
+ * both for identifying a projector in the CSS and for
+ * selecting projectors in the projector panel menu */
+let name = (p: t): string =>
+  switch (p) {
+  | Fold => "fold"
+  | Probe => "probe"
+  | Statics => "statics"
+  | Checkbox => "check"
+  | Slider => "slider"
+  | SliderF => "sliderf"
+  | Card => "card"
+  | Livelit => "livelit"
+  | TextArea => "text"
+  | Csv => "csv"
+  };
+
+/* This must be updated and kept 1-to-1 with the above
+ * name function in order to be able to select the
+ * projector in the projector panel menu */
+let of_name = (p: string): t =>
+  switch (p) {
+  | "fold" => Fold
+  | "probe" => Probe
+  | "statics" => Statics
+  | "check" => Checkbox
+  | "slider" => Slider
+  | "sliderf" => SliderF
+  | "text" => TextArea
+  | "livelit" => Livelit
+  | "card" => Card
+  | "csv" => Csv
+  | _ => failwith("Unknown projector kind")
+  };
+
+let is_name = str => List.mem(str, List.map(name, all));