Allow Erotisi panel for singleton sets. Factor out DNF

crates/argus/src/aadebug/dnf.rs

@@ -0,0 +1,73 @@
+// TODO: this is a very naive implementation, we can certainly make it more efficient.
+pub struct And<I: Copy>(Vec<I>);
+pub struct Dnf<I: Copy>(Vec<And<I>>);
+
+impl<I: Copy> IntoIterator for And<I> {
+  type Item = I;
+  type IntoIter = std::vec::IntoIter<I>;
+
+  fn into_iter(self) -> Self::IntoIter {
+    self.0.into_iter()
+  }
+}
+
+impl<I: Copy> And<I> {
+  #[inline]
+  pub fn iter(&self) -> impl Iterator<Item = &I> + '_ {
+    self.0.iter()
+  }
+
+  fn distribute(&self, rhs: &Dnf<I>) -> Dnf<I> {
+    Dnf(
+      rhs
+        .0
+        .iter()
+        .map(|And(rhs)| {
+          And(self.0.iter().copied().chain(rhs.iter().copied()).collect())
+        })
+        .collect(),
+    )
+  }
+}
+
+impl<I: Copy> Dnf<I> {
+  pub fn into_iter_conjuncts(self) -> impl Iterator<Item = And<I>> {
+    self.0.into_iter()
+  }
+
+  pub fn and(vs: impl Iterator<Item = Self>) -> Option<Self> {
+    vs.fold(None, |opt_lhs, rhs| match opt_lhs {
+      None => Some(rhs),
+      Some(lhs) => Self::distribute(lhs, rhs),
+    })
+  }
+
+  pub fn or(vs: impl Iterator<Item = Self>) -> Option<Self> {
+    let vs = vs.flat_map(|Self(v)| v).collect::<Vec<_>>();
+    if vs.is_empty() {
+      None
+    } else {
+      Some(Self(vs))
+    }
+  }
+
+  #[allow(clippy::needless_pass_by_value)]
+  fn distribute(self, other: Self) -> Option<Self> {
+    Self::or(
+      self
+        .0
+        .into_iter()
+        .map(|conjunct| conjunct.distribute(&other)),
+    )
+  }
+
+  #[inline]
+  pub fn single(i: I) -> Self {
+    Self(vec![And(vec![i])])
+  }
+
+  #[inline]
+  pub fn default() -> Self {
+    Self(vec![])
+  }
+}

crates/argus/src/aadebug/mod.rs

@@ -1,3 +1,4 @@
+mod dnf;
 mod tree;
 mod ty;
 
@@ -8,7 +9,7 @@ use argus_ext::ty::EvaluationResultExt;
 use index_vec::IndexVec;
 use rustc_infer::traits::solve::GoalSource;
 use rustc_trait_selection::solve::inspect::{InspectCandidate, InspectGoal};
-use rustc_utils::timer::elapsed;
+use rustc_utils::timer;
 use serde::Serialize;
 #[cfg(feature = "testing")]
 use ts_rs::TS;
