Add dynamic mode to type projector

src/CLI/Print.re

@@ -10,6 +10,7 @@ let exp_to_segment_settings: ExpToSegment.Settings.t = {
   hide_fixpoints: false,
   show_filters: true,
   show_unknown_as_hole: true,
+  raise_if_padding: false,
 };
 
 let segmentize =

src/haz3lcore/pretty/ExpToSegment.re

@@ -43,6 +43,7 @@ module Settings = {
     hide_fixpoints: bool,
     show_filters: bool,
     show_unknown_as_hole: bool,
+    raise_if_padding: bool,
   };
 
   let of_core = (~inline, ~fold_fn_bodies=?, settings: CoreSettings.t) => {
@@ -59,6 +60,7 @@ module Settings = {
     hide_fixpoints: !settings.evaluation.show_fixpoints,
     show_filters: settings.evaluation.show_stepper_filters,
     show_unknown_as_hole: true,
+    raise_if_padding: false,
   };
 
   let editable = (~inline) => {
@@ -72,6 +74,7 @@ module Settings = {
       hide_fixpoints: false,
       show_filters: true,
       show_unknown_as_hole: true,
+      raise_if_padding: false,
     };
   };
 };
@@ -955,9 +958,12 @@ let mk_form =
 
 /* HACK[Matt]: Sometimes terms that should have multiple ids won't because
    evaluation only ever gives them one */
