Reapply "Unused Variable Warnings" (#1825)

src/haz3lcore/derived/CachedStatics.re

@@ -7,6 +7,7 @@ type t = {
   elaborated: Exp.t,
   info_map: Statics.Map.t,
   error_ids: list(Id.t),
+  warning_ids: list(Id.t),
   targets: Sample.targets /* Maps expr/pat IDs to capture specs for sampling */
 };
 
@@ -21,6 +22,7 @@ let empty: t = {
   },
   info_map: Id.Map.empty,
   error_ids: [],
+  warning_ids: [],
   targets: Sample.no_targets,
 };
 
@@ -92,6 +94,7 @@ let init_from_term =
     );
   let info_map = Statics.mk(~ana?, settings, ctx_init, term);
   let error_ids = Statics.Map.error_ids(info_map);
+  let warning_ids = Statics.Map.warning_ids(info_map);
   let elaborated =
     switch () {
     | _ when !settings.statics => dh_err("Statics disabled")
@@ -109,6 +112,7 @@ let init_from_term =
     elaborated,
     info_map,
     error_ids,
+    warning_ids,
     targets,
   };
 };

src/haz3lcore/projectors/ProjectorBase.re

@@ -112,7 +112,8 @@ module View = {
     sort: Sort.t, /* What sort does the parent editor attribute to the projector? */
     indication: option(Direction.t), /* Is the parent editor caret adjacent? */
     selected: bool, /* Is the projector contained within a selection? */
-    error: bool /* Is there an error mark on the projector? */
+    error: bool, /* Is there an error mark on the projector? */
+    warning: bool /* Is there a warning mark on the projector? */
   };
 
   [@deriving (show({with_path: false}), sexp, yojson)]

src/language/CoreSettings.re

@@ -42,6 +42,7 @@ type t = {
   dynamics: bool,
   probe_all: bool,
   flip_animations: bool,
+  display_warnings: bool,
   evaluation: Evaluation.t,
 };
 
@@ -52,6 +53,7 @@ let off: t = {
   dynamics: false,
   probe_all: false,
   flip_animations: false,
+  display_warnings: false,
   evaluation: Evaluation.init,
 };
 
@@ -62,6 +64,7 @@ let on: t = {
   dynamics: true,
   probe_all: false, /* Off by default even in "on" config - opt-in feature */
   flip_animations: true,
+  display_warnings: true,
   evaluation: Evaluation.init,
 };
 

src/language/statics/CoCtx.re

@@ -79,6 +79,9 @@ let meet: (Ctx.t, list(entry)) => Typ.t =
     };
   };
 
+let contains_hole = (co_ctx: t): bool =>
+  VarMap.lookup(co_ctx, "$hole") !== None;
+
 let has_any = (co_ctx: t, vs: list(Var.t)): bool => {
   List.exists(v => VarMap.contains(co_ctx, v), vs);
 };

src/language/statics/Info.re

