Merge remote-tracking branch 'origin/dynamic_statics' into tables-all-revamp

Author: 7h3kk1d

src/CLI/Print.re

@@ -11,6 +11,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/derived/CachedStatics.re

@@ -7,7 +7,9 @@ type t = {
   elaborated: Exp.t,
   info_map: Statics.Map.t,
   error_ids: list(Id.t),
-  targets: Sample.targets /* Maps expr/pat IDs to capture specs for sampling */
+  targets: Sample.targets, /* Maps expr/pat IDs to capture specs for sampling */
+  dynamic_info_map: Statics.Map.t,
+  dynamic_error_ids: list(Id.t),
 };
 
 let empty: t = {
@@ -22,6 +24,8 @@ let empty: t = {
   info_map: Id.Map.empty,
   error_ids: [],
   targets: Sample.no_targets,
+  dynamic_info_map: Id.Map.empty,
+  dynamic_error_ids: [],
 };
 
 let elaborate =
@@ -46,19 +50,59 @@ let all_probeable_ids = (info_map: Statics.Map.t): Id.Map.t(unit) =>
     Id.Map.empty,
   );
 
+/* Collect IDs of expressions/patterns with partially unknown types.
+ * Used for live_typing to automatically probe terms that need dynamic type feedback.
+ * Note: We check the SELF (synthesized) type, not the fixed TY, because
+ * an expression like `1 : ?` analyzed against String would have ty=String
+ * but self=Unknown - we need dynamic feedback for the Unknown part. */
+let ids_with_unknown_types = (info_map: Statics.Map.t): Id.Map.t(unit) =>
+  Id.Map.fold(
+    (id, info, acc) =>
+      switch (info) {
+      | Info.InfoExp({self: Common(Just(ty)), _})
+          when Typ.contains_unknown(ty) =>
+        Id.Map.add(id, (), acc)
+      | Info.InfoPat({self: Common(Just(ty)), _})
+          when Typ.contains_unknown(ty) =>
+        Id.Map.add(id, (), acc)
+      | _ => acc
+      },
+    info_map,
+    Id.Map.empty,
+  );
+
 /* Compute targets from probe_ids. For each ID, determine whether it's
  * an expression or pattern target, then look up the appropriate refs to capture.
  * When probe_all is enabled, we target everything in info_map that passes
- * should_probe, ignoring the passed probe_ids (which are a subset anyway). */
+ * should_probe, ignoring the passed probe_ids (which are a subset anyway).
+ * When live_typing is enabled, we also include expressions with unknown types. */
 let compute_targets =
     (
       ~settings: CoreSettings.t,
       ~info_map: Statics.Map.t,
       ~probe_ids: Id.Map.t(unit),
     )
     : Sample.targets => {
+  /* Start with explicit probe IDs */
+  let base_ids = probe_ids;
+  /* If probe_all is enabled, include all probeable expressions */
+  let base_ids =
+    settings.probe_all
+      ? Id.Map.union(
+          (_, _, _) => Some(),
+          base_ids,
+          all_probeable_ids(info_map),
+        )
+      : base_ids;
+  /* If live_typing is enabled, include expressions with unknown types */
   let effective_probe_ids =
-    settings.probe_all ? all_probeable_ids(info_map) : probe_ids;
+    settings.live_typing
+      ? Id.Map.union(
+          (_, _, _) => Some(),
+          base_ids,
+          ids_with_unknown_types(info_map),
+        )
+      : base_ids;
   Id.Map.fold(
     (id, (), acc) => {
       let refs =
@@ -110,6 +154,8 @@ let init_from_term =
     info_map,
     error_ids,
     targets,
+    dynamic_info_map: Statics.Map.empty,
+    dynamic_error_ids: [],
   };
 };
 

src/haz3lcore/pretty/ExpToSegment.re

@@ -44,6 +44,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) => {
@@ -61,6 +62,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) => {
@@ -75,6 +77,7 @@ module Settings = {
       hide_fixpoints: false,
       show_filters: true,
       show_unknown_as_hole: true,
+      raise_if_padding: false,
     };
   };
 };
@@ -969,9 +972,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;
@@ -1072,6 +1078,7 @@ let project_table_if = (should_project, pieces) =>
       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={
@@ -1624,6 +1631,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);
@@ -1794,6 +1802,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);
@@ -2037,6 +2046,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

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

src/haz3lcore/projectors/implementations/ProbeProj.re

@@ -245,6 +245,23 @@ module SampleLength = {
   let set = (id: int, length: int): unit => Hashtbl.add(lengths, id, length);
 };
 
+/* Remove opaque values like function literals */
+let rm_opaques: list(Sample.Env.entry) => list(Sample.Env.entry) =
+  List.filter_map((en: Sample.Env.entry) =>
+    switch (en.value) {
+    | Opaque => None
+    | Val(_) => Some(en)
+    }
+  );
+
+let cur_ap = (info: info) =>
+  switch (info.statics) {
+  | Some(InfoExp({term: {term: Ap(_), _} as ap, _}))
+  | Some(InfoExp({term: {term: TypAp(_), _} as ap, _})) =>
+    Some(Exp.rep_id(ap))
+  | _ => None
+  };
+
 /* Select samples to display, using stateful window offset.
  * This wraps Sample.Selection with WindowState for offset persistence.
  * Optionally takes pre-filtered samples to avoid redundant filtering. */

src/haz3lcore/projectors/implementations/TableRenderer.re

@@ -243,8 +243,6 @@ let convert_column =
               ),
             ]),
           ),
-          None,
-          None,
         ),
       )
     )
@@ -269,8 +267,6 @@ let rename_column =
               tup_label(label(new_name), dot(var("r"), label(old_name))),
             ]),
           ),
-          None,
-          None,
         )
       )
     ),
@@ -289,8 +285,6 @@ let add_column_after =
             var("r"),
             tuple([tup_label(label(new_column), empty_hole())]),
           ),
-          None,
-          None,
         ),
       )
     )
@@ -307,12 +301,7 @@ let group_by_column = (info: info, column: string): Base.segment => {
           var("group_on_key"),
           tuple([
             deferral(InAp),
-            fn(
-              Pat.var("row"),
-              dot(var("row"), label(column)),
-              None,
-              None,
-            ),
+            fn(Pat.var("row"), dot(var("row"), label(column))),
           ]),
         )
       ),
@@ -333,8 +322,6 @@ let filter_by_column = (op, info: info, column: string): Base.segment => {
             fn(
               Pat.var("row"),
               bin_op(op, dot(var("row"), label(column)), empty_hole()),
-              None,
-              None,
             ),
           ]),
         )
@@ -532,8 +519,6 @@ let sort_column_with_direction =
                               dot(var("r2"), label(header)),
                             ]),
                           ),
-                          None,
-                          None,
                         ),
                         deferral(InAp),
                       ]),