From 56228a6fdbb71d3ceed66d9641afa4abd7110c65 Mon Sep 17 00:00:00 2001 From: gavinleroy Date: Thu, 11 Jul 2024 17:46:55 -0600 Subject: [PATCH] Allow Erotisi panel for singleton sets. Factor out DNF --- crates/argus/src/aadebug/dnf.rs | 73 ++++++++ crates/argus/src/aadebug/mod.rs | 7 +- crates/argus/src/aadebug/tree.rs | 167 ++++++------------ flake.nix | 4 + .../panoptes/src/TreeView/Erotisi.tsx | 18 +- 5 files changed, 153 insertions(+), 116 deletions(-) create mode 100644 crates/argus/src/aadebug/dnf.rs diff --git a/crates/argus/src/aadebug/dnf.rs b/crates/argus/src/aadebug/dnf.rs new file mode 100644 index 0000000..5374acf --- /dev/null +++ b/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(Vec); +pub struct Dnf(Vec>); + +impl IntoIterator for And { + type Item = I; + type IntoIter = std::vec::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + self.0.into_iter() + } +} + +impl And { + #[inline] + pub fn iter(&self) -> impl Iterator + '_ { + self.0.iter() + } + + fn distribute(&self, rhs: &Dnf) -> Dnf { + Dnf( + rhs + .0 + .iter() + .map(|And(rhs)| { + And(self.0.iter().copied().chain(rhs.iter().copied()).collect()) + }) + .collect(), + ) + } +} + +impl Dnf { + pub fn into_iter_conjuncts(self) -> impl Iterator> { + self.0.into_iter() + } + + pub fn and(vs: impl Iterator) -> Option { + vs.fold(None, |opt_lhs, rhs| match opt_lhs { + None => Some(rhs), + Some(lhs) => Self::distribute(lhs, rhs), + }) + } + + pub fn or(vs: impl Iterator) -> Option { + let vs = vs.flat_map(|Self(v)| v).collect::>(); + if vs.is_empty() { + None + } else { + Some(Self(vs)) + } + } + + #[allow(clippy::needless_pass_by_value)] + fn distribute(self, other: Self) -> Option { + 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![]) + } +} diff --git a/crates/argus/src/aadebug/mod.rs b/crates/argus/src/aadebug/mod.rs index 5396a3b..7270b64 100644 --- a/crates/argus/src/aadebug/mod.rs +++ b/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, diff --git a/crates/argus/src/aadebug/tree.rs b/crates/argus/src/aadebug/tree.rs index 058bdd8..0bbcd18 100644 --- a/crates/argus/src/aadebug/tree.rs +++ b/crates/argus/src/aadebug/tree.rs @@ -8,11 +8,12 @@ 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}, @@ -20,9 +21,6 @@ use crate::{ pub type I = ProofNodeIdx; -pub struct And(Vec); -pub struct Dnf(Vec); - #[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::>(); - - 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 { - self.0.into_iter() - } - - fn or(vs: impl Iterator) -> Option { - let vs = vs.flat_map(|Self(v)| v).collect::>(); - 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) -> Option { - 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 { + pub fn dnf(&self) -> Dnf { + fn _goal(this: &T, goal: &Goal) -> Option> { 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 { + fn _candidate(this: &T, candidate: &Candidate) -> Option> { if candidate.result.is_yes() { return None; } let goals = candidate.source_subgoals(); - let nested = goals.filter_map(|g| _goal(this, &g)).collect::>(); - - 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) -> SetHeuristic { + let goals = and + .iter() + .map(|&idx| self.goal(idx).expect("goal").analyze()) + .collect::>(); + + 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 { - 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> { + self.dnf().into_iter_conjuncts() } } diff --git a/flake.nix b/flake.nix index ad9aafe..4204072 100644 --- a/flake.nix +++ b/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 diff --git a/ide/packages/panoptes/src/TreeView/Erotisi.tsx b/ide/packages/panoptes/src/TreeView/Erotisi.tsx index 06108c6..efde208 100644 --- a/ide/packages/panoptes/src/TreeView/Erotisi.tsx +++ b/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 ( + +

+ 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! +

+ + + ); } const firstForm = formOptions(tree, sets, []);