Add dynamic mode to type projector

src/haz3lcore/pretty/ExpToSegment.re

@@ -132,6 +132,7 @@ let external_precedence_typ = (tp: Typ.t) =>
   | Unknown(Internal)
   | Unknown(SynSwitch)
   | Unknown(Hole(EmptyHole))
+  | Unknown(Inconsistent)
   | Var(_)
   | Atom(_)
   | Label(_)
@@ -467,6 +468,7 @@ and parenthesize_typ =
   | Var(_)
   | Unknown(Hole(Invalid(_)))
   | Unknown(Internal)
+  | Unknown(Inconsistent)
   | Unknown(SynSwitch)
   | Unknown(Hole(EmptyHole))
   | Atom(_) => typ
@@ -1239,6 +1241,7 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
   | Unknown(Hole(Invalid(s))) =>
     text_to_pretty(typ |> Typ.rep_id, Sort.Typ, s)
   | Unknown(Internal)
+  | Unknown(Inconsistent)
   | Unknown(SynSwitch)
   | Unknown(Hole(EmptyHole)) =>
     if (settings.show_unknown_as_hole) {

src/haz3lcore/projectors/ProjectorCore.re

@@ -20,6 +20,7 @@ module Kind = {
   type t =
     | Fold
     | Info
+    | DynType
     | Probe
     | Checkbox
     | Slider
@@ -37,7 +38,8 @@ module Kind = {
     Livelit,
   ];
 
-  let projectors: list(t) = livelit_projectors @ [Fold, Info, Probe];
+  let projectors: list(t) =
+    livelit_projectors @ [Fold, Info, DynType, Probe];
 
   /* A friendly name for each projector. This is used
    * both for identifying a projector in the CSS and for
@@ -46,6 +48,7 @@ module Kind = {
     switch (p) {
     | Fold => "fold"
     | Info => "type"
+    | DynType => "dyntype"
     | Probe => "probe"
     | Checkbox => "check"
     | Slider => "slider"
@@ -59,9 +62,11 @@ module Kind = {
    * name function in order to be able to select the
    * projector in the projector panel menu */
   let of_name = (p: string): t =>
+    // TODO Use a map built from above
     switch (p) {
     | "fold" => Fold
     | "type" => Info
+    | "dyntype" => DynType
     | "probe" => Probe
     | "check" => Checkbox
     | "slider" => Slider

src/haz3lcore/projectors/ProjectorInit.re

@@ -8,6 +8,7 @@ let to_module = (kind: ProjectorCore.Kind.t): (module Cooked) =>
   switch (kind) {
   | Fold => (module Cook(FoldProj.M))
   | Info => (module Cook(TypeProj.M))
+  | DynType => (module Cook(DynTypeProj.M))
   | Probe => (module Cook(ProbeProj.M))
   | Slider => (module Cook(SliderProj.M))
   | SliderF => (module Cook(SliderFProj.M))

src/haz3lcore/projectors/implementations/DynTypeProj.re

@@ -0,0 +1,114 @@
+open Virtual_dom.Vdom;
+open Node;
+open ProjectorBase;
+open Language;
+
+let self_ty = (info: option(Info.t)): option(Typ.t) =>
+  switch (info) {
+  | Some(InfoExp({self, _})) => Self.typ_of_exp(self)
+  | Some(InfoPat({self, _})) => Self.typ_of_pat(self)
+  | _ => None
+  };
+module M: Projector = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type model =
+    | Expected
+    | Self;
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type action =
+    | ToggleDisplay;
+
+  let init = (any: Term.Any.t): option(model) => {
+    switch (any) {
+    | Exp(_)
+    | Pat(_) => Some(Expected)
+    | Any () => Some(Expected) /* Grout don't have sorts rn */
+    | _ => None
+    };
+  };
+
+  let dynamics = true;
+  let focusable = Focusable.non;
+
+  let typ_view = (info: info, utility, view_seg: View.seg) => {
+    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: Dynamics.Probe.Closure.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) |> Util.OptUtil.sequence;
+
+             Option.map(Typ.consistent_join(Ctx.empty), types);
+           },
+         )
+      |> Option.value(~default=Typ.fresh(Unknown(Internal)));
+    div(
+      ~attrs=[Attr.classes(["dyntype-cell"])],
+      [Typ(dynamic_typ) |> utility.term_to_seg |> view_seg(Sort.Typ)],
+    );
+  };
+
+  let update = (model, _, a: action) =>
+    switch (a, model) {
+    | (ToggleDisplay, Expected) => Self
+    | (ToggleDisplay, Self) => Expected
+    };
+
+  let syntax_str = (info: info) => {
+    let max_len = 30;
+    let seg = Segment.unparenthesize(info.syntax);
+    let str = info.utility.seg_to_string(seg);
+    let str = Re.Str.global_replace(Re.Str.regexp("\n"), " ", str);
+    String.length(str) > max_len
+      ? String.sub(str, 0, max_len) ++ "..." : str;
+  };
+
+  let placeholder = (_m, info) =>
+    ProjectorCore.Shape.inline(3 + String.length(syntax_str(info)));
+
+  let syntax_view = (info: info) => info |> syntax_str |> text;
+
+  let icon = div(~attrs=[Attr.classes(["icon"])], []);
+
+  let view =
+      (
+        _: model,
+        info: info,
+        ~local: action => Ui_effect.t(unit),
+        ~parent as _,
+        ~view_seg,
+      ) =>
+    View.{
+      inline:
+        div(
+          ~attrs=[
+            Attr.classes(["main"]),
+            Attr.on_double_click(_ => local(ToggleDisplay)),
+          ],
+          [syntax_view(info), icon],
+        ),
+      offside:
+        Some(
+          div(
+            ~attrs=[Attr.classes(["offside"])],
+            [typ_view(info, info.utility, view_seg)],
+          ),
+        ),
+      overlay: None,
+    };
+};