@@ -119,11 +120,11 @@ impl<'tcx> Storage<'tcx> {
       tree
         .iter_correction_sets()
         .fold(Vec::new(), |mut sets, conjunct| {
-          sets.push(conjunct.weight(tree));
+          sets.push(tree.weight(&conjunct));
           sets
         });
 
-    elapsed("aadeg::into_results", tree_start);
+    timer::elapsed("aadeg::into_results", tree_start);
 
     AnalysisResults {
       problematic_sets: sets,

crates/argus/src/aadebug/tree.rs

@@ -8,21 +8,19 @@ use rustc_middle::{
   ty::{self, TyCtxt},
 };
 use rustc_trait_selection::solve::inspect::ProbeKind;
-use rustc_utils::timer::elapsed;
+use rustc_utils::timer;
 use serde::Serialize;
 #[cfg(feature = "testing")]
 use ts_rs::TS;
 
+use super::dnf::{And, Dnf};
 use crate::{
   analysis::EvaluationResult,
   proof_tree::{topology::TreeTopology, ProofNodeIdx},
 };
 
 pub type I = ProofNodeIdx;
 
-pub struct And(Vec<I>);
-pub struct Dnf(Vec<And>);
-
 #[derive(Serialize, Debug, Clone)]
 #[serde(rename_all = "camelCase")]
 #[cfg_attr(feature = "testing", derive(TS))]
@@ -100,96 +98,6 @@ impl GoalKind {
   }
 }
 
-impl And {
-  fn distribute(&self, rhs: &Dnf) -> Dnf {
-    Dnf(
-      rhs
-        .0
-        .iter()
-        .map(|And(rhs)| {
-          And(self.0.iter().copied().chain(rhs.iter().copied()).collect())
-        })
-        .collect(),
-    )
-  }
-
-  /// Failed predicates are weighted as follows.
-  ///
-  /// Each predicate is marked as local / external, local predicates are
-  /// trusted less, while external predicates are assumed correct.
-  ///
-  /// Trait predicates `T: C`, are weighted by how much they could change.
-  /// A type `T` that is local is non-rigid while external types are considered
-  /// rigid, meaning they cannot be changed.
-  ///
-  /// Non-intrusive changes:
-  ///
-  /// A local type failing to implement a trait (local/external).
-  /// NOTE that `T: C` where `T` is an external type is considered impossible
-  /// to change, if this is the only option a relaxed rule might suggest
-  /// creating a wapper for the type.
-  ///
-  /// Intrusive changes
-  ///
-  /// Changing types. That could either be changing a type to match an
-  /// alias-relate, deleting function parameters or tuple elements.
-  pub fn weight(self, tree: &T) -> SetHeuristic {
-    let goals = self
-      .0
-      .iter()
-      .map(|&idx| tree.goal(idx).expect("goal").analyze())
-      .collect::<Vec<_>>();
-
-    let momentum = goals.iter().fold(0, |acc, g| acc + g.kind.weight());
-    let velocity = self
-      .0
-      .iter()
-      .map(|&idx| tree.topology.depth(idx))
-      .max()
-      .unwrap_or(0);
-
-    SetHeuristic {
-      momentum,
-      velocity,
-      goals,
-    }
-  }
-}
-
-impl Dnf {
-  pub fn into_iter_conjuncts(self) -> impl Iterator<Item = And> {
-    self.0.into_iter()
-  }
-
-  fn or(vs: impl Iterator<Item = Self>) -> Option<Self> {
-    let vs = vs.flat_map(|Self(v)| v).collect::<Vec<_>>();
-    if vs.is_empty() {
-      None
-    } else {
-      Some(Self(vs))
-    }
-  }
-
-  #[allow(clippy::needless_pass_by_value)]
-  fn distribute(self, other: Self) -> Self {
-    Self::or(
-      self
-        .0
-        .into_iter()
-        .map(|conjunct| conjunct.distribute(&other)),
-    )
-    .expect("non-empty")
-  }
-
-  fn and(vs: impl Iterator<Item = Self>) -> Option<Self> {
-    vs.reduce(Self::distribute)
-  }
-
-  fn single(i: I) -> Self {
-    Self(vec![And(vec![i])])
-  }
-}
-
 #[allow(clippy::struct_field_names)]
 pub struct Goal<'a, 'tcx> {
   idx: I,
@@ -451,8 +359,8 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
     }
   }
 