@@ -272,6 +272,7 @@ type exp = {
   co_ctx: CoCtx.t, /* Locally free variables */
   cls: Cls.t, /* DERIVED: Syntax class (i.e. form name) */
   status: status_exp, /* DERIVED: Ok/Error statuses for display */
+  warning: Warning.t,
   ty: Typ.t, /* DERIVED: Type after nonempty hole fixing */
   label_inference: option(label_inference(exp)), /* Label inference information for the tuple */
   inferred_label: option(LabeledTuple.label), /* Inferred label for an expression within the tuple */
@@ -289,6 +290,7 @@ type pat = {
   self: Self.pat,
   cls: Cls.t,
   status: status_pat,
+  warning: Warning.t,
   ty: Typ.t,
   constraint_: Coverage.Constraint.t,
   label_inference: option(label_inference(pat)),
@@ -304,6 +306,7 @@ type typ = {
   expects: typ_expects,
   cls: Cls.t,
   status: status_typ,
+  warning: Warning.t,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -313,6 +316,7 @@ type tpat = {
   ctx: Ctx.t,
   cls: Cls.t,
   status: status_tpat,
+  warning: Warning.t,
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -402,6 +406,14 @@ let error_of: t => option(error) =
   | InfoTPat({status: InHole(err), _}) => Some(TPat(err))
   | Secondary(_) => None;
 
+let warning_of: t => Warning.t =
+  fun
+  | InfoExp({warning, _})
+  | InfoPat({warning, _})
+  | InfoTyp({warning, _})
+  | InfoTPat({warning, _}) => warning
+  | Secondary(_) => None;
+
 /* A term is "typable" if it can meaningfully be assigned a type and will
    have a runtime value. This includes expressions and patterns, but excludes
    types, type patterns, and certain expression forms (deferrals, labels,
@@ -800,6 +812,8 @@ let is_error = (ci: t): bool => {
   };
 };
 
+let is_warning = (ci: t): bool => warning_of(ci) != None;
+
 /* Determined the type of an expression or pattern 'after hole fixing';
    that is, some ill-typed terms are considered to be 'wrapped in
    non-empty holes', i.e. assigned Unknown type. */
@@ -921,12 +935,14 @@ let derived_exp =
   let cls = Cls.Exp(Exp.cls_of_term(uexp.term));
   let status = status_exp(ctx, ana, self);
   let ty = fixed_typ_exp(ctx, ana, self);
+  let warning: Warning.t = None;
   {
     cls,
     self,
     ty,
     ana,
     status,
+    warning,
     ctx,
     co_ctx,
     ancestors,
@@ -956,6 +972,11 @@ let derived_pat =
   let cls = Cls.Pat(Pat.cls_of_term(upat.term));
   let status = status_pat(ctx, ana, self);
   let ty = fixed_typ_pat(ctx, ana, self);
+  let warning: Warning.t =
+    switch (upat.term) {
+    | Var(name) => Warning.var_is_unused(co_ctx, name)
+    | _ => None
+    };
 
   // replace constraints with Hole if this info has an error
   let constraint_': Coverage.Constraint.t =
@@ -972,6 +993,7 @@ let derived_pat =
     ana,
     ty,
     status,
+    warning,
     ctx,
     co_ctx,
     ancestors,
@@ -993,12 +1015,14 @@ let derived_typ = (~utyp: Typ.t, ~ctx, ~ancestors, ~expects): typ => {
     | (_, cls) => Cls.Typ(cls)
     };
   let status = status_typ(ctx, expects, utyp);
+  let warning: Warning.t = None;
   {
     cls,
     ctx,
     ancestors,
     status,
     expects,
+    warning,
     term: utyp,
   };
 };
@@ -1007,10 +1031,12 @@ let derived_typ = (~utyp: Typ.t, ~ctx, ~ancestors, ~expects): typ => {
 let derived_tpat = (~utpat: TPat.t, ~ctx, ~ancestors): tpat => {
   let cls = Cls.TPat(TPat.cls_of_term(utpat.term));
   let status = status_tpat(ctx, utpat);
+  let warning: Warning.t = None;
   {
     cls,
     ancestors,
     status,
+    warning,
     ctx,
     term: utpat,
   };

src/language/statics/Statics.re

@@ -288,10 +288,28 @@ and uexp_to_info_map =
 
     (info, add_info(IdTagged.ids(elaborated_exp), InfoExp(info), m));
   };
+
   let atomic = self => {
-    add(~self, ~co_ctx=CoCtx.empty, m);
+    // HACK: we use the co-context to check for unused variables in surrounding
+    // pattern bindings, but we don't want unused variable warnings to appear
+    // when there are holes present in the binding scopes. so if we detect a
+    // a hole in this expression, we add a "$hole" entry to the co-context
+    // that gets bubbled up to the relevant bindings and is checked for in the
+    // warning logic.
+    let hole_co_ctx =
+      switch (term) {
+      | MultiHole(_)
+      | EmptyHole
+      | Invalid(_) =>
+        CoCtx.singleton(
+          "$hole",
+          Exp.rep_id(uexp),
+          Unknown(Internal) |> Typ.temp,
+        )
+      | _ => CoCtx.empty
+      };
+    add(~self, ~co_ctx=hole_co_ctx, m);
   };
-
   // This is the case where we aren't a singleton labeled tuple
   let default_case = () => {
     switch (term) {
@@ -365,11 +383,8 @@ and uexp_to_info_map =
         m,
       );
     | Var(name) =>
-      add'(
-        ~self=Self.of_exp_var(ctx, name),
-        ~co_ctx=CoCtx.singleton(name, Exp.rep_id(uexp), ana),
-        m,
-      )
+      let co_ctx = CoCtx.singleton(name, Exp.rep_id(uexp), ana);
+      add'(~self=Self.of_exp_var(ctx, name), ~co_ctx, m);
     | DynamicErrorHole(e, _)
     | Parens(e)
     | Projector(_, e) =>
@@ -1218,8 +1233,7 @@ and uexp_to_info_map =
         );
 
       let e_tys = List.map(Info.exp_ty, es);
-      let e_co_ctxs =
-        List.map2(CoCtx.mk(ctx), p_ctxs, List.map(Info.exp_co_ctx, es));
+      let e_co_ctxs = List.map(Info.exp_co_ctx, es);
       let unwrapped_self: Self.exp =
         Common(Self.match(ctx, e_tys, branch_ids));
       let (constraints, m) =
@@ -1279,7 +1293,12 @@ and uexp_to_info_map =
         );
       };
       let m = add_redundancy(ps, redundant_rows, m);
-      add'(~self, ~co_ctx=CoCtx.union([scrut.co_ctx] @ e_co_ctxs), m);
+      let co_ctx =
+        CoCtx.union([
+          scrut.co_ctx,
+          ...List.map2(CoCtx.mk(ctx), p_ctxs, e_co_ctxs),
+        ]);
+      add'(~self, ~co_ctx, m);
     | TyAlias(typat, utyp, body) =>
       let m = utpat_to_info_map(~ctx, ~ancestors, typat, m) |> snd;
       switch (typat.term) {
@@ -1393,6 +1412,7 @@ and upat_to_info_map =
     (
       ~is_synswitch,
       ~ctx,
+      // the co-ctx of the pattern's scope
       ~co_ctx,
       ~ancestors: Info.ancestors,
       ~duplicate_bindings: list(string)=[],
@@ -2053,6 +2073,7 @@ and utyp_to_info_map =
       status: InHole(BadToken("_")),
       expects,
       term: utyp,
+      warning: None,
     };
     (info, add_info(ids, InfoTyp(info), m));
   | TupLabel({term: ExplicitNonlabel, _} as label, t) =>
@@ -2065,6 +2086,7 @@ and utyp_to_info_map =
       status: NotInHole(EmptyLabel),
       expects,
       term: utyp,
+      warning: None,
     };
 
     let m = add_info(label.annotation.ids, InfoTyp(label_info), m);

src/language/statics/StaticsBase.re

@@ -21,6 +21,17 @@ module Map = {
       info_map,
       [],
     );
+  let warning_ids = (info_map: t): list(Id.t) =>
+    Id.Map.fold(
+      (id, info, acc) =>
+        acc
+        |> (
+          Info.is_warning(info) && id == Info.id_of(info)
+            ? List.cons(id) : Fun.id
+        ),
+      info_map,
+      [],
+    );
 
   let errors = (map: t): list((Id.t, Info.error)) =>
     Id.Map.fold(

src/language/statics/Warning.re

@@ -0,0 +1,23 @@
+open Util;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type warning_pat =
+  | UnusedVar(string);
+//  | ShadowedVar(string, string)
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t =
+  | WarningPat(warning_pat)
+  | None;
+
+let empty: t = None;
+
+let var_is_unused = (co_ctx, name): t =>
+  if (String.starts_with(~prefix="_", name) || CoCtx.contains_hole(co_ctx)) {
+    None;
+  } else {
+    switch (VarMap.lookup(co_ctx, name)) {
+    | None => WarningPat(UnusedVar(name))
+    | Some(_) => None
+    };
+  };

src/web/Settings.re

@@ -28,6 +28,7 @@ module Model = {
       dynamics: true,
       probe_all: false,
       flip_animations: true,
+      display_warnings: false,
       evaluation: {
         show_case_clauses: true,
         show_fn_bodies: false,
@@ -125,6 +126,7 @@ module Update = {
     | Evaluation(evaluation)
     | Sidebar(SidebarModel.Settings.action)
     | ExplainThis(ExplainThisModel.Settings.action)
+    | DisplayWarnings
     | Assistant(AssistantSettings.action)
     | FlipAnimations
     | ToggleLineNumbers
@@ -190,6 +192,13 @@ module Update = {
             flip_animations: !settings.core.flip_animations,
           },
         }
+      | DisplayWarnings => {
+          ...settings,
+          core: {
+            ...settings.core,
+            display_warnings: !settings.core.display_warnings,
+          },
+        }
       | Evaluation(u) =>
         let evaluation = settings.core.evaluation;
         let evaluation: Language.CoreSettings.Evaluation.t =

src/web/app/common/ProjectorView.re

@@ -79,6 +79,9 @@ module Model = {
     error:
       Option.map(Language.Info.is_error, info.statics)
       |> Option.value(~default=false),
+    warning:
+      Option.map(Language.Info.is_warning, info.statics)
+      |> Option.value(~default=false),
     kind: p.kind,
     indication: editor_active ? indication(indicated, id) : None,
     selected: editor_active ? List.mem(id, selection_ids) : false,
@@ -137,10 +140,11 @@ let backing_deco =
 /* Adds attributes to a projector UI to support
  * custom styling when selected or indicated */
 let projector_clss =
-    ({kind, sort, indication, selected, error}: Model.status) =>
+    ({kind, sort, indication, selected, error, warning}: Model.status) =>
   ["projector", ProjectorCore.Kind.name(kind), Sort.show(sort)]
   @ (selected ? ["selected"] : [])
   @ (error ? ["error"] : [])
+  @ (warning ? ["warning"] : [])
   @ (
     switch (indication) {
     | Some(d) => ["indicated", Direction.show(d)]