src/language/term/Grammar.re

@@ -154,6 +154,7 @@ and type_provenance('a) =
   | SynSwitch
   | Hole(type_hole('a))
   | Internal
+  | Inconsistent
 and filter('a) = {
   pat: exp_t('a),
   act: FilterAction.t,
@@ -416,6 +417,7 @@ and map_type_provenance_annotation:
     | SynSwitch => SynSwitch
     | Hole(h) => Hole(map_type_hole_annotation(f, h))
     | Internal => Internal
+    | Inconsistent => Inconsistent
     };
   }
 and map_type_hole_annotation:

src/language/term/TermBase.re

@@ -590,6 +590,7 @@ and Typ: {
         | Unknown(Hole(Invalid(_)))
         | Unknown(SynSwitch)
         | Unknown(Internal)
+        | Unknown(Inconsistent)
         | Atom(_)
         | Label(_)
         | Var(_) => term

src/language/term/Typ.re

@@ -9,6 +9,7 @@ type cls =
   | MultiHole
   | SynSwitch
   | Internal
+  | Inconsistent
   | Arrow
   | Prod
   | TupLabel
@@ -81,6 +82,7 @@ let cls_of_term: Grammar.typ_term('a) => cls =
   | Unknown(Hole(MultiHole(_))) => MultiHole
   | Unknown(SynSwitch) => SynSwitch
   | Unknown(Internal) => Internal
+  | Unknown(Inconsistent) => Inconsistent
   | Atom(c) => Atom(c)
   | List(_) => List
   | Arrow(_) => Arrow
@@ -99,6 +101,7 @@ let show_cls: cls => string =
   | Invalid => "Invalid type"
   | MultiHole => "Broken type"
   | EmptyHole => "Type hole"
+  | Inconsistent => "Join of Inconsistent types"
   | SynSwitch => "Synthetic type"
   | Internal => "Internal type"
   | Atom(_) => "Base type"
@@ -224,6 +227,8 @@ let join_type_provenance =
   | (Internal, SynSwitch) => SynSwitch
   | (Internal | Hole(_), _)
   | (_, Hole(_)) => Internal
+  | (Inconsistent, _)
+  | (_, Inconsistent) => Inconsistent
   | (SynSwitch, SynSwitch) => SynSwitch
   };
 
@@ -430,13 +435,23 @@ let equal = (t1: t, t2: t): bool => fast_equal(t1, t2);
    resolve parameter specifies whether, in the case of a type
    variable and a succesful join, to return the resolved join type,
    or to return the (first) type variable for readability */
-let rec join = (~resolve=false, ctx: Ctx.t, ty1: t, ty2: t): option(t) => {
-  let join' = join(~resolve, ctx);
+let rec join =
+        (
+          ~inconsistent: option(t)=?,
+          ~resolve=false,
+          ctx: Ctx.t,
+          ty1: t,
+          ty2: t,
+        )
+        : option(t) => {
+  let join' = join(~inconsistent?, ~resolve, ctx);
   switch (term_of(ty1), term_of(ty2)) {
   | (_, Parens(ty2)) => join'(ty1, ty2)
   | (Parens(ty1), _) => join'(ty1, ty2)
   | (Unknown(p1), Unknown(p2)) =>
     Some(Unknown(join_type_provenance(p1, p2)) |> temp)
+  | (Unknown(Inconsistent), _) => Some(ty1)
+  | (_, Unknown(Inconsistent)) => Some(ty2)
   | (Unknown(_), _) => Some(ty2)
   | (_, Unknown(_)) => Some(ty1)
   | (Var(n1), Var(n2)) =>
@@ -466,7 +481,7 @@ let rec join = (~resolve=false, ctx: Ctx.t, ty1: t, ty2: t): option(t) => {
       };
     let+ ty_body = join(~resolve, ctx, ty1', ty2);
     Rec(tp1, ty_body) |> temp;
-  | (Rec(_), _) => None
+  | (Rec(_), _) => inconsistent
   | (Forall(x1, ty1), Forall(x2, ty2)) =>
     let ty1' =
       switch (TPat.tyvar_of_utpat(x2)) {
@@ -482,25 +497,25 @@ let rec join = (~resolve=false, ctx: Ctx.t, ty1: t, ty2: t): option(t) => {
      be exposed to the user. We preserve the variable name of the
      second type to preserve synthesized type variable names, which
      come from user annotations. */
-  | (Forall(_), _) => None
+  | (Forall(_), _) => inconsistent
   | (Atom(c1), Atom(c2)) when c1 == c2 => Some(ty1)
-  | (Atom(_), _) => None
+  | (Atom(_), _) => inconsistent
   | (Label(_), Label("")) => Some(ty1)
   | (Label(""), Label(_)) => Some(ty2)
   | (Label(name1), Label(name2))
       when LabeledTuple.match_labels(name1, name2) =>
     Some(ty1)
-  | (Label(_), _) => None
+  | (Label(_), _) => inconsistent
   | (Arrow(ty1, ty2), Arrow(ty1', ty2')) =>
     let* ty1 = join'(ty1, ty1');
     let+ ty2 = join'(ty2, ty2');
     Arrow(ty1, ty2) |> temp;
-  | (Arrow(_), _) => None
+  | (Arrow(_), _) => inconsistent
   | (TupLabel(lab1, ty1'), TupLabel(lab2, ty2')) =>
     let* lab = join'(lab1, lab2);
     let+ ty = join'(ty1', ty2');
     TupLabel(lab, ty) |> temp;
-  | (TupLabel(_), _) => None
+  | (TupLabel(_), _) => inconsistent
   | (Prod(tys1), Prod(tys2)) =>
     if (List.length(tys1) != List.length(tys2)) {
       None;
@@ -509,15 +524,15 @@ let rec join = (~resolve=false, ctx: Ctx.t, ty1: t, ty2: t): option(t) => {
       let+ tys = OptUtil.sequence(tys);
       Prod(tys) |> temp;
     }
-  | (Prod(_), _) => None
+  | (Prod(_), _) => inconsistent
   | (Sum(sm1), Sum(sm2)) =>
     let+ sm' = ConstructorMap.join(equal, join(~resolve, ctx), sm1, sm2);
     Sum(sm') |> temp;
-  | (Sum(_), _) => None
+  | (Sum(_), _) => inconsistent
   | (List(ty1), List(ty2)) =>
     let+ ty = join'(ty1, ty2);
     List(ty) |> temp;
-  | (List(_), _) => None
+  | (List(_), _) => inconsistent
   | (Ap(_), _) => failwith("Type join of ap")
   };
 };
@@ -561,16 +576,34 @@ let rec match_synswitch = (t1: t, t2: t) => {
   };
 };
 
-let join_all = (~empty: t, ctx: Ctx.t, ts: list(t)): option(t) =>
+let join_all =
+    (~inconsistent=?, ~empty: t, ctx: Ctx.t, ts: list(t)): option(t) =>
   List.fold_left(
-    (acc, ty) => OptUtil.and_then(join(ctx, ty), acc),
+    (acc, ty) => OptUtil.and_then(join(~inconsistent?, ctx, ty), acc),
     Some(empty),
     ts,
   );
 
 let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool =>
   join(ctx, ty1, ty2) != None;
 
+/*
+    Computes the most precise type that is consistent with all input types.
+    Like a multi-way join, but if any ground types are inconsistent, replaces
+    that position with an "unknown" type rather than failing.
+    This operation is NOT associative — applying it pairwise may yield
+    a different result than applying it to the whole list at once.
+ */
+let consistent_join = (ctx: Ctx.t, tys: list(t)): t => {
+  join_all(
+    ~inconsistent=Unknown(Inconsistent) |> temp,
+    ~empty=Unknown(SynSwitch) |> temp,
+    ctx,
+    tys,
+  )
+  |> Option.value(~default=Unknown(SynSwitch) |> temp);
+};
+
 /**
    * Determines if one type (`ty1`) is more precise than another type (`ty2`) within a given context (`ctx`).
    *

src/web/app/explainthis/ExplainThis.re

@@ -2400,6 +2400,7 @@ let get_doc =
     switch (bypass_parens_typ(term).term) {
     | Unknown(SynSwitch)
     | Unknown(Internal)
+    | Unknown(Inconsistent)
     | Unknown(Hole(EmptyHole)) => get_message(HoleTyp.empty_hole)
     | Unknown(Hole(MultiHole(_))) => get_message(HoleTyp.multi_hole)
     | Atom(Int) => get_message(TerminalTyp.int)

src/web/app/input/Shortcut.re

@@ -130,6 +130,13 @@ let shortcuts = (sys: Util.Key.sys): list(t) =>
       "Type",
       Globals(ActiveEditor(Project(SetIndicated(Specific(Info))))),
     ),
+    mk_shortcut(
+      ~hotkey="alt+d",
+      ~mdIcon="camera",
+      ~section="Projection",
+      "Dynamic Type",
+      Globals(ActiveEditor(Project(SetIndicated(Specific(DynType))))),
+    ),
     mk_shortcut(
       ~hotkey="alt+l",
       ~mdIcon="camera",

src/web/www/style/projectors/proj-base.css

@@ -3,6 +3,7 @@
 @import "panel.css";
 @import "proj-probe.css";
 @import "proj-type.css";
+@import "proj-dyntype.css";
 @import "proj-cards.css";
 @import "proj-text.css";
 @import "proj-fold.css";