Update components with toolkit, settings dropdown, proper font sizes

crates/argus/src/analysis/entry.rs

@@ -209,24 +209,8 @@ pub(in crate::analysis) fn build_obligations_in_body<'tcx>(
   body_id: BodyId,
   typeck_results: &'tcx TypeckResults<'tcx>,
 ) -> (Forgettable<FullData<'tcx>>, ObligationsInBody) {
-  let mut obligations = tls::take_obligations();
-  let obligation_data = tls::unsafe_take_data();
-  let obligation_data = FullData::new(obligation_data);
-
-  // XXX: it's possible that Argus reports false negatives. Meaning that
-  // in a body that type checks, failing obligations are reported.
-  // This happens as a result of how predicates are extracted from rustc (ask gavin)
-  // so as a first heuristic, if the body isn't tainted by errors, we'll just remove
-  // all non-successful obligations.
-  if typeck_results.tainted_by_errors.is_none() {
-    log::debug!(
-      "Removing failures: Body not-tainted {:?}",
-      typeck_results.hir_owner
-    );
-    obligations.retain(|prov| prov.it.result.is_yes());
-  } else {
-    log::debug!("Body tainted! {:?}", typeck_results.hir_owner);
-  }
+  let obligations = tls::take_obligations();
+  let obligation_data = FullData::new(tls::unsafe_take_data());
 
   let ctx = ErrorAssemblyCtx {
     tcx,

crates/argus/src/analysis/transform.rs

@@ -148,6 +148,7 @@ pub fn transform<'a, 'tcx: 'a>(
 
   ObligationsInBody::new(
     name,
+    typeck_results.tainted_by_errors.is_some(),
     body_range,
     builder.ambiguity_errors,
     builder.trait_errors,

crates/argus/src/proof_tree/mod.rs

@@ -13,6 +13,7 @@ use index_vec::IndexVec;
 use rustc_infer::infer::InferCtxt;
 use rustc_middle::ty;
 use serde::Serialize;
+use serde_json as json;
 pub use topology::*;
 #[cfg(feature = "testing")]
 use ts_rs::TS;
@@ -48,7 +49,7 @@ pub enum Node {
 #[cfg_attr(feature = "testing", ts(export))]
 pub struct GoalData {
   #[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))]
-  value: serde_json::Value,
+  value: json::Value,
 
   necessity: ObligationNecessity,
   num_vars: usize,
@@ -69,7 +70,7 @@ pub struct GoalData {
 pub enum CandidateData {
   Impl {
     #[cfg_attr(feature = "testing", ts(type = "ImplHeader"))]
-    hd: serde_json::Value,
+    hd: json::Value,
     is_user_visible: bool,
   },
   ParamEnv(usize),
@@ -106,11 +107,11 @@ pub struct SerializedTree {
   pub results: IndexVec<ResultIdx, ResultData>,
 
   #[cfg_attr(feature = "testing", ts(type = "TyVal[]"))]
-  pub tys: IndexVec<TyIdx, serde_json::Value>,
+  pub tys: IndexVec<TyIdx, json::Value>,
 
   pub projection_values: HashMap<TyIdx, TyIdx>,
 
-  pub all_impl_candidates: HashMap<ProofNodeIdx, Vec<CandidateIdx>>,
+  pub all_impl_candidates: HashMap<ProofNodeIdx, Implementors>,
 
   pub topology: TreeTopology,
 
@@ -120,6 +121,17 @@ pub struct SerializedTree {
   pub analysis: aadebug::AnalysisResults,
 }
 
+#[derive(Serialize, Debug, Clone)]
+#[serde(rename_all = "camelCase")]
+#[cfg_attr(feature = "testing", derive(TS))]
+#[cfg_attr(feature = "testing", ts(export))]
+pub struct Implementors {
+  #[cfg_attr(feature = "testing", ts(type = "TraitRefPrintOnlyTraitPath"))]
+  pub _trait: json::Value,
+
+  pub impls: Vec<CandidateIdx>,
+}
+
 #[derive(Serialize, Debug, Clone)]
 #[cfg_attr(feature = "testing", derive(TS))]
 #[cfg_attr(feature = "testing", ts(export))]

crates/argus/src/proof_tree/serialize.rs

@@ -25,7 +25,7 @@ pub struct SerializedTreeVisitor<'tcx> {
   pub topology: TreeTopology,
   pub cycle: Option<ProofCycle>,
   pub projection_values: HashMap<TyIdx, TyIdx>,
-  pub all_impl_candidates: HashMap<ProofNodeIdx, Vec<CandidateIdx>>,
+  pub all_impl_candidates: HashMap<ProofNodeIdx, Implementors>,
 
   deferred_leafs: Vec<(ProofNodeIdx, EvaluationResult)>,
   interners: Interners,
@@ -243,14 +243,26 @@ impl<'tcx> SerializedTreeVisitor<'tcx> {
     // If the Goal is a TraitPredicate we will cache *all* possible implementors
     if let Some(tp) = goal.goal().predicate.as_trait_predicate() {
       let infcx = goal.infcx();
+
+      // Make Trait ref name
+      // FIXME: this is a mega hack
+      let _trait =
+        ser::TraitRefPrintOnlyTraitPathDef(tp.skip_binder().trait_ref);
+
+      let _trait = tls::unsafe_access_interner(|ty_interner| {
+        ser::to_value_expect(infcx, ty_interner, &_trait)
+      });
+
+      // Gather all impls
+      let mut impls = vec![];
       for can in infcx.find_similar_impl_candidates(tp) {
         let can_idx = self.interners.intern_impl(infcx, can.impl_def_id);
-        self
-          .all_impl_candidates
-          .entry(idx)
-          .or_default()
-          .push(can_idx);
+        impls.push(can_idx);
       }
+
+      self
+        .all_impl_candidates
+        .insert(idx, Implementors { _trait, impls });
     }
   }
 }

crates/argus/src/types.rs

@@ -134,6 +134,8 @@ pub struct ObligationsInBody {
   /// Range of the represented body.
   pub range: CharRange,
 
+  pub is_tainted: bool,
+
   /// All ambiguous expression in the body. These *could* involve
   /// trait errors, so it's important that we can map the specific
   /// obligations to these locations. (That is, if they occur.)
@@ -157,6 +159,7 @@ pub struct ObligationsInBody {
 impl ObligationsInBody {
   pub fn new(
     id: Option<(&InferCtxt, DefId)>,
+    is_tainted: bool,
     range: CharRange,
     ambiguity_errors: IndexSet<AmbiguityError>,
     trait_errors: Vec<TraitError>,
@@ -174,6 +177,7 @@ impl ObligationsInBody {
       name: json_name,
       hash: BodyHash::new(),
       range,
+      is_tainted,
       ambiguity_errors,
       trait_errors,
       obligations,

ide/packages/common/src/BodyInfo.ts

@@ -8,7 +8,7 @@ import type {
   ObligationIdx,
   ObligationsInBody
 } from "./bindings";
-import { isVisibleObligation } from "./func";
+// import { isVisibleObligation } from "./func";
 
 class BodyInfo {
   private existsImportantFailure;
@@ -29,12 +29,20 @@ class BodyInfo {
     );
   }
 
+  get isTainted(): boolean {
+    return this.oib.isTainted;
+  }
+
   get hash(): BodyHash {
     return this.oib.hash;
   }
 
   get numErrors(): number {
-    return this.oib.ambiguityErrors.length + this.oib.traitErrors.length;
+    // NOTE: is the body isn't tainted by errors, the number of errors
+    // is ZERO, even if Argus sends errors to the frontend.
+    return !this.isTainted
+      ? 0
+      : this.oib.ambiguityErrors.length + this.oib.traitErrors.length;
   }
 
   get name() {
@@ -100,18 +108,25 @@ class BodyInfo {
   isVisible(idx: ObligationIdx) {
     const o = this.obligation(idx);
     if (o === undefined) return false;
+    // If the body isn't tainted by errors, we only show obligations that hold true.
+    if (!this.isTainted && o.result !== "yes") return false;
 
-    return (
-      this.showHidden ||
-      isVisibleObligation(
-        o,
+    const _isVisibleObligation = () =>
+      // Short-circuit ambiguities if we're filtering them
+      !(
+        (o.result === "maybe-ambiguity" || o.result === "maybe-overflow") &&
         // HACK: If there is a failing obligation, we filter ambiguities. This is
         // a short workaround for a backend incompleteness. We can't filter obligations
         // that get resolved in a second round of trait solving, this leaves Argus with
         // more "failures" than rustc shows.
         this.existsImportantFailure
-      )
-    );
+      ) &&
+      // If the obligation is listed as necessary, it's visible
+      (o.necessity === "Yes" ||
+        // If the obligation is listed as necessary on error, and it failed, it's visible
+        (o.necessity === "OnError" && o.result === "no"));
+
+    return this.showHidden || _isVisibleObligation();
   }
 }
 

ide/packages/common/src/TreeInfo.ts

@@ -6,6 +6,7 @@ import type {
   EvaluationResult,
   GoalIdx,
   GoalKind,
+  Implementors,
   ProofNodeIdx,
   ResultIdx,
   SerializedTree,
@@ -442,7 +443,7 @@ export class TreeInfo {
     return _.min(_.map(hs, TreeInfo.setInertia)) ?? 10_000;
   }
 
-  public implCandidates(idx: ProofNodeIdx): CandidateIdx[] | undefined {
+  public implCandidates(idx: ProofNodeIdx): Implementors | undefined {
     return this.tree.allImplCandidates[idx];
   }
 }

ide/packages/common/src/context.ts

@@ -10,13 +10,19 @@ import type {
   SystemSpec
 } from "./lib";
 
+export const settingsToggles = ["show-hidden-obligations"] as const;
+
+export type Settings = {
+  [K in (typeof settingsToggles)[number]]: boolean;
+};
+
 export const AppContext = {
   MessageSystemContext: createContext<MessageSystem | undefined>(undefined),
   ConfigurationContext: createContext<
     (PanoptesConfig & { evalMode: EvaluationMode }) | undefined
   >(undefined),
   SystemSpecContext: createContext<SystemSpec | undefined>(undefined),
-  ShowHiddenObligationsContext: createContext<boolean>(false)
+  SettingsContext: createContext<Settings>({ "show-hidden-obligations": false })
 };
 
 export const FileContext = createContext<Filename | undefined>(undefined);

ide/packages/common/src/func.ts

@@ -5,10 +5,8 @@ import type {
   BoundTyKind,
   BoundVariableKind,
   CharRange,
-  EvaluationResult,
   GenericArg,
   ObligationHash,
-  ObligationNecessity,
   Predicate,
   Region,
   Ty,
@@ -67,19 +65,10 @@ export function makeHighlightPosters(
   return [addHighlight, removeHighlight];
 }
 
-export const isVisibleObligation = (
-  o: { necessity: ObligationNecessity; result: EvaluationResult },
-  filterAmbiguities = false
-) =>
-  // Short-circuit ambiguities if we're filtering them
-  !(
-    (o.result === "maybe-ambiguity" || o.result === "maybe-overflow") &&
-    filterAmbiguities
-  ) &&
-  // If the obligation is listed as necessary, it's visible
-  (o.necessity === "Yes" ||
-    // If the obligation is listed as necessary on error, and it failed, it's visible
-    (o.necessity === "OnError" && o.result === "no"));
+export const composeEvents =
+  <T>(...es: (((t: T) => void) | undefined)[]) =>
+  (t: T) =>
+    _.forEach(es, e => (e ? e(t) : {}));
 
 export function searchObject(obj: any, target: any) {
   for (let key in obj) {

ide/packages/panoptes/src/App.css

@@ -1,5 +1,5 @@
 #root {
-    font-size: var(--vscode-editor-font-size);
+    font-size: var(--vscode-font-size);
 }
 
 .app-nav {
@@ -20,6 +20,22 @@
     margin-bottom: 0.25em;
 }
 
+.SettingsArea {
+    display: flex;
+    flex-direction: column;
+    gap: 0.5em;
+    justify-content: flex-start;
+}
+
+.SettingsIco {
+    padding: 0.25em;
+}
+
+.SettingsIco > i:hover {
+    cursor: pointer;
+    color: var(--vscode-input-placeholderForeground);
+}
+
 .DefinitionWrapper.hovered.meta-pressed {
     color: var(--vscode-editorLink-activeForeground);
     text-decoration: underline;