Skip to content

Commit

Permalink
Add impl candidates for each proof node idx
Browse files Browse the repository at this point in the history
  • Loading branch information
gavinleroy committed Aug 16, 2024
1 parent 3443fb5 commit f28c069
Show file tree
Hide file tree
Showing 8 changed files with 49 additions and 65 deletions.
9 changes: 0 additions & 9 deletions crates/argus/src/aadebug/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,10 @@ use std::time::Instant;
use anyhow::Result;
use argus_ext::ty::EvaluationResultExt;
use index_vec::IndexVec;
use rustc_data_structures::fx::FxHashMap as HashMap;
use rustc_infer::traits::solve::GoalSource;
use rustc_trait_selection::solve::inspect::{InspectCandidate, InspectGoal};
use rustc_utils::timer;
use serde::Serialize;
use serde_json as json;
#[cfg(feature = "testing")]
use ts_rs::TS;

Expand All @@ -28,12 +26,6 @@ pub struct Storage<'tcx> {
#[cfg_attr(feature = "testing", ts(export))]
pub struct AnalysisResults {
pub problematic_sets: Vec<tree::SetHeuristic>,

#[cfg_attr(
feature = "testing",
ts(type = "Record<ProofNodeIdx, ImplHeader[]>")
)]
pub impl_candidates: HashMap<ProofNodeIdx, Vec<json::Value>>,
}

impl<'tcx> Storage<'tcx> {
Expand Down Expand Up @@ -126,7 +118,6 @@ impl<'tcx> Storage<'tcx> {

AnalysisResults {
problematic_sets: sets,
impl_candidates: tree.reportable_impl_candidates(),
}
}
}
45 changes: 1 addition & 44 deletions crates/argus/src/aadebug/tree.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,7 @@
use std::{cell::RefCell, ops::Deref, time::Instant};

use argus_ext::{
rustc::InferCtxtExt,
ty::{EvaluationResultExt, PredicateExt, TyCtxtExt, TyExt},
};
use argus_ser as ser;
use argus_ext::ty::{EvaluationResultExt, TyCtxtExt, TyExt};
use index_vec::IndexVec;
use rustc_data_structures::fx::FxHashMap as HashMap;
use rustc_infer::infer::InferCtxt;
use rustc_middle::{
traits::solve::{CandidateSource, Goal as RGoal},
Expand All @@ -22,7 +17,6 @@ use super::dnf::{And, Dnf};
use crate::{
analysis::EvaluationResult,
proof_tree::{topology::TreeTopology, ProofNodeIdx},
tls,
};

pub type I = ProofNodeIdx;
Expand Down Expand Up @@ -487,43 +481,6 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> {
goals,
}
}

pub fn reportable_impl_candidates(
&self,
) -> HashMap<I, Vec<serde_json::Value>> {
let mut indices = Vec::default();
self.for_correction_set(|and| indices.extend(and.iter().copied()));

let goals_only = indices.iter().filter_map(|&idx| self.goal(idx));

let trait_goals = goals_only.filter(|g| {
matches!(
g.analyze().kind,
GoalKind::Trait { .. } | GoalKind::FnToTrait { .. }
)
});

trait_goals
.filter_map(|g| {
g.predicate().as_trait_predicate().map(|tp| {
let candidates = g
.infcx
.find_similar_impl_candidates(tp)
.into_iter()
.filter_map(|can| {
let header =
ser::argus::get_opt_impl_header(g.infcx.tcx, can.impl_def_id)?;
Some(tls::unsafe_access_interner(|ty_interner| {
ser::to_value_expect(g.infcx, ty_interner, &header)
}))
})
.collect();

(g.idx, candidates)
})
})
.collect()
}
}

// ------------------
Expand Down
6 changes: 5 additions & 1 deletion crates/argus/src/proof_tree/interners.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,11 @@ impl Interners {
.insert(CanKey::ParamEnv(idx), CandidateData::ParamEnv(idx))
}