-let pad_ids = (n: int, ids: list(Id.t)): list(Id.t) => {
+let pad_ids = (~settings: Settings.t, n: int, ids: list(Id.t)): list(Id.t) => {
   let len = List.length(ids);
   if (len < n) {
+    if (settings.raise_if_padding) {
+      raise(Failure("Padding required but not enough ids provided."));
+    };
     ids @ List.init(n - len, _ => Id.mk());
   } else {
     ListUtil.split_n(n, ids) |> fst;
@@ -1049,6 +1055,7 @@ let fold_fun_if = (condition, f_name: string, pieces, exp) =>
       that the expression has no Closures or DynamicErrorHoles
    */
 let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
+  let pad_ids = pad_ids(~settings);
   let go = (~inline=settings.inline) =>
     exp_to_pretty(
       ~settings={
@@ -1588,6 +1595,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
 }
 and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
   let go = pat_to_pretty(~settings: Settings.t);
+  let pad_ids = pad_ids(~settings);
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
   /* Use settings-aware concatenation and form building */
   let (@) = concat_segment(~secondary=settings.secondary);
@@ -1750,6 +1758,7 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
 }
 and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
   let go = typ_to_pretty(~settings: Settings.t);
+  let pad_ids = pad_ids(~settings);
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
   /* Use settings-aware concatenation and form building */
   let (@) = concat_segment(~secondary=settings.secondary);
@@ -1985,6 +1994,7 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
 }
 and tpat_to_pretty = (~settings: Settings.t, tpat: TPat.t): pretty => {
   let wrap = wrap_with_secondary(~secondary=settings.secondary);
+  let pad_ids = pad_ids(~settings);
   /* Use settings-aware concatenation and form building */
   switch (tpat |> IdTagged.term_of) {
   | Invalid(t) =>

src/haz3lcore/pretty/PadIds.re

@@ -0,0 +1,38 @@
+open Language;
+
+/* Number of IDs required for ExpToSegment compatibility per type constructor */
+let necessary_ids: Typ.t => int =
+  ty => {
+    switch (ty.term) {
+    | Prod([]) => 1 /* Empty product (unit-like) */
+    | Prod(tys) => List.length(tys) - 1 /* One ID per separator */
+    | Sum(tys) => List.length(tys) + 1 /* Constructors + prefix */
+    | _ => 1 /* Default for other type constructors */
+    };
+  };
+
+/**
+ * Pads type IDs to ensure ExpToSegment uses them instead of creating new ones,
+ * preserving ID correspondence for styling. Test_PadIds property test that checks
+ *  ExpToSegment compatibility and padding equivalence.
+ */
+let pad_typ_ids = (ty: Typ.t): Typ.t => {
+  Typ.map_term(
+    ~f_typ=
+      (cont, ty) => {
+        let current_ids = ty.annotation.ids;
+        let needed_ids = necessary_ids(ty);
+        let ids =
+          current_ids
+          @ List.init(needed_ids - List.length(current_ids), _ => Id.mk());
+        cont({
+          ...ty,
+          annotation: {
+            ids,
+            secondary: ty.annotation.secondary,
+          },
+        });
+      },
+    ty,
+  );
+};

src/haz3lcore/projectors/ProjectorBase.re

@@ -120,6 +120,7 @@ module View = {
     (
       ~single_line: bool=?,
       ~background: bool=?,
+      ~is_dynamic: Id.t => bool=?,
       ~text_only: bool=?,
       Sort.t,
       list(syntax)

src/haz3lcore/projectors/ProjectorCore.re

@@ -63,25 +63,21 @@ module Kind = {
     | 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 */
+  module StringMap = Map.Make(String);
+  let name_to_kind: StringMap.t(t) =
+    List.fold_left(
+      (map, kind) => StringMap.add(name(kind), kind, map),
+      StringMap.empty,
+      all,
+    );
+
   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")
+    switch (StringMap.find_opt(p, name_to_kind)) {
+    | Some(k) => k
+    | None => failwith("Unknown projector kind")
     };
 
-  let is_name = str => List.mem(str, List.map(name, all));
+  let is_name = StringMap.mem(_, name_to_kind);
 };
 
 /* Projectors in syntax */

src/haz3lcore/projectors/ProjectorPerform.re

@@ -195,18 +195,14 @@ let go =
       if (ProjectorCore.Kind.is_refractor(kind)) {
         Zipper.update_manuals(
           map =>
-            ListUtil.assoc_update(
-              projector_idx_to_id(idx),
-              fun
-              | Some(entry: Refractors.entry) =>
-                Some(
-                  Refractors.{
-                    kind: entry.kind,
-                    model: new_model,
-                  },
-                )
-              | None => None,
-              map,
+            ListUtil.update_nth(idx, map, ((id, entry: Refractors.entry)) =>
+              (
+                id,
+                Refractors.{
+                  kind: entry.kind,
+                  model: new_model,
+                },
+              )
             ),
           z,
         );

src/haz3lcore/projectors/implementations/TypeProj.re

@@ -24,11 +24,44 @@ let totalize_ty = (expected_ty: option(Typ.t)): Typ.t =>
   | None => Typ.fresh(Unknown(Internal))
   };
 
+let get_dynamic_typ = (info: info): Typ.t => {
+  let dynamic_typ =
+    info.dynamics
+    |> Option.bind(
+         _,
+         (d: Dynamics.Info.t) => {
+           let statics =
+             Statics.mk(CoreSettings.on, Builtins.ctx_init(Some(Int)));
+           let type_of = (c: Sample.t) => {
+             IdTagged.rep_id(c.value)
+             |> Id.Map.find_opt(_, statics(c.value))
+             |> Option.bind(
+                  _,
+                  fun
+                  | InfoExp(e) => {
+                      Some(e.ty);
+                    }
+                  | _ => None,
+                );
+           };
+           let types = List.map(type_of, d.samples) |> Util.OptUtil.sequence;
+
+           Option.bind(
+             types,
+             Typ.meet_all(~empty=Typ.fresh(Unknown(Internal)), Ctx.empty),
+           );
+         },
+       )
+    |> Option.value(~default=Typ.fresh(Unknown(Internal)));
+  dynamic_typ;
+};
+
 module M: Projector = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model =
     | Expected
-    | Self;
+    | Self
+    | Dynamic;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type action =
@@ -37,54 +70,76 @@ module M: Projector = {
   let init = (any: Any.t): option(model) => {
     switch (any) {
     | Exp(_)
-    | Pat(_) => Some(Expected)
+    | Pat(_)
+    | Typ(_) => Some(Expected)
     | Any () => Some(Expected) /* Grout don't have sorts rn */
     | _ => None
     };
   };
 
-  let dynamics = false;
+  let dynamics = true;
   let focusable = Focusable.non;
 
-  let display_ty = (model, statics): option(Typ.t) =>
-    switch (model) {
-    | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn =>
-      statics |> self_ty
-    | Self => statics |> self_ty
-    | Expected => statics |> expected_ty
-    };
-
-  let display_mode = (model: model, statics: option(Language.Info.t)): string =>
+  let display_mode = (model: model, statics: option(Language.Info.t)): string => {
     switch (model) {
+    | Dynamic => "↦"
     | _ when self_ty(statics) == expected_ty(statics) => "⇔"
     | _ when expected_ty(statics) |> totalize_ty |> Typ.is_syn => "⇒"
     | Self => "⇒"
     | Expected => "⇐"
     };
-
+  };
   let mode_view = (model, info) =>
     div(
       ~attrs=[Attr.classes(["mode"])],
       [text(display_mode(model, info))],
     );
 
   let typ_view = (model, info: info, utility, view_seg: View.seg) => {
-    let typ = display_ty(model, info.statics) |> totalize_ty;
+    let (is_dynamic, typ) =
+      switch (model) {
+      | Dynamic =>
+        let dyn_typ =
+          get_dynamic_typ(info)
+          |> Grammar.map_typ_annotation(_ => IdTagged.IdTag.fresh())
+          |> PadIds.pad_typ_ids;
+        let self_ty =
+          Option.value(
+            ~default=Typ.fresh(Unknown(Internal)),
+            self_ty(info.statics),
+          );
+        let dynamic_ids: list(Id.t) = Typ.diff(self_ty, dyn_typ);
+        (List.mem(_, dynamic_ids), dyn_typ);
+      | Expected when expected_ty(info.statics) |> totalize_ty |> Typ.is_syn => (
+          (_ => false),
+          self_ty(info.statics) |> totalize_ty,
+        )
+      | Expected => ((_ => false), expected_ty(info.statics) |> totalize_ty)
+      | Self => ((_ => false), self_ty(info.statics) |> totalize_ty)
+      };
+
     div(
       ~attrs=[Attr.classes(["type-cell"])],
       [
         Typ(typ)
         |> utility.term_to_seg
-        |> view_seg(~single_line=true, Sort.Typ),
+        |> view_seg(~single_line=true, ~is_dynamic, Sort.Typ),
       ],
     );
   };
 
-  let update = (model, _, a: action) =>
+  let update = (model, info, a: action) => {
+    let has_expected =
+      switch (expected_ty(info.statics)) {
+      | Some(ty) => !Typ.is_syn(ty)
+      | None => false
+      };
     switch (a, model) {
-    | (ToggleDisplay, Expected) => Self
-    | (ToggleDisplay, Self) => Expected
+    | (ToggleDisplay, Expected) => if (has_expected) {Self} else {Dynamic}
+    | (ToggleDisplay, Self) => Dynamic
+    | (ToggleDisplay, Dynamic) => if (has_expected) {Expected} else {Self}
     };
+  };
 
   let placeholder = (_, _) => ProjectorCore.Shape.default;
 

src/haz3lcore/zipper/action/Introduce.re

@@ -249,6 +249,7 @@ module Make =
           hide_fixpoints: false,
           show_filters: true,
           show_unknown_as_hole: true,
+          raise_if_padding: false,
         },
         term,
         already_parenthesized(z),

src/language/statics/Elaborator.re

@@ -451,21 +451,13 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
         );
       Match(e', List.combine(ps', es')) |> rewrap;
     };
+
   (dhexp, elaborated_type);
 };
 
-//let dhexp_of_uexp = Core.Memo.general(~cache_size_bound=1000, dhexp_of_uexp);
-
-/* This function gives a new id to all the types
-   in the expression. It does this to get rid of
-   all the invalid ids we added to prevent generating
-   too many new ids */
-let fix_typ_ids =
-  Exp.map_term(~f_typ=(cont, e) => e |> IdTagged.new_ids |> cont);
-
 let uexp_elab = (m: Statics.Map.t, uexp: Exp.t): ElaborationResult.t => {
   switch (elaborate(m, uexp)) {
   | exception MissingTypeInfo => DoesNotElaborate
-  | (d, ty) => Elaborates(d |> fix_typ_ids, ty)
+  | (d, ty) => Elaborates(d, ty)
   };
 };

src/language/term/IdTagged.re

@@ -44,6 +44,8 @@ module IdTag = {
     ids,
     secondary,
   };
+
+  let rep_id = ({ids, _}: t) => List.hd(ids);
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]