-  pub fn dnf(&self) -> Dnf {
-    fn _goal(this: &T, goal: &Goal) -> Option<Dnf> {
+  pub fn dnf(&self) -> Dnf<I> {
+    fn _goal(this: &T, goal: &Goal) -> Option<Dnf<I>> {
       if !((this.maybe_ambiguous && goal.result.is_maybe())
         || goal.result.is_no())
       {
@@ -471,30 +379,69 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
       Dnf::or(nested.into_iter())
     }
 
-    fn _candidate(this: &T, candidate: &Candidate) -> Option<Dnf> {
+    fn _candidate(this: &T, candidate: &Candidate) -> Option<Dnf<I>> {
       if candidate.result.is_yes() {
         return None;
       }
 
       let goals = candidate.source_subgoals();
-      let nested = goals.filter_map(|g| _goal(this, &g)).collect::<Vec<_>>();
-
-      if nested.is_empty() {
-        return None;
-      }
-
-      Dnf::and(nested.into_iter())
+      Dnf::and(goals.filter_map(|g| _goal(this, &g)))
     }
 
+    let dnf_report_msg =
+      format!("Normalizing to DNF from {} nodes", self.ns.len());
+    let dnf_start = Instant::now();
+
     let root = self.goal(self.root).expect("invalid root");
-    _goal(self, &root).unwrap_or_else(|| Dnf(vec![]))
+    let dnf = _goal(self, &root).unwrap_or_else(|| Dnf::default());
+    timer::elapsed(&dnf_report_msg, dnf_start);
+
+    dnf
+  }
+
+  /// Failed predicates are weighted as follows.
+  ///
+  /// Each predicate is marked as local / external, local predicates are
+  /// trusted less, while external predicates are assumed correct.
+  ///
+  /// Trait predicates `T: C`, are weighted by how much they could change.
+  /// A type `T` that is local is non-rigid while external types are considered
+  /// rigid, meaning they cannot be changed.
+  ///
+  /// Non-intrusive changes:
+  ///
+  /// A local type failing to implement a trait (local/external).
+  /// NOTE that `T: C` where `T` is an external type is considered impossible
+  /// to change, if this is the only option a relaxed rule might suggest
+  /// creating a wapper for the type.
+  ///
+  /// Intrusive changes
+  ///
+  /// Changing types. That could either be changing a type to match an
+  /// alias-relate, deleting function parameters or tuple elements.
+  pub fn weight(&self, and: &And<I>) -> SetHeuristic {
+    let goals = and
+      .iter()
+      .map(|&idx| self.goal(idx).expect("goal").analyze())
+      .collect::<Vec<_>>();
+
+    let momentum = goals.iter().fold(0, |acc, g| acc + g.kind.weight());
+    let velocity = and
+      .iter()
+      .map(|&idx| self.topology.depth(idx))
+      .max()
+      .unwrap_or(0);
+
+    SetHeuristic {
+      momentum,
+      velocity,
+      goals,
+    }
   }
 
-  pub fn iter_correction_sets(&self) -> impl Iterator<Item = And> {
-    let tree_start = Instant::now();
-    let iter = self.dnf().into_iter_conjuncts();
-    elapsed("tree::dnf", tree_start);
-    iter
+  #[inline]
+  pub fn iter_correction_sets(&self) -> impl Iterator<Item = And<I>> {
+    self.dnf().into_iter_conjuncts()
   }
 }
 

flake.nix

@@ -42,12 +42,16 @@
 
         llvmPackages_latest.llvm
         llvmPackages_latest.lld
+
         guile
         depotjs
         nodejs_22
         nodePackages.pnpm
+
         cargo-make
         cargo-watch
+        rust-analyzer
+
         toolchain
       ] ++ lib.optionals stdenv.isDarwin [
         darwin.apple_sdk.frameworks.SystemConfiguration

ide/packages/panoptes/src/TreeView/Erotisi.tsx

@@ -1,7 +1,9 @@
 import type { TreeInfo } from "@argus/common/TreeInfo";
 import type { ProofNodeIdx, SetHeuristic } from "@argus/common/bindings";
 import { TreeAppContext } from "@argus/common/context";
+import ErrorDiv from "@argus/print/ErrorDiv";
 import Indented from "@argus/print/Indented";
+import ReportBugUrl from "@argus/print/ReportBugUrl";
 import { VSCodeButton } from "@vscode/webview-ui-toolkit/react";
 import _ from "lodash";
 import React, { useContext, useState } from "react";
@@ -80,9 +82,19 @@ function formOptions(
 const Erotisi = () => {
   const tree = useContext(TreeAppContext.TreeContext)!;
   const sets = sortedSubsets(tree.failedSets);
-  // If there's only one error we don't need to present questions...
-  if (sets.length <= 1) {
-    return null;
+  if (sets.length === 0) {
+    return (
+      <ErrorDiv>
+        <p>
+          Argus didn’t find any root errors in this tree. If you’re seeing this,
+          it’s likely a bug. Please click below to report it!
+        </p>
+        <ReportBugUrl
+          error={"No error sets found for tree"}
+          logText={JSON.stringify(tree)}
+        />
+      </ErrorDiv>
+    );
   }
 
   const firstForm = formOptions(tree, sets, []);