fn intern_impl(&mut self, infcx: &InferCtxt, def_id: DefId) -> CandidateIdx {
pub(super) fn intern_impl(
&mut self,
infcx: &InferCtxt,
def_id: DefId,
) -> CandidateIdx {
if let Some(i) = self.candidates.get_idx(&CanKey::Impl(def_id)) {
return i;
}
Expand Down
4 changes: 4 additions & 0 deletions crates/argus/src/proof_tree/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,9 +110,13 @@ pub struct SerializedTree {

pub projection_values: HashMap<TyIdx, TyIdx>,

pub all_impl_candidates: HashMap<ProofNodeIdx, Vec<CandidateIdx>>,

pub topology: TreeTopology,

#[serde(skip_serializing_if = "Option::is_none")]
pub cycle: Option<ProofCycle>,

pub analysis: aadebug::AnalysisResults,
}

Expand Down
34 changes: 32 additions & 2 deletions crates/argus/src/proof_tree/serialize.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
use anyhow::{bail, Result};
use argus_ext::ty::{EvaluationResultExt, TyExt};
use argus_ext::{
rustc::InferCtxtExt,
ty::{EvaluationResultExt, PredicateExt, TyExt},
};
use index_vec::IndexVec;
use rustc_hir::def_id::DefId;
use rustc_infer::infer::InferCtxt;
Expand All @@ -22,6 +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>>,

deferred_leafs: Vec<(ProofNodeIdx, EvaluationResult)>,
interners: Interners,
Expand All @@ -37,6 +41,7 @@ impl SerializedTreeVisitor<'_> {
topology: TreeTopology::new(),
cycle: None,
projection_values: HashMap::default(),
all_impl_candidates: HashMap::default(),

deferred_leafs: Vec::default(),
interners: Interners::default(),
Expand Down Expand Up @@ -117,6 +122,7 @@ impl SerializedTreeVisitor<'_> {
mut interners,
aadebug,
deferred_leafs,
all_impl_candidates,
..
} = self
else {
Expand All @@ -143,6 +149,7 @@ impl SerializedTreeVisitor<'_> {
results,
tys,
projection_values,
all_impl_candidates,
topology,
cycle,
analysis,
Expand All @@ -154,7 +161,7 @@ impl SerializedTreeVisitor<'_> {
// interned keys does essentially). We should wait until the new trait solver
// has some mechanism for detecting cycles and piggy back off that.
// FIXME: this is currently dissabled but we should check for cycles again...
#[allow(dead_code)]
#[allow(dead_code, unused)]
fn check_for_cycle_from(&mut self, from: ProofNodeIdx) {
if self.cycle.is_some() {
return;
Expand Down Expand Up @@ -226,6 +233,25 @@ impl<'tcx> SerializedTreeVisitor<'tcx> {
}
}
}

fn record_all_impls(
&mut self,
idx: ProofNodeIdx,
goal: &InspectGoal<'_, '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();
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);
}
}
}
}

impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor<'tcx> {
Expand All @@ -240,6 +266,10 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor<'tcx> {

let here_node = self.interners.mk_goal_node(goal);
let here_idx = self.nodes.push(here_node);

// Record all the possible candidate impls for this goal.
self.record_all_impls(here_idx, goal);

// Push node into the analysis tree.
self.aadebug.push_goal(here_idx, goal).unwrap();

Expand Down
5 changes: 2 additions & 3 deletions ide/packages/common/src/TreeInfo.ts
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import type {
EvaluationResult,
GoalIdx,
GoalKind,
ImplHeader,
ProofNodeIdx,
ResultIdx,
SerializedTree,
Expand Down Expand Up @@ -443,8 +442,8 @@ export class TreeInfo {
return _.min(_.map(hs, TreeInfo.setInertia)) ?? 10_000;
}

public implCandidates(idx: ProofNodeIdx): ImplHeader[] | undefined {
return this.tree.analysis.implCandidates[idx];
public implCandidates(idx: ProofNodeIdx): CandidateIdx[] | undefined {
return this.tree.allImplCandidates[idx];
}
}

Expand Down
2 changes: 2 additions & 0 deletions ide/packages/panoptes/src/TreeView/TopDown.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import _ from "lodash";
import React, { useContext } from "react";

import { DirRecursive } from "./Directory";
import { WrapImplCandidates } from "./Wrappers";

const TopDown = ({ start }: { start?: ProofNodeIdx }) => {
const tree = useContext(TreeAppContext.TreeContext)!;
Expand Down Expand Up @@ -64,6 +65,7 @@ const TopDown = ({ start }: { start?: ProofNodeIdx }) => {
})();

const renderParams: TreeRenderParams = {
Wrappers: [WrapImplCandidates],
styleEdges: true,
...ops
};
Expand Down
9 changes: 3 additions & 6 deletions ide/packages/panoptes/src/TreeView/Wrappers.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import type {
import { TreeAppContext } from "@argus/common/context";
import { arrUpdate } from "@argus/common/func";
import { IcoListUL, IcoTreeDown } from "@argus/print/Icons";
import { PrintImplHeader } from "@argus/print/lib";
import {
FloatingArrow,
FloatingFocusManager,
Expand All @@ -23,6 +22,7 @@ import classNames from "classnames";
import _ from "lodash";
import React, { type ReactElement, useState, useContext, useRef } from "react";
import Graph from "./Graph";
import { Candidate } from "./Node";

import "./Wrappers.css";

Expand Down Expand Up @@ -140,18 +140,15 @@ export const WrapTreeIco = ({ n, reportActive }: InfoWrapperProps) => (
export const WrapImplCandidates = ({ n, reportActive }: InfoWrapperProps) => {
const tree = useContext(TreeAppContext.TreeContext)!;
const candidates = tree.implCandidates(n);

if (candidates === undefined || candidates.length === 0) {
return null;
}
if (candidates === undefined || candidates.length === 0) return null;

return (
<DetailsPortal reportActive={reportActive} info={<IcoListUL />}>
<p>The following {candidates.length} implementations are available:</p>
<div className="ImplCandidatesPanel">
{_.map(candidates, (c, i) => (
<div key={i}>
<PrintImplHeader impl={c} />
<Candidate idx={c} />
</div>
))}
</div>
Expand Down

0 comments on commit f28c069

Please sign in to comment.