From 1a680ed0b9bc4f4bf4ae33687d4cc5b523405fb2 Mon Sep 17 00:00:00 2001 From: Gavin Gray <20209337+gavinleroy@users.noreply.github.com> Date: Mon, 5 Aug 2024 19:04:02 -0600 Subject: [PATCH] Lots'O Goodies (#25) * Add Bottom Up -> Top Down jump and implementors * Typo and using details for Toggle * Highlight jumped to obligations and update GoalKind in aadebug::tree * Force rerender of workspace when jump target changes * Cache panel contents and force rerender on programatic change. * Remove unused ty mod * Remove unused type CandidateImplementors --- crates/argus-ext/src/lib.rs | 2 +- crates/argus-ext/src/rustc/mod.rs | 98 +++--- crates/argus/src/aadebug/dnf.rs | 16 +- crates/argus/src/aadebug/mod.rs | 31 +- crates/argus/src/aadebug/tree.rs | 102 +++++- crates/argus/src/aadebug/ty.rs | 158 ---------- ide/packages/common/src/TreeInfo.ts | 290 +++++++++++++---- ide/packages/common/src/communication.ts | 59 +++- ide/packages/common/src/func.ts | 22 +- ide/packages/extension/src/ctx.ts | 2 +- ide/packages/extension/src/utils.ts | 13 - ide/packages/panoptes/src/App.tsx | 24 +- ide/packages/panoptes/src/Code.css | 6 +- ide/packages/panoptes/src/Expr.tsx | 27 +- ide/packages/panoptes/src/File.css | 6 - ide/packages/panoptes/src/File.tsx | 63 ++-- ide/packages/panoptes/src/FillScreen.tsx | 9 +- ide/packages/panoptes/src/Obligation.tsx | 17 +- .../panoptes/src/TreeView/BottomUp.css | 19 ++ .../panoptes/src/TreeView/BottomUp.tsx | 294 +++++++++++------- .../panoptes/src/TreeView/Directory.tsx | 43 ++- .../panoptes/src/TreeView/Erotisi.tsx | 10 +- .../{Workspace.css => TreeView/Panels.css} | 2 +- ide/packages/panoptes/src/TreeView/Panels.tsx | 153 +++++++++ .../panoptes/src/TreeView/Subsets.css | 19 -- .../panoptes/src/TreeView/Subsets.tsx | 168 ---------- .../panoptes/src/TreeView/TopDown.css | 16 - .../panoptes/src/TreeView/TopDown.tsx | 120 ++----- .../panoptes/src/TreeView/TreeApp.tsx | 106 ++++--- .../panoptes/src/TreeView/Wrappers.css | 36 +++ .../panoptes/src/TreeView/Wrappers.tsx | 170 ++++++++++ .../panoptes/src/TreeView/heuristic.ts | 9 +- ide/packages/panoptes/src/Workspace.tsx | 107 ++++--- ide/packages/panoptes/src/signals.ts | 11 +- ide/packages/print/src/Attention.css | 47 +++ ide/packages/print/src/Attention.tsx | 13 + ide/packages/print/src/Comment.tsx | 2 + ide/packages/print/src/Icons.tsx | 7 +- ide/packages/print/src/Toggle.css | 12 +- ide/packages/print/src/Toggle.tsx | 14 +- ide/packages/print/src/private/ty.tsx | 1 - 41 files changed, 1374 insertions(+), 950 deletions(-) delete mode 100644 crates/argus/src/aadebug/ty.rs rename ide/packages/panoptes/src/{Workspace.css => TreeView/Panels.css} (96%) create mode 100644 ide/packages/panoptes/src/TreeView/Panels.tsx delete mode 100644 ide/packages/panoptes/src/TreeView/Subsets.css delete mode 100644 ide/packages/panoptes/src/TreeView/Subsets.tsx delete mode 100644 ide/packages/panoptes/src/TreeView/TopDown.css create mode 100644 ide/packages/panoptes/src/TreeView/Wrappers.css create mode 100644 ide/packages/panoptes/src/TreeView/Wrappers.tsx create mode 100644 ide/packages/print/src/Attention.css create mode 100644 ide/packages/print/src/Attention.tsx diff --git a/crates/argus-ext/src/lib.rs b/crates/argus-ext/src/lib.rs index 33548b1..66e8495 100644 --- a/crates/argus-ext/src/lib.rs +++ b/crates/argus-ext/src/lib.rs @@ -22,7 +22,7 @@ pub mod iter; // Most of the rustc code is copied from private rustc modules // and it's not worth fixing all the clippy warnings. #[allow(clippy::pedantic)] -mod rustc; +pub mod rustc; pub mod ty; pub mod utils; diff --git a/crates/argus-ext/src/rustc/mod.rs b/crates/argus-ext/src/rustc/mod.rs index 1c6ff1d..04be8ce 100644 --- a/crates/argus-ext/src/rustc/mod.rs +++ b/crates/argus-ext/src/rustc/mod.rs @@ -72,10 +72,10 @@ pub trait InferCtxtExt<'tcx> { error: ty::Predicate<'tcx>, ) -> bool; - // fn find_similar_impl_candidates( - // &self, - // trait_pred: ty::PolyTraitPredicate<'tcx>, - // ) -> Vec>; + fn find_similar_impl_candidates( + &self, + trait_pred: ty::PolyTraitPredicate<'tcx>, + ) -> Vec>; fn fuzzy_match_tys( &self, @@ -219,52 +219,52 @@ impl<'tcx> InferCtxtExt<'tcx> for InferCtxt<'tcx> { } } - // fn find_similar_impl_candidates( - // &self, - // trait_pred: ty::PolyTraitPredicate<'tcx>, - // ) -> Vec> { - // let mut candidates: Vec<_> = self - // .tcx - // .all_impls(trait_pred.def_id()) - // .filter_map(|def_id| { - // let imp = self.tcx.impl_trait_header(def_id).unwrap(); - // if imp.polarity == ty::ImplPolarity::Negative - // || !self.tcx.is_user_visible_dep(def_id.krate) - // { - // return None; - // } - // let imp = imp.trait_ref.skip_binder(); + fn find_similar_impl_candidates( + &self, + trait_pred: ty::PolyTraitPredicate<'tcx>, + ) -> Vec> { + let mut candidates: Vec<_> = self + .tcx + .all_impls(trait_pred.def_id()) + .filter_map(|def_id| { + let imp = self.tcx.impl_trait_header(def_id).unwrap(); + if imp.polarity == ty::ImplPolarity::Negative + || !self.tcx.is_user_visible_dep(def_id.krate) + { + return None; + } + let imp = imp.trait_ref.skip_binder(); - // self - // .fuzzy_match_tys( - // trait_pred.skip_binder().self_ty(), - // imp.self_ty(), - // false, - // ) - // .map(|similarity| ImplCandidate { - // trait_ref: imp, - // similarity, - // impl_def_id: def_id, - // }) - // .or(Some(ImplCandidate { - // trait_ref: imp, - // similarity: CandidateSimilarity::Other, - // impl_def_id: def_id, - // })) - // }) - // .collect(); - // if candidates - // .iter() - // .any(|c| matches!(c.similarity, CandidateSimilarity::Exact { .. })) - // { - // // If any of the candidates is a perfect match, we don't want to show all of them. - // // This is particularly relevant for the case of numeric types (as they all have the - // // same category). - // candidates - // .retain(|c| matches!(c.similarity, CandidateSimilarity::Exact { .. })); - // } - // candidates - // } + self + .fuzzy_match_tys( + trait_pred.skip_binder().self_ty(), + imp.self_ty(), + false, + ) + .map(|similarity| ImplCandidate { + trait_ref: imp, + similarity, + impl_def_id: def_id, + }) + .or(Some(ImplCandidate { + trait_ref: imp, + similarity: CandidateSimilarity::Other, + impl_def_id: def_id, + })) + }) + .collect(); + if candidates + .iter() + .any(|c| matches!(c.similarity, CandidateSimilarity::Exact { .. })) + { + // If any of the candidates is a perfect match, we don't want to show all of them. + // This is particularly relevant for the case of numeric types (as they all have the + // same category). + candidates + .retain(|c| matches!(c.similarity, CandidateSimilarity::Exact { .. })); + } + candidates + } fn fuzzy_match_tys( &self, diff --git a/crates/argus/src/aadebug/dnf.rs b/crates/argus/src/aadebug/dnf.rs index 5374acf..8fb9d9d 100644 --- a/crates/argus/src/aadebug/dnf.rs +++ b/crates/argus/src/aadebug/dnf.rs @@ -1,10 +1,16 @@ +use smallvec::{smallvec, SmallVec}; + +const MAX_CONJUNCTS: usize = 4; + // TODO: this is a very naive implementation, we can certainly make it more efficient. -pub struct And(Vec); +#[derive(Clone)] +pub struct And(SmallVec<[I; MAX_CONJUNCTS]>); + pub struct Dnf(Vec>); impl IntoIterator for And { type Item = I; - type IntoIter = std::vec::IntoIter; + type IntoIter = smallvec::IntoIter<[I; MAX_CONJUNCTS]>; fn into_iter(self) -> Self::IntoIter { self.0.into_iter() @@ -31,8 +37,8 @@ impl And { } impl Dnf { - pub fn into_iter_conjuncts(self) -> impl Iterator> { - self.0.into_iter() + pub fn iter_conjuncts(&self) -> impl Iterator> { + self.0.iter() } pub fn and(vs: impl Iterator) -> Option { @@ -63,7 +69,7 @@ impl Dnf { #[inline] pub fn single(i: I) -> Self { - Self(vec![And(vec![i])]) + Self(vec![And(smallvec![i])]) } #[inline] diff --git a/crates/argus/src/aadebug/mod.rs b/crates/argus/src/aadebug/mod.rs index c167cf8..d37665c 100644 --- a/crates/argus/src/aadebug/mod.rs +++ b/crates/argus/src/aadebug/mod.rs @@ -1,16 +1,17 @@ mod dnf; pub(crate) mod tree; -mod ty; 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; @@ -26,7 +27,13 @@ pub struct Storage<'tcx> { #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export))] pub struct AnalysisResults { - problematic_sets: Vec, + pub problematic_sets: Vec, + + #[cfg_attr( + feature = "testing", + ts(type = "Record") + )] + pub impl_candidates: HashMap>, } impl<'tcx> Storage<'tcx> { @@ -107,27 +114,19 @@ impl<'tcx> Storage<'tcx> { root: ProofNodeIdx, topo: &TreeTopology, ) -> AnalysisResults { - let tree = &tree::T { - root, - ns: &self.ns, - topology: topo, - maybe_ambiguous: false, - }; - + let tree = &tree::T::new(root, &self.ns, topo, false); let tree_start = Instant::now(); - let sets = - tree - .iter_correction_sets() - .fold(Vec::new(), |mut sets, conjunct| { - sets.push(tree.weight(&conjunct)); - sets - }); + let mut sets = vec![]; + tree.for_correction_set(|conjunct| { + sets.push(tree.weight(&conjunct)); + }); timer::elapsed("aadeg::into_results", tree_start); AnalysisResults { problematic_sets: sets, + impl_candidates: tree.reportable_impl_candidates(), } } } diff --git a/crates/argus/src/aadebug/tree.rs b/crates/argus/src/aadebug/tree.rs index 7914d58..54a6267 100644 --- a/crates/argus/src/aadebug/tree.rs +++ b/crates/argus/src/aadebug/tree.rs @@ -1,7 +1,12 @@ -use std::time::Instant; +use std::{cell::RefCell, ops::Deref, time::Instant}; -use argus_ext::ty::{EvaluationResultExt, TyCtxtExt, TyExt}; +use argus_ext::{ + rustc::InferCtxtExt, + ty::{EvaluationResultExt, PredicateExt, TyCtxtExt, TyExt}, +}; +use argus_ser as ser; 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}, @@ -17,6 +22,7 @@ use super::dnf::{And, Dnf}; use crate::{ analysis::EvaluationResult, proof_tree::{topology::TreeTopology, ProofNodeIdx}, + tls, }; pub type I = ProofNodeIdx; @@ -59,6 +65,12 @@ enum GoalKind { FnToTrait { _trait: Location, arity: usize }, TyAsCallable { arity: usize }, DeleteFnParams { delta: usize }, + AddFnParams { delta: usize }, + // Represents a function with the correct number of parameters, + // but the parameters trait bounds or types are unsatisifed. + // TODO if it's worth the extra effort, we could figure out which + // parameters are incorrect and highlight them to the user. + IncorrectParams { arity: usize }, Misc, } @@ -88,7 +100,9 @@ impl GoalKind { } => 2, GK::TyChange => 4, - GK::DeleteFnParams { delta } => 5 * delta, + GK::IncorrectParams { arity: delta } + | GK::AddFnParams { delta } + | GK::DeleteFnParams { delta } => 5 * delta, GK::FnToTrait { _trait: E, arity } // You could implement the unstable Fn traits for a type, // we could thens suggest this if there's nothing else better. @@ -184,8 +198,12 @@ impl<'a, 'tcx> Goal<'a, 'tcx> { GoalKind::DeleteFnParams { delta: fn_arity - trait_arity, } + } else if fn_arity < trait_arity { + GoalKind::AddFnParams { + delta: trait_arity - fn_arity, + } } else { - GoalKind::Misc + GoalKind::IncorrectParams { arity: fn_arity } } } @@ -247,7 +265,7 @@ impl<'a, 'tcx> Goal<'a, 'tcx> { } ty::PredicateKind::Clause(ty::ClauseKind::Trait(t)) => { - log::debug!("Trait Self Ty {:?}", t.self_ty()); + log::warn!("Trait Self Ty {:?} didn't match", t.self_ty()); GoalKind::Misc } @@ -321,9 +339,31 @@ pub struct T<'a, 'tcx: 'a> { pub ns: &'a IndexVec>, pub topology: &'a TreeTopology, pub maybe_ambiguous: bool, + dnf: RefCell>>, } impl<'a, 'tcx: 'a> T<'a, 'tcx> { + pub fn new( + root: I, + ns: &'a IndexVec>, + topology: &'a TreeTopology, + maybe_ambiguous: bool, + ) -> Self { + Self { + root, + ns, + topology, + maybe_ambiguous, + dnf: RefCell::new(None), + } + } + + pub fn for_correction_set(&self, mut f: impl FnMut(&And)) { + for and in self.dnf().iter_conjuncts() { + f(and); + } + } + pub fn goal(&self, i: I) -> Option> { match &self.ns[i] { N::R { @@ -358,7 +398,16 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> { } } - pub fn dnf(&self) -> Dnf { + fn expect_dnf(&self) -> impl Deref> + '_ { + use std::cell::Ref; + Ref::map(self.dnf.borrow(), |o| o.as_ref().expect("dnf")) + } + + pub fn dnf(&self) -> impl Deref> + '_ { + if self.dnf.borrow().is_some() { + return self.expect_dnf(); + } + fn _goal(this: &T, goal: &Goal) -> Option> { if !((this.maybe_ambiguous && goal.result.is_maybe()) || goal.result.is_no()) @@ -395,7 +444,8 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> { let dnf = _goal(self, &root).unwrap_or_else(Dnf::default); timer::elapsed(&dnf_report_msg, dnf_start); - dnf + self.dnf.replace(Some(dnf)); + self.expect_dnf() } /// Failed predicates are weighted as follows. @@ -438,9 +488,41 @@ impl<'a, 'tcx: 'a> T<'a, 'tcx> { } } - #[inline] - pub fn iter_correction_sets(&self) -> impl Iterator> { - self.dnf().into_iter_conjuncts() + pub fn reportable_impl_candidates( + &self, + ) -> HashMap> { + 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() } } diff --git a/crates/argus/src/aadebug/ty.rs b/crates/argus/src/aadebug/ty.rs deleted file mode 100644 index db80108..0000000 --- a/crates/argus/src/aadebug/ty.rs +++ /dev/null @@ -1,158 +0,0 @@ -// use rustc_infer::infer::InferCtxt; -// use rustc_middle::{ -// traits::solve::Goal, -// ty::{ -// self, fold::BottomUpFolder, Predicate, Ty, TyCtxt, TypeFoldable, -// TypeVisitableExt, Upcast, -// }, -// }; - -// use crate::{analysis::EvaluationResult, rustc::ImplCandidate}; - -// #[derive(Debug)] -// pub struct ImplementorInfo<'tcx> { -// implementor: ty::TraitRef<'tcx>, -// terrs: Vec>, -// } - -// pub trait InferCtxtEvalExt<'tcx> { -// fn eval_goal( -// &self, -// obligation: Goal<'tcx, Predicate<'tcx>>, -// ) -> EvaluationResult; - -// fn eval_with_self( -// &self, -// self_ty: Ty<'tcx>, -// trait_ref: ty::PolyTraitRef<'tcx>, -// param_env: ty::ParamEnv<'tcx>, -// ) -> EvaluationResult; - -// fn find_implementing_type( -// &self, -// single: &ImplCandidate<'tcx>, -// trait_ref: ty::PolyTraitRef<'tcx>, -// param_env: ty::ParamEnv<'tcx>, -// ) -> Option>; -// } - -// impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> { -// fn eval_goal( -// &self, -// obligation: Goal<'tcx, Predicate<'tcx>>, -// ) -> EvaluationResult { -// use rustc_trait_selection::{ -// solve::{GenerateProofTree, InferCtxtEvalExt}, -// traits::query::NoSolution, -// }; -// self.probe(|_| { -// match self -// .evaluate_root_goal(obligation.clone().into(), GenerateProofTree::Never) -// .0 -// { -// Ok((_, c)) => Ok(c), -// _ => Err(NoSolution), -// } -// }) -// } - -// fn eval_with_self( -// &self, -// self_ty: Ty<'tcx>, -// trait_ref: ty::PolyTraitRef<'tcx>, -// param_env: ty::ParamEnv<'tcx>, -// ) -> EvaluationResult { -// let tp = trait_ref.map_bound(|tp| tp.with_self_ty(self.tcx, self_ty)); -// let goal = Goal { -// predicate: tp.upcast(self.tcx), -// param_env, -// }; -// self.eval_goal(goal) -// } - -// fn find_implementing_type( -// &self, -// single: &ImplCandidate<'tcx>, -// trait_ref: ty::PolyTraitRef<'tcx>, -// param_env: ty::ParamEnv<'tcx>, -// ) -> Option> { -// use rustc_span::DUMMY_SP; -// use rustc_trait_selection::traits::{ -// Obligation, ObligationCause, ObligationCtxt, -// }; -// self.probe(|_| { -// let ocx = ObligationCtxt::new(self); -// let fresh_ty_var = self.next_ty_var(rustc_span::DUMMY_SP); -// let fresh_trait_ref = trait_ref -// .rebind(trait_ref.skip_binder().with_self_ty(self.tcx, fresh_ty_var)); - -// self.enter_forall(fresh_trait_ref, |obligation_trait_ref| { -// let impl_args = self.fresh_args_for_item(DUMMY_SP, single.impl_def_id); -// let impl_trait_ref = ocx.normalize( -// &ObligationCause::dummy(), -// param_env, -// ty::EarlyBinder::bind(single.trait_ref) -// .instantiate(self.tcx, impl_args), -// ); - -// ocx.register_obligations( -// self -// .tcx -// .predicates_of(single.impl_def_id) -// .instantiate(self.tcx, impl_args) -// .into_iter() -// .map(|(clause, _)| { -// Obligation::new( -// self.tcx, -// ObligationCause::dummy(), -// param_env, -// clause, -// ) -// }), -// ); - -// if !ocx.select_where_possible().is_empty() { -// return None; -// } - -// let mut terrs = vec![]; -// for (obligation_arg, impl_arg) in -// std::iter::zip(obligation_trait_ref.args, impl_trait_ref.args) -// { -// if (obligation_arg, impl_arg).references_error() { -// return None; -// } -// if let Err(terr) = ocx.eq( -// &ObligationCause::dummy(), -// param_env, -// impl_arg, -// obligation_arg, -// ) { -// terrs.push(terr); -// } -// if !ocx.select_where_possible().is_empty() { -// return None; -// } -// } - -// let cand = self.resolve_vars_if_possible(impl_trait_ref).fold_with( -// &mut BottomUpFolder { -// tcx: self.tcx, -// ty_op: |ty| ty, -// lt_op: |lt| lt, -// ct_op: |ct| ct.normalize(self.tcx, ty::ParamEnv::empty()), -// }, -// ); - -// if cand.references_error() { -// return None; -// } - -// Some(ImplementorInfo { -// implementor: cand, -// terrs, -// }) -// }) -// }) -// } -// } diff --git a/ide/packages/common/src/TreeInfo.ts b/ide/packages/common/src/TreeInfo.ts index 3024390..feaef1d 100644 --- a/ide/packages/common/src/TreeInfo.ts +++ b/ide/packages/common/src/TreeInfo.ts @@ -5,21 +5,67 @@ import type { CandidateIdx, EvaluationResult, GoalIdx, + GoalKind, + ImplHeader, ProofNodeIdx, ResultIdx, SerializedTree, + SetHeuristic, TreeTopology } from "./bindings"; +export type TreeViewWithRoot = TreeView & { root: ProofNodeIdx }; + +export interface TreeView { + topology: TreeTopology; + underlying?: TreeView; +} + type MultiRecord = Record; type Direction = "to-root" | "from-root"; -interface Path { - from: T; - to: T; - path: T[]; - d: D; +type Reverse = T extends "to-root" + ? "from-root" + : "to-root"; + +function reverseDirection(d: Direction): Reverse { + // HACK: ugh, get rid of the `any` here. + return d === "to-root" ? "from-root" : ("to-root" as any); +} + +class Path { + constructor( + private readonly from: T, + private readonly to: T, + private readonly path: T[], + private readonly d: D + ) { + if (_.first(path) !== from) { + throw new Error("Path does not start from the `from` node"); + } + + if (_.last(path) !== to) { + throw new Error("Path does not end at the `to` node"); + } + } + + get pathInclusive() { + return this.path; + } + + get length() { + return this.path.length; + } + + reverse(): Path> { + return new Path( + this.to, + this.from, + _.reverse(this.path), + reverseDirection(this.d) + ); + } } function makeTreeView( @@ -70,12 +116,116 @@ function makeTreeView( } } -export interface TreeView { - topology: TreeTopology; - underlying?: TreeView; +type ControlFlow = "keep" | "remove-tree" | "remove-node"; + +class TopologyBuilder { + private topo: TreeTopology; + constructor( + readonly root: ProofNodeIdx, + readonly tree: TreeInfo + ) { + this.topo = { children: {}, parent: {} }; + } + + public toView(): TreeViewWithRoot { + return { topology: this.topo, root: this.root }; + } + + get topology() { + return this.topo; + } + + add(from: ProofNodeIdx, to: ProofNodeIdx) { + if (this.topo.children[from] === undefined) { + this.topo.children[from] = []; + } + this.topo.children[from].push(to); + this.topo.parent[to] = from; + } + + /** + * + * @param root the root node from where this path should start. + * @param path a path to be added uniquely to the tree. + */ + public addPathFromRoot(path: ProofNodeIdx[]) { + const thisRoot = _.head(path); + if ( + thisRoot === undefined || + !_.isEqual(this.tree.node(thisRoot), this.tree.node(this.root)) + ) { + throw new Error("Path does not start from the root"); + } + + let previous = this.root; + _.forEach(_.tail(path), node => { + // We want to add a node from `previous` to `node` only if an + // equivalent connection does not already exist. Equivalent is + // defined by the `Node` the `ProofNodeIdx` points to. + const currKids = this.topo.children[previous] ?? []; + const myNode = this.tree.node(node); + const hasEquivalent = _.find( + currKids, + kid => this.tree.node(kid) === myNode + ); + if (hasEquivalent === undefined) { + this.add(previous, node); + previous = node; + } else { + previous = hasEquivalent; + } + }); + } } -type ControlFlow = "keep" | "remove-tree" | "remove-node"; +/** + * Invert the current `TreeView` on the `TreeInfo`, using `leaves` as the roots. + * For the purpose of inverting a tree anchored at failed goals, some of these goals will + * be 'distinct' nodes, but their inner `GoalIdx` will be the same. We want to root all of + * these together. + */ +export function invertViewWithRoots( + leaves: ProofNodeIdx[], + tree: TreeInfo +): TreeViewWithRoot[] { + const groups: ProofNodeIdx[][] = _.values( + _.groupBy(leaves, leaf => { + const node = tree.node(leaf); + if ("Goal" in node) { + return node.Goal; + } + throw new Error("Leaves must be goals"); + }) + ); + + return _.map(groups, group => { + // Each element of the group is equivalent, so just take the first + const builder = new TopologyBuilder(group[0], tree); + + // Get the paths to the root from all leaves, filter paths that + // contain successful nodes. + const pathsToRoot = _.map( + group, + parent => tree.pathToRoot(parent).pathInclusive + ); + + _.forEach(pathsToRoot, path => { + // No need to take the tail, `addPathFromRoot` checks that the + // roots are equal and then skips the first element. + builder.addPathFromRoot(path); + }); + + return builder.toView(); + }); +} + +function isBadUnification(kind: GoalKind) { + return ( + kind.type === "DeleteFnParams" || + kind.type === "AddFnParams" || + kind.type === "IncorrectParams" + ); +} export class TreeInfo { private _maxHeight: Map; @@ -95,7 +245,7 @@ export class TreeInfo { const goalData = tree.goals[node.Goal]; const result = tree.results[goalData.result]; return "keep"; - // FIXME: I think this logic is correct...but when enabled argus crashes. + // FIXME: I belive that this logic is correct, but argus crashes when enabled // return isHiddenObl({ necessity: goalData.necessity, result }) // ? "remove-tree" // : "remove-node"; @@ -113,7 +263,7 @@ export class TreeInfo { } } - constructor( + private constructor( private readonly tree: SerializedTree, readonly showHidden: boolean, readonly view: TreeView @@ -130,12 +280,54 @@ export class TreeInfo { return this.tree.root; } + public failedSets() { + if (this.showHidden) return this.tree.analysis.problematicSets; + + // If all the problematic sets involve a bad unification, then we + // have to live with them, don't filter. + if ( + _.every(this.tree.analysis.problematicSets, s => + _.some(s.goals, g => isBadUnification(g.kind)) + ) + ) + return this.tree.analysis.problematicSets; + + // Keep only the sets that don't have a bad unification + return _.filter(this.tree.analysis.problematicSets, s => + _.every(s.goals, g => !isBadUnification(g.kind)) + ); + } + + private unificationFailures(): ProofNodeIdx[] { + const goals = _.flatMap(this.tree.analysis.problematicSets, s => s.goals); + return _.map( + _.filter(goals, g => isBadUnification(g.kind)), + g => g.idx + ); + } + + private nodesInUnificationFailurePath(): ProofNodeIdx[] { + if (this.showHidden) return []; + + const nonUnificationFailures = _.flatMap( + _.flatMap(this.failedSets(), s => _.map(s.goals, g => g.idx)), + n => this.pathToRoot(n).pathInclusive + ); + + const uFs = _.flatMap( + this.unificationFailures(), + n => this.pathToRoot(n).pathInclusive + ); + + return _.difference(uFs, nonUnificationFailures); + } + public node(n: ProofNodeIdx) { return this.tree.nodes[n]; } public depth(n: ProofNodeIdx) { - return this.pathToRoot(n).path.length; + return this.pathToRoot(n).length; } public goalOfNode(n: ProofNodeIdx) { @@ -156,7 +348,16 @@ export class TreeInfo { } public children(n: ProofNodeIdx): ProofNodeIdx[] { - return this.view.topology.children[n] ?? []; + const nodesToUnifyFailures = this.nodesInUnificationFailurePath(); + + // if (_.includes(nodesToUnifyFailures, 6222)) { + // throw new Error("NODE NOT THERE"); + // } else { + // console.debug("Nodes to unify failures includes 6222"); + // } + + const children = this.view.topology.children[n] ?? []; + return _.difference(children, nodesToUnifyFailures); } public result(n: ResultIdx): EvaluationResult { @@ -190,47 +391,11 @@ export class TreeInfo { current = parent; } - return { - from, - to: this.root, - path, - d: "to-root" - }; + return new Path(from, this.root, path, "to-root"); } public pathFromRoot(from: ProofNodeIdx): Path { - let { from: f, to, path } = this.pathToRoot(from); - return { - from: to, - to: f, - path: _.reverse(path), - d: "from-root" - }; - } - - public errorLeaves(): ProofNodeIdx[] { - if (this.nodeResult(this.root) === "yes") { - return []; - } - - let errorLeaves = []; - let stack = [this.root]; - while (stack.length > 0) { - const current = stack.pop()!; - const children = this.children(current); - if (children.length === 0 && this.nodeResult(current) !== "yes") { - const node = this.node(current); - if ("Result" in node) { - errorLeaves.push(current); - } else { - console.error("Node has no children but isn't a leaf", node); - } - } else { - const errorKids = _.filter(children, n => this.nodeResult(n) !== "yes"); - stack.push(...errorKids); - } - } - return errorLeaves; + return this.pathToRoot(from).reverse(); } public inferVars(n: ProofNodeIdx): number { @@ -259,8 +424,27 @@ export class TreeInfo { return height; } - get failedSets() { - return this.tree.analysis.problematicSets; + /** + * Define the heuristic used for inertia in the system. Previously we were + * using `momentum / velocity` but this proved too sporatic. Some proof trees + * were deep, needlessely, and this threw a wrench in the order. + */ + public static setInertia = (set: SetHeuristic) => { + return set.momentum; + }; + + public minInertiaOnPath(n: ProofNodeIdx): number { + const hs = _.filter(this.failedSets(), h => + _.some(h.goals, g => _.includes(this.pathToRoot(g.idx).pathInclusive, n)) + ); + + // HACK: the high default is a hack to get rid of undefined, + // but it should never be undefined. + return _.min(_.map(hs, TreeInfo.setInertia)) ?? 10_000; + } + + public implCandidates(idx: ProofNodeIdx): ImplHeader[] | undefined { + return this.tree.analysis.implCandidates[idx]; } } diff --git a/ide/packages/common/src/communication.ts b/ide/packages/common/src/communication.ts index dbc7369..d31377a 100644 --- a/ide/packages/common/src/communication.ts +++ b/ide/packages/common/src/communication.ts @@ -10,44 +10,70 @@ import { isPanoMsgTree } from "./lib"; -export type InfoWrapper = React.FC<{ +export type InfoWrapperProps = { n: ProofNodeIdx; - Child: React.ReactElement; -}>; + reportActive: (b: boolean) => void; +}; + +export type InfoWrapper = React.FC; + export interface TreeRenderParams { - Wrapper?: InfoWrapper; + Wrappers?: InfoWrapper[]; styleEdges?: boolean; + startOpenP?: (n: ProofNodeIdx) => boolean; + onMount?: () => void; } export interface MessageSystem { - postData(body: PanoptesToSystemMsg): void; + postData( + command: T, + body: Omit, "command"> + ): void; requestData( - body: PanoptesToSystemMsg + command: T, + body: Omit, "command"> ): Promise>; } export const vscodeMessageSystem: MessageSystem = { - postData(body: PanoptesToSystemMsg) { - return messageHandler.send(body.command, body); + postData( + command: T, + body: Omit, "command"> + ) { + return messageHandler.send(command, { command, ...body }); }, - requestData(body: PanoptesToSystemMsg) { - return messageHandler.request>(body.command, body); + requestData( + command: T, + body: Omit, "command"> + ): Promise> { + return messageHandler.request>(command, { + command, + ...body + }); } }; export function createClosedMessageSystem(bodies: BodyBundle[]): MessageSystem { const systemMap = _.groupBy(bodies, bundle => bundle.filename); return { - postData(_body: PanoptesToSystemMsg) { + postData( + _command: T, + _body: Omit, "command"> + ) { // Intentionally blank, no system to post to. }, - requestData(body: PanoptesToSystemMsg) { + requestData( + command: T, + bodyOmit: Omit, "command"> + ) { return new Promise>((resolve, reject) => { + const body = { command, ...bodyOmit }; + if (!isPanoMsgTree(body)) { - return reject(new Error(`"Invalid message type" ${body.command}`)); + return reject(new Error(`"Invalid message type" ${command}`)); } const rangesInFile = systemMap[body.file]; @@ -71,7 +97,12 @@ export function createClosedMessageSystem(bodies: BodyBundle[]): MessageSystem { ) ); if (tree === undefined) { - console.error("Body", foundBodies, "hash", body.predicate.hash); + console.error( + "Tree not found in bodies", + foundBodies, + "hash", + body.predicate.hash + ); return reject(new Error("Obligation hash not found in maps")); } diff --git a/ide/packages/common/src/func.ts b/ide/packages/common/src/func.ts index 6e44535..ae81a5e 100644 --- a/ide/packages/common/src/func.ts +++ b/ide/packages/common/src/func.ts @@ -15,6 +15,9 @@ import type { import type { MessageSystem } from "./communication"; import type { Filename } from "./lib"; +export const arrUpdate = (arr: T[], idx: number, val: T) => + _.map(arr, (v, i) => (i !== idx ? v : val)); + export function isObject(x: any): x is object { return typeof x === "object" && x !== null; } @@ -44,19 +47,17 @@ export function makeHighlightPosters( file: Filename ) { const addHighlight = () => { - messageSystem.postData({ + messageSystem.postData("add-highlight", { type: "FROM_WEBVIEW", file, - command: "add-highlight", range }); }; const removeHighlight = () => { - messageSystem.postData({ + messageSystem.postData("remove-highlight", { type: "FROM_WEBVIEW", file, - command: "remove-highlight", range }); }; @@ -180,3 +181,16 @@ export function isNamedBoundVariable(bv: BoundVariableKind) { return false; } + +export function makeid(length = 16) { + let result = ""; + const characters = + "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"; + const charactersLength = characters.length; + let counter = 0; + while (counter < length) { + result += characters.charAt(Math.floor(Math.random() * charactersLength)); + counter += 1; + } + return result; +} diff --git a/ide/packages/extension/src/ctx.ts b/ide/packages/extension/src/ctx.ts index 4745795..fdc3d6f 100644 --- a/ide/packages/extension/src/ctx.ts +++ b/ide/packages/extension/src/ctx.ts @@ -8,6 +8,7 @@ import type { ObligationsInBody, SerializedTree } from "@argus/common/bindings"; +import { makeid } from "@argus/common/func"; import type { CallArgus, ErrorJumpTargetInfo, @@ -27,7 +28,6 @@ import { isDocumentInWorkspace, isRustDocument, isRustEditor, - makeid, rustRangeToVscodeRange } from "./utils"; import { View } from "./view"; diff --git a/ide/packages/extension/src/utils.ts b/ide/packages/extension/src/utils.ts index 937679f..794eeca 100644 --- a/ide/packages/extension/src/utils.ts +++ b/ide/packages/extension/src/utils.ts @@ -4,19 +4,6 @@ import vscode from "vscode"; export type RustDocument = vscode.TextDocument & { languageId: "rust" }; export type RustEditor = vscode.TextEditor & { document: RustDocument }; -export function makeid(length: number) { - let result = ""; - const characters = - "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"; - const charactersLength = characters.length; - let counter = 0; - while (counter < length) { - result += characters.charAt(Math.floor(Math.random() * charactersLength)); - counter += 1; - } - return result; -} - export function isRustDocument( document: vscode.TextDocument ): document is RustDocument { diff --git a/ide/packages/panoptes/src/App.tsx b/ide/packages/panoptes/src/App.tsx index 88ce840..07a3188 100644 --- a/ide/packages/panoptes/src/App.tsx +++ b/ide/packages/panoptes/src/App.tsx @@ -5,7 +5,6 @@ import { } from "@argus/common/communication"; import { AppContext } from "@argus/common/context"; import { - type ErrorJumpTargetInfo, type EvaluationMode, type FileInfo, type PanoptesConfig, @@ -39,13 +38,7 @@ import { PrintTyValue } from "@argus/print/lib"; import classNames from "classnames"; import MiniBuffer from "./MiniBuffer"; import Workspace from "./Workspace"; -import { MiniBufferDataStore, highlightedObligation } from "./signals"; - -function blingObserver(info: ErrorJumpTargetInfo) { - console.debug(`Highlighting obligation ${info}`); - highlightedObligation.set(info); - return setTimeout(() => highlightedObligation.reset(), 1500); -} +import { HighlightTargetStore, MiniBufferDataStore } from "./signals"; const webSysSpec: SystemSpec = { osPlatform: "web-bundle", @@ -84,7 +77,7 @@ function listener( console.debug("Received message from system", payload); if (isSysMsgOpenError(payload)) { - return blingObserver(payload); + return HighlightTargetStore.set(payload); } else if (isSysMsgOpenFile(payload)) { return setOpenFiles(currFiles => { const newEntry = { @@ -148,9 +141,8 @@ const mkLocationActionable = if (selectKeys(event)) { event.preventDefault(); event.stopPropagation(); - system.postData({ + system.postData("jump-to-def", { type: "FROM_WEBVIEW", - command: "jump-to-def", location }); } @@ -247,13 +239,17 @@ const App = observer(({ config }: { config: PanoptesConfig }) => { () => MiniBufferDataStore.pin(), () => MiniBufferDataStore.unpin() ); + window.addEventListener("message", listen); - if (config.target !== undefined) { - blingObserver(config.target); - } return () => window.removeEventListener("message", listen); }, []); + useEffect(() => { + if (config.target !== undefined) { + HighlightTargetStore.set(config.target); + } + }, [config.target]); + const Navbar = ( <>
diff --git a/ide/packages/panoptes/src/Code.css b/ide/packages/panoptes/src/Code.css index cbf061d..5632c63 100644 --- a/ide/packages/panoptes/src/Code.css +++ b/ide/packages/panoptes/src/Code.css @@ -1,6 +1,6 @@ pre.shiki { /* Shiki sets a background color inline, we need to override it. */ - background-color: var(--background) !important; + background-color: transparent!important; /* Make the default element inline (to use as directory label) */ display: inline; @@ -9,15 +9,15 @@ pre.shiki { /* The code should always blend in with the view panel */ .shiki code { + background-color: transparent; font-family: var(--vscode-editor-font-family); - background-color: var(--background); } /* Change the code colors based on VSCode exported body classes */ body.vscode-dark .shiki, body.vscode-dark .shiki span { color: var(--shiki-dark) !important; - background-color: var(--shiki-dark-bg) !important; + background-color: transparent !important; /* Optional, if you also want font styles */ font-style: var(--shiki-dark-font-style) !important; font-weight: var(--shiki-dark-font-weight) !important; diff --git a/ide/packages/panoptes/src/Expr.tsx b/ide/packages/panoptes/src/Expr.tsx index 3104d4a..95099d2 100644 --- a/ide/packages/panoptes/src/Expr.tsx +++ b/ide/packages/panoptes/src/Expr.tsx @@ -5,20 +5,14 @@ import { FileContext } from "@argus/common/context"; import { makeHighlightPosters } from "@argus/common/func"; -import classNames from "classnames"; import _ from "lodash"; import { observer } from "mobx-react"; import React, { useContext } from "react"; - import Code from "./Code"; import { ObligationFromIdx } from "./Obligation"; import { CollapsibleElement } from "./TreeView/Directory"; -import { highlightedObligation } from "./signals"; +import { HighlightTargetStore } from "./signals"; -/** - * Expression-level obligations within a `File`. Expects that - * the `BodyInfoContext` is available. - */ const Expr = observer(({ idx }: { idx: ExprIdx }) => { const bodyInfo = useContext(BodyInfoContext)!; const file = useContext(FileContext)!; @@ -44,24 +38,13 @@ const Expr = observer(({ idx }: { idx: ExprIdx }) => { )); - // TODO: we should limit the length of the expression snippet. - // or at the very least syntax highlight it in some way... - // I think there should be a better way to represent this information than a blank expr. - const header = ; + const openChildren = idx === HighlightTargetStore.value?.exprIdx; - const openChildren = idx === highlightedObligation.value?.exprIdx; - // If there is no targeted obligation then we want to highlight - // the expression level div. - const className = classNames({ - bling: highlightedObligation.value && !highlightedObligation.value.hash - }); + // TODO: we should limit the length of the expression snippet or collapse large blocks in some way. + const header = ; return ( -
+
ƒ; +const fnIndicator = ƒ; const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => { if (!bodyInfo.hasVisibleExprs()) { @@ -43,7 +43,7 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => { const header = ( <> - + {fnIndicator} {"\u00A0"} {bodyName} @@ -51,50 +51,33 @@ const ObligationBody = observer(({ bodyInfo }: { bodyInfo: BodyInfo }) => { ); - const openChildren = bodyInfo.hash === highlightedObligation.value?.bodyIdx; + const Kids = () => + _.map(bodyInfo.exprs(), (i, idx) => ); + + const openChildren = bodyInfo.hash === HighlightTargetStore.value?.bodyIdx; return ( - _.map(bodyInfo.exprs(), (i, idx) => ) - } + Children={Kids} /> ); }); -const File = ({ - file, - osibs -}: { +export interface FileProps { file: Filename; osibs: ObligationsInBody[]; -}) => { +} + +const File = ({ file, osibs }: FileProps) => { const showHidden = useContext(AppContext.ShowHiddenObligationsContext); const bodyInfos = _.map( osibs, (osib, idx) => new BodyInfo(osib, idx, showHidden) ); - const bodiesWithVisibleExprs = _.filter(bodyInfos, bi => - bi.hasVisibleExprs() - ); - - const bodies = _.map(bodiesWithVisibleExprs, (bodyInfo, idx) => ( - - {idx > 0 ? : null} - - - - - )); const noBodiesFound = ( @@ -109,9 +92,29 @@ const File = ({ ); + const bodiesWithVisibleExprs = _.filter(bodyInfos, bi => + bi.hasVisibleExprs() + ); + + if (bodiesWithVisibleExprs.length === 0) { + return noBodiesFound; + } + return ( - {bodies.length > 0 ? bodies : noBodiesFound} + {_.map(bodiesWithVisibleExprs, (bodyInfo, idx) => ( + + {idx > 0 ? : null} + + + + + ))} ); }; diff --git a/ide/packages/panoptes/src/FillScreen.tsx b/ide/packages/panoptes/src/FillScreen.tsx index de6f72c..dc183bc 100644 --- a/ide/packages/panoptes/src/FillScreen.tsx +++ b/ide/packages/panoptes/src/FillScreen.tsx @@ -1,4 +1,3 @@ -import _ from "lodash"; import React, { useState, useEffect } from "react"; import "./FillScreen.css"; @@ -32,11 +31,9 @@ export const Spacer = () =>
{"\u00A0"}
; const FillScreen = () => { const { height } = useWindowDimensions(); - // FIXME: this assumes that nobody is using a `font-size` smaller than 14. - // A better approach would be to make the height of the spacing div 80% of - // the screen height and then width 100%. Probably easier than the loop anyways. - const fontSize = 14; - return _.map(_.range(height / fontSize), i => ); + // 75% of the screen height means there is always *something* visible, + // and the user can almost scroll the contents to the top of the view. + return
; }; export default FillScreen; diff --git a/ide/packages/panoptes/src/Obligation.tsx b/ide/packages/panoptes/src/Obligation.tsx index c4295cf..9a03c7f 100644 --- a/ide/packages/panoptes/src/Obligation.tsx +++ b/ide/packages/panoptes/src/Obligation.tsx @@ -10,7 +10,6 @@ import { makeHighlightPosters, obligationCardId } from "@argus/common/func"; import ErrorDiv from "@argus/print/ErrorDiv"; import ReportBugUrl from "@argus/print/ReportBugUrl"; import { PrintObligation } from "@argus/print/lib"; -import classNames from "classnames"; import { observer } from "mobx-react"; import React, { useContext, @@ -25,7 +24,7 @@ import { CollapsibleElement } from "./TreeView/Directory"; import { ResultRaw } from "./TreeView/Node"; import TreeApp from "./TreeView/TreeApp"; import { WaitingOn } from "./WaitingOn"; -import { highlightedObligation } from "./signals"; +import { HighlightTargetStore } from "./signals"; export const ObligationFromIdx = ({ idx }: { idx: ObligationIdx }) => { const bodyInfo = useContext(BodyInfoContext)!; @@ -79,10 +78,9 @@ const ProofTreeWrapper = ({ useEffect(() => { const getData = async () => { - const tree = await messageSystem.requestData<"tree">({ + const tree = await messageSystem.requestData("tree", { type: "FROM_WEBVIEW", file: file, - command: "tree", predicate: obligation, range: range }); @@ -119,21 +117,18 @@ const Obligation = observer( ); const isTargetObligation = - highlightedObligation.value?.hash === obligation.hash; - const className = classNames("ObligationCard", { - bling: isTargetObligation - }); + HighlightTargetStore.value?.hash === obligation.hash; useLayoutEffect(() => { - if (highlightedObligation.value?.hash === obligation.hash) { + if (isTargetObligation) { ref.current?.scrollIntoView({ behavior: "smooth" }); } - }, []); + }, [isTargetObligation]); const header = (
i { + position: absolute; + top: 0; + right: 0; + + font-size: 0.25em; +} \ No newline at end of file diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index bd8251f..dc0e2e4 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx @@ -1,116 +1,28 @@ -import type { TreeInfo, TreeView } from "@argus/common/TreeInfo"; -import type { ProofNodeIdx, TreeTopology } from "@argus/common/bindings"; -import type { TreeRenderParams } from "@argus/common/communication"; -import { TreeAppContext } from "@argus/common/context"; import type { EvaluationMode } from "@argus/common/lib"; import { PrintGoal } from "@argus/print/lib"; -import _ from "lodash"; -import React, { useContext } from "react"; +import React, { useContext, useState } from "react"; import { flushSync } from "react-dom"; import { createRoot } from "react-dom/client"; -import "./BottomUp.css"; -import { CollapsibleElement, DirRecursive } from "./Directory"; - -export type TreeViewWithRoot = TreeView & { root: ProofNodeIdx }; - -class TopologyBuilder { - private topo: TreeTopology; - constructor( - readonly root: ProofNodeIdx, - readonly tree: TreeInfo - ) { - this.topo = { children: {}, parent: {} }; - } - - public toView(): TreeViewWithRoot { - return { topology: this.topo, root: this.root }; - } - - get topology() { - return this.topo; - } - - add(from: ProofNodeIdx, to: ProofNodeIdx) { - if (this.topo.children[from] === undefined) { - this.topo.children[from] = []; - } - this.topo.children[from].push(to); - this.topo.parent[to] = from; - } - - /** - * - * @param root the root node from where this path should start. - * @param path a path to be added uniquely to the tree. - */ - public addPathFromRoot(path: ProofNodeIdx[]) { - const thisRoot = _.head(path); - if ( - thisRoot === undefined || - !_.isEqual(this.tree.node(thisRoot), this.tree.node(this.root)) - ) { - throw new Error("Path does not start from the root"); - } - - let previous = this.root; - _.forEach(_.tail(path), node => { - // We want to add a node from `previous` to `node` only if an - // equivalent connection does not already exist. Equivalent is - // defined by the `Node` the `ProofNodeIdx` points to. - const currKids = this.topo.children[previous] ?? []; - const myNode = this.tree.node(node); - const hasEquivalent = _.find( - currKids, - kid => this.tree.node(kid) === myNode - ); - if (hasEquivalent === undefined) { - this.add(previous, node); - previous = node; - } else { - previous = hasEquivalent; - } - }); - } -} - -/** - * Invert the current `TreeView` on the `TreeInfo`, using `leaves` as the roots. - * For the purpose of inverting a tree anchored at failed goals, some of these goals will - * be 'distinct' nodes, but their inner `GoalIdx` will be the same. We want to root all of - * these together. - */ -export function invertViewWithRoots( - leaves: ProofNodeIdx[], - tree: TreeInfo -): TreeViewWithRoot[] { - const groups: ProofNodeIdx[][] = _.values( - _.groupBy(leaves, leaf => { - const node = tree.node(leaf); - if ("Goal" in node) { - return node.Goal; - } - throw new Error("Leaves must be goals"); - }) - ); - - return _.map(groups, group => { - // Each element of the group is equivalent, so just take the first - const builder = new TopologyBuilder(group[0], tree); - - // Get the paths to the root from all leaves, filter paths that - // contain successful nodes. - const pathsToRoot = _.map(group, parent => tree.pathToRoot(parent).path); +import type { ProofNodeIdx, SetHeuristic } from "@argus/common/bindings"; +import type { TreeRenderParams } from "@argus/common/communication"; +import { AppContext, TreeAppContext } from "@argus/common/context"; +import classNames from "classnames"; +import _ from "lodash"; +import { observer } from "mobx-react"; +import { MiniBufferDataStore } from "../signals"; - _.forEach(pathsToRoot, path => { - // No need to take the tail, `addPathFromRoot` checks that the - // roots are equal and then skips the first element. - builder.addPathFromRoot(path); - }); +import { + TreeInfo, + type TreeView, + type TreeViewWithRoot, + invertViewWithRoots +} from "@argus/common/TreeInfo"; +import { IcoComment } from "@argus/print/Icons"; +import { WrapImplCandidates, mkJumpToTopDownWrapper } from "./Wrappers"; - return builder.toView(); - }); -} +import { CollapsibleElement, DirRecursive } from "./Directory"; +import "./BottomUp.css"; const RenderEvaluationViews = ({ recommended, @@ -161,17 +73,6 @@ const RenderEvaluationViews = ({ ); }; -export const BottomUpRenderParams: TreeRenderParams = { - Wrapper: ({ - n: _n, - Child - }: { - n: ProofNodeIdx; - Child: React.ReactElement; - }) => Child, - styleEdges: false -}; - /** * The actual entry point for rendering the bottom up view. All others are used in testing or evaluation. */ @@ -200,10 +101,10 @@ export const RenderBottomUpViews = ({ ); return ( - + <> {fallbacks} - + ); }; @@ -239,3 +140,158 @@ export const BottomUpImpersonator = ({ /> ); }; + +export const sortedSubsets = (sets: SetHeuristic[]) => + _.sortBy(sets, TreeInfo.setInertia); + +const mkGetChildren = (view: TreeView) => (idx: ProofNodeIdx) => + view.topology.children[idx] ?? []; + +const GroupedFailures = observer( + (views: { + tree: TreeViewWithRoot[]; + inertia: number; + momentum: number; + velocity: number; + }) => { + if (views.tree.length === 0) { + return null; + } + + const [hovered, setHovered] = useState(false); + const cn = classNames("FailingSet", { "is-hovered": hovered }); + + // If there is only a single predicate, no need to provide all the + // extra information around "grouped predicate sets". + if (views.tree.length === 1) { + return ( +
+ +
+ ); + } + + const onHover = () => { + MiniBufferDataStore.set({ + kind: "argus-note", + data: ( +

+ The outlined obligations must be resolved together +

+ ) + }); + setHovered(true); + }; + + const onNoHover = () => { + MiniBufferDataStore.reset(); + setHovered(false); + }; + + return ( +
+ + {_.map(views.tree, (leaf, i) => ( + + ))} +
+ ); + } +); + +export const RenderBottomUpSets = ({ + views, + jumpTo +}: { + jumpTo: (n: ProofNodeIdx) => void; + views: { + tree: TreeViewWithRoot[]; + inertia: number; + velocity: number; + momentum: number; + }[]; +}) => { + const argusRecommends = ; + const tail = _.tail(views); + + const otherLabel = "Other failures"; + const fallbacks = + tail.length === 0 ? null : ( + {otherLabel} ...} + Children={() => + _.map(tail, (v, i) => ) + } + /> + ); + + const SubsetRenderParams: TreeRenderParams = { + Wrappers: [WrapImplCandidates, mkJumpToTopDownWrapper(jumpTo)], + styleEdges: false + }; + + return ( + +

+ Argus recommends investigating these failed obligations. Click on ’ + {otherLabel}‘ below to see other failed obligations. +

+ + {fallbacks} + + ); +}; + +const BottomUp = ({ + jumpToTopDown +}: { jumpToTopDown: (n: ProofNodeIdx) => void }) => { + const tree = useContext(TreeAppContext.TreeContext)!; + const evaluationMode = + useContext(AppContext.ConfigurationContext)?.evalMode ?? "release"; + const sets = sortedSubsets(tree.failedSets()); + + const makeSets = (sets: SetHeuristic[]) => + _.map(sets, h => { + return { + tree: invertViewWithRoots( + _.map(h.goals, g => g.idx), + tree + ), + inertia: TreeInfo.setInertia(h), + velocity: h.velocity, + momentum: h.momentum + }; + }); + + if (evaluationMode === "release") { + return ; + } + + const flattenSets = (sets: SetHeuristic[]) => + _.flatMap(sets, h => + invertViewWithRoots( + _.map(h.goals, g => g.idx), + tree + ) + ); + + // Flatten all the sets and return them as a list. + const suggestedPredicates = flattenSets(_.slice(sets, 0, 3)); + const others = flattenSets(_.slice(sets, 3)); + return ( + + ); +}; + +export default BottomUp; diff --git a/ide/packages/panoptes/src/TreeView/Directory.tsx b/ide/packages/panoptes/src/TreeView/Directory.tsx index e238a07..be58457 100644 --- a/ide/packages/panoptes/src/TreeView/Directory.tsx +++ b/ide/packages/panoptes/src/TreeView/Directory.tsx @@ -12,7 +12,9 @@ import _ from "lodash"; import React, { useContext, useEffect, useState } from "react"; import "./Directory.css"; +import Attention from "@argus/print/Attention"; import { Node } from "./Node"; +import { WrapNode } from "./Wrappers"; export type ElementPair = [React.ReactElement, React.ReactElement]; @@ -37,21 +39,18 @@ export const CollapsibleElement = ({ const config = useContext(AppContext.ConfigurationContext)!; const openByDefault = startOpen || config.evalMode !== "release"; - const [isOpen, setIsOpen] = useState(openByDefault); const [openIco, closedIco] = icons; - let [children, setChildren] = useState( + const [isOpen, setIsOpen] = useState(openByDefault); + const [children, setChildren] = useState( undefined ); + useEffect(() => { if (children === undefined && Children !== null && isOpen) { setChildren(); } }, [isOpen]); - useEffect(() => { - setIsOpen(startOpen || isOpen); - }, [startOpen, isOpen]); - const toggleCollapse = (e: React.MouseEvent) => { e.preventDefault(); e.stopPropagation(); @@ -63,6 +62,8 @@ export const CollapsibleElement = ({ collapsed: !isOpen }); + const LabelWrapper = startOpen ? Attention : React.Fragment; + return (
{/* biome-ignore lint/a11y/useKeyWithClickEvents: TODO */} @@ -70,7 +71,9 @@ export const CollapsibleElement = ({
{Children !== null ? (isOpen ? openIco : closedIco) : null}
-
{info}
+
+ {info} +
{children}
@@ -85,14 +88,27 @@ export const DirNode = ({ Children: React.FC | null; }) => { const tree = useContext(TreeAppContext.TreeContext)!; - const { Wrapper } = useContext(TreeAppContext.TreeRenderContext); + const { Wrappers, startOpenP } = useContext(TreeAppContext.TreeRenderContext); const node = tree.node(idx); const arrows: ElementPair = [, ]; const dots: ElementPair = [, ]; const icons = "Result" in node ? dots : arrows; - const infoChild = ; - const info = Wrapper ? : infoChild; + const infoChild = ( + + + + ); + + const info = + Wrappers === undefined ? ( + infoChild + ) : ( + + {infoChild} + + ); + const startOpen = startOpenP ? startOpenP(idx) : false; return ( ); }; @@ -112,7 +129,7 @@ export const DirRecursive = ({ getNext: (idx: ProofNodeIdx) => ProofNodeIdx[]; }) => { const tree = useContext(TreeAppContext.TreeContext)!; - const { styleEdges } = useContext(TreeAppContext.TreeRenderContext); + const { styleEdges, onMount } = useContext(TreeAppContext.TreeRenderContext); const node = tree.node(level[0]); const className = classNames("DirRecursive", { "is-candidate": styleEdges && "Candidate" in node, @@ -120,6 +137,10 @@ export const DirRecursive = ({ "generic-edge": !styleEdges }); + useEffect(() => { + onMount ? onMount() : {}; + }, []); + return (
{_.map(level, (current, i) => { diff --git a/ide/packages/panoptes/src/TreeView/Erotisi.tsx b/ide/packages/panoptes/src/TreeView/Erotisi.tsx index efde208..b6bc699 100644 --- a/ide/packages/panoptes/src/TreeView/Erotisi.tsx +++ b/ide/packages/panoptes/src/TreeView/Erotisi.tsx @@ -8,8 +8,8 @@ import { VSCodeButton } from "@vscode/webview-ui-toolkit/react"; import _ from "lodash"; import React, { useContext, useState } from "react"; +import { sortedSubsets } from "./BottomUp"; import { Node } from "./Node"; -import { sortedSubsets } from "./Subsets"; type Target = | { kind: "candidate"; node: ProofNodeIdx } @@ -37,7 +37,7 @@ function formOptions( return ( parent !== undefined && (parent === child || - _.includes(cansOnly(tree.pathToRoot(child).path), parent)) + _.includes(cansOnly(tree.pathToRoot(child).pathInclusive), parent)) ); }; @@ -47,7 +47,9 @@ function formOptions( } const highestNode = _.maxBy(target.goals, g => tree.depth(g.idx))!; - const pathOnlyCandidates = cansOnly(tree.pathFromRoot(highestNode.idx).path); + const pathOnlyCandidates = cansOnly( + tree.pathFromRoot(highestNode.idx).pathInclusive + ); // Remove the candidates that are parents of (or equal to) a decided root. const path = _.dropWhile(pathOnlyCandidates, n => _.some(roots, r => isParentOf(n, r)) @@ -81,7 +83,7 @@ function formOptions( const Erotisi = () => { const tree = useContext(TreeAppContext.TreeContext)!; - const sets = sortedSubsets(tree.failedSets); + const sets = sortedSubsets(tree.failedSets()); if (sets.length === 0) { return ( diff --git a/ide/packages/panoptes/src/Workspace.css b/ide/packages/panoptes/src/TreeView/Panels.css similarity index 96% rename from ide/packages/panoptes/src/Workspace.css rename to ide/packages/panoptes/src/TreeView/Panels.css index 416512a..faae922 100644 --- a/ide/packages/panoptes/src/Workspace.css +++ b/ide/packages/panoptes/src/TreeView/Panels.css @@ -1,3 +1,3 @@ vscode-panel-view { flex-direction: column; -} +} \ No newline at end of file diff --git a/ide/packages/panoptes/src/TreeView/Panels.tsx b/ide/packages/panoptes/src/TreeView/Panels.tsx new file mode 100644 index 0000000..f6caf50 --- /dev/null +++ b/ide/packages/panoptes/src/TreeView/Panels.tsx @@ -0,0 +1,153 @@ +import { arrUpdate } from "@argus/common/func"; +import { TextEmphasis } from "@argus/print/Attention"; +import { + VSCodePanelTab, + VSCodePanelView, + VSCodePanels +} from "@vscode/webview-ui-toolkit/react"; +import _ from "lodash"; +import React, { useId, useState, useEffect } from "react"; + +import "./Panels.css"; + +export type TabProps = React.ComponentPropsWithRef; +export type ViewProps = React.ComponentPropsWithRef; +export type PanelsProps = React.ComponentPropsWithRef; + +export interface PanelDescription { + title: string; + Content: React.FC; + tabProps?: TabProps; + viewProps?: ViewProps; + // FIXME: this shouldn't be here, we should require the title to be unique + fn?: string; +} + +interface PanelState { + activePanel: number; + node?: number; + programatic?: boolean; +} + +export function usePanelState() { + const [state, setState] = useState({ activePanel: 0 }); + return [state, setState] as const; +} + +// NOTE: we don't expect someone to have more than 15 tabs open...the `VSCodePanels` +// is tricky to navigate so this would be an issue. But, we should make this robust to track +// the size of the underlying buffer better. For safety and performance. +function useStateArray(n = 15) { + const [values, setValues] = useState<(T | undefined)[]>( + Array.from({ length: n }) + ); + const updateValue = (idx: number, value: T | undefined) => + setValues(a => arrUpdate(a, idx, value)); + const updateAll = (a: (T | undefined)[]) => + setValues(Array.from({ ...a, length: n })); + return [values, updateValue, updateAll] as const; +} + +const Panels = ({ + manager, + description +}: { + manager?: [number, (n: number) => void, boolean?]; + description: PanelDescription[]; +}) => { + const id = useId(); + const [active, setActive, programaticSwitch] = manager || useState(0); + const tabId = (n: number) => `tab-${id}-${n}`; + + const [openFiles, setOpenFiles, resetOpenFiles] = useStateArray(); + const [tabs, setTabs, resetTabs] = useStateArray(); + const [panels, setPanels, resetPanels] = useStateArray(); + + useEffect(() => { + console.debug(`Panel(${id}) mounted`); + resetOpenFiles(_.map(description, d => d.fn ?? d.title)); + fullRender(); + }, []); + + // NOTE: rerenders should not occur if the user clicks on a tab. We cache the + // elements in state to avoid this. IFF the change is *programatic*, meaning + // some GUI action caused the change, we always want to force a rerender so that + // state change visuals are shown. + useEffect(() => { + console.debug(`Panel(${id}) params changed`, active, programaticSwitch); + if (programaticSwitch) { + // On a programatic switch only rerender the active tab + rerender(active); + } + }, [active, programaticSwitch]); + + // A change in description should always rerender. `useEffect` compares with `Object.is` which + // returns false for the same valued arrays, a simple hash is the concatenation of all panel titles + // which is stable across rerenders. + const descriptionHash = _.reduceRight( + description, + (acc, d) => acc + (d.fn ?? d.title), + "" + ); + useEffect(() => { + console.debug(`Panel(${id}) description changed`); + _.forEach(_.zip(openFiles, description), ([file, d], idx) => { + if (file === (d?.fn ?? d?.title)) return; + + console.debug("Rerendering due to description change", file, d); + setOpenFiles(idx, d?.fn ?? d?.title); + rerender(idx, d); + }); + }, [descriptionHash]); + + const TWrapper = ({ idx, str }: { idx: number; str: string }) => + idx === active && programaticSwitch ? ( + {str} + ) : ( + str + ); + + const elementsAt = (idx: number, d: PanelDescription) => + [ + setActive(idx)} + > + + , + + + + ] as const; + + const rerender = (idx: number, desc?: PanelDescription) => { + if (idx < 0 || description.length <= idx) { + setTabs(idx, undefined); + setPanels(idx, undefined); + } + + const d = desc ?? description[idx]; + const [t, p] = elementsAt(idx, d); + setTabs(idx, t); + setPanels(idx, p); + }; + + const fullRender = () => { + const [ts, ps] = _.unzip( + _.map(description, (d, idx) => elementsAt(idx, d)) + ); + resetTabs(ts); + resetPanels(ps); + }; + + return ( + + {tabs} + {panels} + + ); +}; + +export default Panels; diff --git a/ide/packages/panoptes/src/TreeView/Subsets.css b/ide/packages/panoptes/src/TreeView/Subsets.css deleted file mode 100644 index 4f3da03..0000000 --- a/ide/packages/panoptes/src/TreeView/Subsets.css +++ /dev/null @@ -1,19 +0,0 @@ -.FailingSet { - position: relative; - margin-bottom: 0.25em; - - transition: all 0.25s ease; -} - -.FailingSet.is-hovered { - border: 2px dashed var(--vscode-focusBorder); - padding: 0.25em; -} - -.FailingSet > i { - position: absolute; - top: 0; - right: 0; - - font-size: 0.25em; -} \ No newline at end of file diff --git a/ide/packages/panoptes/src/TreeView/Subsets.tsx b/ide/packages/panoptes/src/TreeView/Subsets.tsx deleted file mode 100644 index 619b2c5..0000000 --- a/ide/packages/panoptes/src/TreeView/Subsets.tsx +++ /dev/null @@ -1,168 +0,0 @@ -import type { ProofNodeIdx, SetHeuristic } from "@argus/common/bindings"; -import { AppContext, TreeAppContext } from "@argus/common/context"; -import classNames from "classnames"; -import _ from "lodash"; -import { observer } from "mobx-react"; -import React, { useContext, useState } from "react"; -import { MiniBufferDataStore } from "../signals"; - -import type { TreeView } from "@argus/common/TreeInfo"; -import { - BottomUpImpersonator, - BottomUpRenderParams, - type TreeViewWithRoot, - invertViewWithRoots -} from "./BottomUp"; -import { CollapsibleElement, DirRecursive } from "./Directory"; -import "./Subsets.css"; -import { IcoComment } from "@argus/print/Icons"; - -/** - * Define the heuristic used for inertia in the system. Previously we were - * using `momentum / velocity` but this proved too sporatic. Some proof trees - * were deep, needlessely, and this threw a wrench in the order. - */ -const setInertia = (set: SetHeuristic) => set.momentum; -export const sortedSubsets = (sets: SetHeuristic[]) => - _.sortBy(sets, setInertia); - -export const RenderBottomUpSets = ({ - views -}: { - views: { - tree: TreeViewWithRoot[]; - inertia: number; - velocity: number; - momentum: number; - }[]; -}) => { - const mkGetChildren = (view: TreeView) => (idx: ProofNodeIdx) => - view.topology.children[idx] ?? []; - - const MkLevel = observer( - (views: { - tree: TreeViewWithRoot[]; - inertia: number; - momentum: number; - velocity: number; - }) => { - if (views.tree.length === 0) { - return null; - } - - const [hovered, setHovered] = useState(false); - const cn = classNames("FailingSet", { "is-hovered": hovered }); - - // If there is only a single predicate, no need to provide all the - // extra information around "grouped predicate sets". - if (views.tree.length === 1) { - return ( -
- -
- ); - } - - const onHover = () => { - MiniBufferDataStore.set({ - kind: "argus-note", - data: ( -

- The outlined obligations must be resolved together -

- ) - }); - setHovered(true); - }; - - const onNoHover = () => { - MiniBufferDataStore.reset(); - setHovered(false); - }; - - return ( -
- - {_.map(views.tree, (leaf, i) => ( - - ))} -
- ); - } - ); - - const argusRecommends = ; - const tail = _.tail(views); - - const otherLabel = "Other failures"; - const fallbacks = - tail.length === 0 ? null : ( - {otherLabel} ...} - Children={() => _.map(tail, (v, i) => )} - /> - ); - - return ( - -

- Argus recommends investigating these failed oblgiations. Click on ’ - {otherLabel}‘ below to see other failed obligations. -

- - {fallbacks} - - ); -}; - -const FailedSubsets = () => { - const tree = useContext(TreeAppContext.TreeContext)!; - const evaluationMode = - useContext(AppContext.ConfigurationContext)?.evalMode ?? "release"; - const sets = sortedSubsets(tree.failedSets); - - const makeSets = (sets: SetHeuristic[]) => - _.map(sets, h => { - return { - tree: invertViewWithRoots( - _.map(h.goals, g => g.idx), - tree - ), - inertia: setInertia(h), - velocity: h.velocity, - momentum: h.momentum - }; - }); - - if (evaluationMode === "release") { - return ; - } - - const flattenSets = (sets: SetHeuristic[]) => - _.flatMap(sets, h => - invertViewWithRoots( - _.map(h.goals, g => g.idx), - tree - ) - ); - - // Flatten all the sets and return them as a list. - const suggestedPredicates = flattenSets(_.slice(sets, 0, 3)); - const others = flattenSets(_.slice(sets, 3)); - return ( - - ); -}; - -export default FailedSubsets; diff --git a/ide/packages/panoptes/src/TreeView/TopDown.css b/ide/packages/panoptes/src/TreeView/TopDown.css deleted file mode 100644 index d541fa6..0000000 --- a/ide/packages/panoptes/src/TreeView/TopDown.css +++ /dev/null @@ -1,16 +0,0 @@ -.tree-toggle { - padding: 0.25em; -} - -.tree-toggle:hover { - cursor: pointer; - color: var(--vscode-input-placeholderForeground); -} - -.floating-graph { - box-shadow: 0 0 5px 0 var(--vscode-focusBorder); - max-height: 70vh; - overflow-y: auto; - overflow-x: hidden; - width: 90%; -} \ No newline at end of file diff --git a/ide/packages/panoptes/src/TreeView/TopDown.tsx b/ide/packages/panoptes/src/TreeView/TopDown.tsx index 0346028..d35a8d4 100644 --- a/ide/packages/panoptes/src/TreeView/TopDown.tsx +++ b/ide/packages/panoptes/src/TreeView/TopDown.tsx @@ -1,106 +1,29 @@ import type { ProofNodeIdx } from "@argus/common/bindings"; import type { TreeRenderParams } from "@argus/common/communication"; import { TreeAppContext } from "@argus/common/context"; -import { IcoTreeDown } from "@argus/print/Icons"; -import { - FloatingFocusManager, - FloatingPortal, - offset, - shift, - useClick, - useDismiss, - useFloating, - useInteractions -} from "@floating-ui/react"; -import classNames from "classnames"; +import {} from "@floating-ui/react"; import _ from "lodash"; -import React, { useContext, useState } from "react"; +import React, { useContext } from "react"; import { DirRecursive } from "./Directory"; -import Graph from "./Graph"; -import "./TopDown.css"; -export const WrapTreeIco = ({ - n, - Child -}: { - n: ProofNodeIdx; - Child: React.ReactElement; -}) => { - const [isHovered, setIsHovered] = useState(false); - const [isOpen, setIsOpen] = useState(false); - const { refs, floatingStyles, context } = useFloating({ - open: isOpen, - onOpenChange: setIsOpen, - placement: "bottom", - middleware: [offset(() => 5), shift()] - }); - - const click = useClick(context); - const dismiss = useDismiss(context); - const { getReferenceProps, getFloatingProps } = useInteractions([ - click, - dismiss - ]); - - return ( - setIsHovered(true)} - onMouseLeave={() => setIsHovered(false)} - > - {Child} - - - - {isOpen && ( - - -
- -
- - - )} - - ); -}; - -const TopDown = () => { +const TopDown = ({ start }: { start?: ProofNodeIdx }) => { const tree = useContext(TreeAppContext.TreeContext)!; - - // Sort the candidates by the #infer vars / height of the tree const getGoalChildren = (kids: ProofNodeIdx[]) => - _.sortBy(kids, [k => -tree.maxHeight(k)]); + _.sortBy(kids, [k => tree.minInertiaOnPath(k)]); const getCandidateChildren = (kids: ProofNodeIdx[]) => _.sortBy(_.uniq(kids), [ - // k => { - // const node = tree.node(k); - // return "Goal" in node && tree.goal(node.Goal).isMainTv ? 1 : 0; - // }, k => { switch (tree.nodeResult(k)) { case "no": - return 0; + return tree.minInertiaOnPath(k); case "maybe-overflow": - return 1; + return tree.minInertiaOnPath(k) + 10_000; case "maybe-ambiguity": - return 2; - case "yes": - return 3; + return tree.minInertiaOnPath(k) + 100_000; default: - return 4; + return 1_000_000; } } ]); @@ -117,9 +40,32 @@ const TopDown = () => { } }; + const ops = + start === undefined + ? undefined + : (() => { + const pathToRootFromStart = tree.pathToRoot(start); + const startOpenP = (idx: ProofNodeIdx) => + _.includes(pathToRootFromStart.pathInclusive, idx); + const onMount = () => { + const element = document.querySelector( + `.proof-node-${start}` + ); + element?.scrollIntoView({ + block: "start", + inline: "nearest", + behavior: "smooth" + }); + }; + return { + startOpenP, + onMount + }; + })(); + const renderParams: TreeRenderParams = { - Wrapper: WrapTreeIco, - styleEdges: true + styleEdges: true, + ...ops }; return ( diff --git a/ide/packages/panoptes/src/TreeView/TreeApp.tsx b/ide/packages/panoptes/src/TreeView/TreeApp.tsx index f12b3e0..66a5721 100644 --- a/ide/packages/panoptes/src/TreeView/TreeApp.tsx +++ b/ide/packages/panoptes/src/TreeView/TreeApp.tsx @@ -1,20 +1,24 @@ import TreeInfo from "@argus/common/TreeInfo"; import type { SerializedTree } from "@argus/common/bindings"; -import { AppContext, TreeAppContext } from "@argus/common/context"; +import { TreeAppContext } from "@argus/common/context"; import { TyCtxt } from "@argus/print/context"; -import { - VSCodePanelTab, - VSCodePanelView, - VSCodePanels -} from "@vscode/webview-ui-toolkit/react"; -import _ from "lodash"; -import React, { useContext } from "react"; +import React from "react"; +import BottomUp from "./BottomUp"; import Erotisi from "./Erotisi"; -import FailedSubsets from "./Subsets"; +import Panels, { type PanelDescription, usePanelState } from "./Panels"; import TopDown from "./TopDown"; import "./TreeApp.css"; -import TreeCycle from "./TreeCycle"; + +// FIXME: this shouldn't ever happen, if a properly hashed +// value is sent and returned. I need to think more about how to handle +// when we want to display "non-traditional" obligations. +const ErrorMessage = () => ( +
+

Whoops! Something went wrong:

+ 
No debug information found.
+
+); const TreeApp = ({ tree, @@ -23,17 +27,6 @@ const TreeApp = ({ tree: SerializedTree | undefined; showHidden?: boolean; }) => { - const evalMode = useContext(AppContext.ConfigurationContext)!.evalMode; - // FIXME: this shouldn't ever happen, if a properly hashed - // value is sent and returned. I need to think more about how to handle - // when we want to display "non-traditional" obligations. - const ErrorMessage = () => ( -
-

Whoops! Something went wrong:

- 
No debug information found.
-
- ); - if (tree === undefined) { console.error("Returned tree `undefined`"); return ; @@ -46,43 +39,64 @@ const TreeApp = ({ return ; } - const tabs: [string, React.FC][] = [["Top Down", TopDown]]; + const tyCtx = { + interner: internedTys, + projections: tree.projectionValues + }; + + // -------------------------------------- + // State dependent data for tab switching - if (treeInfo.errorLeaves().length > 0) { + const [state, setState] = usePanelState(); + + const tabs: PanelDescription[] = [ + { + title: "Top Down", + Content: () => + } + ]; + + if (treeInfo.failedSets().length > 0) { // Unshift to place this first - tabs.unshift(["Bottom Up", FailedSubsets]); + // NOTE: the passing the TopDown panel ID is important, make sure it's always correct. + // FIXME: we probably shouldn't hard-code that value here... + tabs.unshift({ + title: "Bottom Up", + Content: () => ( + + // Callback passed to the BottomUp panel to jump to the TopDown panel. + setState({ activePanel: 1, node: n, programatic: true }) + } + /> + ) + }); // Push to place this last - tabs.push(["Help Me", Erotisi]); + tabs.push({ title: "Help Me", Content: Erotisi }); } // HACK: we shouldn't test for eval mode here but Playwright is off on the button click. - if (tree.cycle !== undefined && evalMode === "release") { - // FIXME: why do I need the '!' here? - - - - - -------- VVVVVVVV - tabs.unshift(["Cycle Detected", () => ]); - } - - const tyCtx = { - interner: internedTys, - projections: tree.projectionValues - }; + // if (tree.cycle !== undefined && evalMode === "release") { + // // FIXME: why do I need the '!' here? - - - - - -------- VVVVVVVV + // tabs.unshift({ + // title: "Cycle Detected", + // Content: () => + // }); + // } return (
- - {_.map(tabs, ([name, _], idx) => ( - - {name} - - ))} - {_.map(tabs, ([_, Component], idx) => ( - - - - ))} - + setState({ activePanel: n }), + state.programatic + ]} + description={tabs} + />
diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.css b/ide/packages/panoptes/src/TreeView/Wrappers.css new file mode 100644 index 0000000..9d122ce --- /dev/null +++ b/ide/packages/panoptes/src/TreeView/Wrappers.css @@ -0,0 +1,36 @@ +.tree-toggle { + padding: 0.25em; +} + +.tree-toggle:hover { + cursor: pointer; + color: var(--vscode-input-placeholderForeground); +} + +.floating-graph { + box-shadow: 0 0 5px 0 var(--vscode-focusBorder); + max-height: 70vh; + overflow-y: auto; + overflow-x: hidden; + width: 90%; +} + +.ImplCandidatesPanel { + padding: 0.5em; +} + +.ImplCandidatesPanel > div { + margin-bottom: 1em; +} + +.WrapperBox { + display: inline-flex; + flex-direction: row; + justify-content: space-evenly; + gap: 0.25em; +} + +.WrapperBox i:hover { + cursor: pointer; + color: var(--vscode-input-placeholderForeground); +} \ No newline at end of file diff --git a/ide/packages/panoptes/src/TreeView/Wrappers.tsx b/ide/packages/panoptes/src/TreeView/Wrappers.tsx new file mode 100644 index 0000000..e1bdf13 --- /dev/null +++ b/ide/packages/panoptes/src/TreeView/Wrappers.tsx @@ -0,0 +1,170 @@ +import type { ProofNodeIdx } from "@argus/common/bindings"; +import type { + InfoWrapper, + InfoWrapperProps +} from "@argus/common/communication"; +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, + FloatingPortal, + arrow, + offset, + shift, + useClick, + useDismiss, + useFloating, + useInteractions +} from "@floating-ui/react"; +import classNames from "classnames"; +import _ from "lodash"; +import React, { type ReactElement, useState, useContext, useRef } from "react"; +import Graph from "./Graph"; + +import "./Wrappers.css"; + +export const WrapNode = ({ + children, + wrappers, + n +}: React.PropsWithChildren<{ wrappers: InfoWrapper[]; n: ProofNodeIdx }>) => { + const [hovered, setHovered] = useState(false); + const [actives, setActives] = useState(Array(wrappers.length).fill(false)); + const active = _.some(actives); + + return ( + setHovered(true)} + onMouseLeave={() => setHovered(false)} + > + {children} + {(hovered || active) && ( + + {_.map(wrappers, (W, i) => ( + setActives(a => arrUpdate(a, i, b))} + /> + ))} + + )} + + ); +}; + +const composeEvents = + (...es: ((t: T) => void)[]) => + (t: T) => + _.forEach(es, e => e(t)); + +const DetailsPortal = ({ + children, + info, + reportActive +}: React.PropsWithChildren< + Omit & { info: ReactElement } +>) => { + const [isOpen, setIsOpen] = useState(false); + const openCallback = composeEvents(setIsOpen, reportActive); + const arrowRef = useRef(null); + + const ARROW_HEIGHT = 10; + const GAP = 5; + + const { refs, floatingStyles, context } = useFloating({ + open: isOpen, + onOpenChange: openCallback, + placement: "bottom", + middleware: [ + offset(ARROW_HEIGHT + GAP), + shift(), + arrow({ + element: arrowRef + }) + ] + }); + + const click = useClick(context); + const dismiss = useDismiss(context); + const { getReferenceProps, getFloatingProps } = useInteractions([ + click, + dismiss + ]); + + return ( + <> + + {info} + + {isOpen && ( + + +
+ + {children} +
+ + + )} + + ); +}; + +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; + } + + return ( + }> +

The following {candidates.length} implementations are available:

+
+ {_.map(candidates, (c, i) => ( +
+ +
+ ))} +
+ + ); +}; + +export const mkJumpToTopDownWrapper = + (jumpTo: (n: ProofNodeIdx) => void) => + ({ n }: InfoWrapperProps) => { + const jumpToTree = (e: React.MouseEvent) => { + e.preventDefault(); + e.stopPropagation(); + jumpTo(n); + }; + + return ; + }; diff --git a/ide/packages/panoptes/src/TreeView/heuristic.ts b/ide/packages/panoptes/src/TreeView/heuristic.ts index 6a37951..c476e79 100644 --- a/ide/packages/panoptes/src/TreeView/heuristic.ts +++ b/ide/packages/panoptes/src/TreeView/heuristic.ts @@ -228,9 +228,9 @@ class Heuristic implements HeuristicI { const sortWeightPaths = (t: T) => { const leaf = f(t); const pathToRoot = this.tree.pathToRoot(leaf); - const len = pathToRoot.path.length; + const len = pathToRoot.length; const numVars = _.reduce( - pathToRoot.path, + pathToRoot.pathInclusive, (sum, k) => sum + this.tree.inferVars(k), 0 ); @@ -260,6 +260,9 @@ class Heuristic implements HeuristicI { } errorLeavesInSimpleRecommendedOrder() { - return this.rank(this.tree.errorLeaves(), _.identity); + const errorLeaves = _.flatMap(this.tree.failedSets(), g => + _.map(g.goals, g => g.idx) + ); + return this.rank(errorLeaves, _.identity); } } diff --git a/ide/packages/panoptes/src/Workspace.tsx b/ide/packages/panoptes/src/Workspace.tsx index 7329a7c..7a7c471 100644 --- a/ide/packages/panoptes/src/Workspace.tsx +++ b/ide/packages/panoptes/src/Workspace.tsx @@ -1,19 +1,16 @@ import type { FileInfo } from "@argus/common/lib"; import ReportBugUrl from "@argus/print/ReportBugUrl"; -import { - VSCodePanelTab, - VSCodePanelView, - VSCodePanels -} from "@vscode/webview-ui-toolkit/react"; import _ from "lodash"; -import React, { useState } from "react"; +import React, { useEffect } from "react"; import { ErrorBoundary } from "react-error-boundary"; +import { observer } from "mobx-react"; import File from "./File"; -import "./Workspace.css"; - -// TODO: the workspace should manage a set of files. Currently the App is doing -// that, but the App should just launch the current workspace. +import Panels, { + type PanelDescription, + usePanelState +} from "./TreeView/Panels"; +import { HighlightTargetStore } from "./signals"; function basename(path: string) { return path.split("/").reverse()[0]; @@ -30,44 +27,64 @@ const FatalErrorPanel = ({ error, resetErrorBoundary }: any) => (
); -const Workspace = ({ - files, - reset -}: { - files: FileInfo[]; - reset: () => void; -}) => { - const [active, setActive] = useState(0); +const Workspace = observer( + ({ + files, + reset + }: { + files: FileInfo[]; + reset: () => void; + }) => { + const [state, setState] = usePanelState(); + + useEffect(() => { + if (HighlightTargetStore.value?.file === undefined) return; - const mkActiveSet = (idx: number) => () => setActive(idx); - const tabName = (idx: number) => `tab-${idx}`; + const idx = _.findIndex( + files, + ({ fn }) => fn === HighlightTargetStore.value?.file + ); + if (0 <= idx && idx !== state.activePanel) + setState({ activePanel: idx, programatic: true }); + }, [HighlightTargetStore.value?.file]); - const tabs = _.map(files, ({ fn }, idx) => ( - - {basename(fn)} - - )); + const viewProps = { + style: { + paddingLeft: 0, + paddingRight: 0 + } + }; - const fileComponents = _.map(files, ({ fn, data }, idx) => ( - - - - - - )); + const tabs: PanelDescription[] = _.map(files, ({ fn, data }, idx) => { + return { + fn, + viewProps, + title: basename(fn), + Content: () => ( + + + + ) + }; + }); - return ( -
- - {tabs} - {fileComponents} - -
- ); -}; + return ( +
+ setState({ activePanel: n }), + state.programatic + ]} + /> +
+ ); + } +); export default Workspace; diff --git a/ide/packages/panoptes/src/signals.ts b/ide/packages/panoptes/src/signals.ts index 3d31e2e..e2daf21 100644 --- a/ide/packages/panoptes/src/signals.ts +++ b/ide/packages/panoptes/src/signals.ts @@ -4,7 +4,9 @@ import type { TypeContext } from "@argus/print/context"; import { action, makeObservable, observable } from "mobx"; import type { ReactElement } from "react"; -class HighlightTargetStore { +class HighlightTarget { + private static DURATION = 1000; + value?: ErrorJumpTargetInfo; constructor() { @@ -17,7 +19,11 @@ class HighlightTargetStore { } set(info: ErrorJumpTargetInfo) { + console.debug("Setting highlight target", info); this.value = info; + + // The target value for a highlight should only last for a short time. + window.setTimeout(() => this.reset(), HighlightTarget.DURATION); } reset() { @@ -25,7 +31,7 @@ class HighlightTargetStore { } } -export const highlightedObligation = new HighlightTargetStore(); +export const HighlightTargetStore = new HighlightTarget(); // MiniBuffer data that should *not* rely on type context type DataNoCtx = { @@ -55,6 +61,7 @@ class MiniBufferData { makeObservable(this, { data: observable, set: action, + reset: action, pin: action, unpin: action }); diff --git a/ide/packages/print/src/Attention.css b/ide/packages/print/src/Attention.css new file mode 100644 index 0000000..fdc62e1 --- /dev/null +++ b/ide/packages/print/src/Attention.css @@ -0,0 +1,47 @@ +@keyframes attention-highlight { + 0% { + display: inline-block; + background-color: transparent; + } + + 50% { + display: inline-block; + background-color: var(--vscode-editor-findMatchBackground); + border: 2px solid var(--vscode-editor-findMatchBorder); + border-radius: 2px; + } + + 100% { + display: inline-block; + background-color: transparent; + } +} + +@keyframes attention-text { + 0% { + font-size: 100%; + font-weight: normal; + } + + 50% { + font-size: 110%; + font-weight: bold; + } + + 100% { + font-size: 100%; + font-weight: normal; + } +} + + +span.Attention { + display: inline-block; + animation: attention-highlight 1.25s ease-out; +} + +span.AttentionText { + display: inline-block; + background-color: transparent; + animation: attention-text 2s ease-in-out; +} \ No newline at end of file diff --git a/ide/packages/print/src/Attention.tsx b/ide/packages/print/src/Attention.tsx new file mode 100644 index 0000000..3d6a99e --- /dev/null +++ b/ide/packages/print/src/Attention.tsx @@ -0,0 +1,13 @@ +import React from "react"; + +import "./Attention.css"; + +export const TextEmphasis = ({ children }: React.PropsWithChildren) => ( + {children} +); + +const Attention = ({ children }: React.PropsWithChildren) => ( + {children} +); + +export default Attention; diff --git a/ide/packages/print/src/Comment.tsx b/ide/packages/print/src/Comment.tsx index 31f656f..1c6d317 100644 --- a/ide/packages/print/src/Comment.tsx +++ b/ide/packages/print/src/Comment.tsx @@ -12,6 +12,8 @@ import classNames from "classnames"; import React, { useState } from "react"; import { IcoComment } from "./Icons"; +import "./Wrappers.css"; + const Comment = ({ Child, Content diff --git a/ide/packages/print/src/Icons.tsx b/ide/packages/print/src/Icons.tsx index cd126cc..87fefbc 100644 --- a/ide/packages/print/src/Icons.tsx +++ b/ide/packages/print/src/Icons.tsx @@ -1,6 +1,7 @@ import React from "react"; import "./Icons.css"; +import classNames from "classnames"; type ButtonProps = { onClick?: (event: React.MouseEvent) => void; @@ -9,7 +10,10 @@ type ButtonProps = { const makeCodicon = (name: string) => (props: React.HTMLAttributes & ButtonProps) => ( - + ); // NOTE: not an exhaustive list of call vscode codicons, just add them when necessary. @@ -37,3 +41,4 @@ export const IcoEyeClosed = makeCodicon("eye-closed"); export const IcoLock = makeCodicon("lock"); export const IcoTreeDown = makeCodicon("type-hierarchy-sub"); export const IcoPinned = makeCodicon("pinned"); +export const IcoListUL = makeCodicon("list-unordered"); diff --git a/ide/packages/print/src/Toggle.css b/ide/packages/print/src/Toggle.css index 1ef4d05..da433b9 100644 --- a/ide/packages/print/src/Toggle.css +++ b/ide/packages/print/src/Toggle.css @@ -1,14 +1,16 @@ -.toggle-box { - display: inline; +details.toggle-box { + display: inline-block; border: 1px solid var(--vscode-textCodeBlock-background); border-radius: 4px; } -.toggle-box.expanded { - display: inline-block; +details[open].toggle-box > summary { + display: none; } -.toggle-box .summary { +details.toggle-box > summary { + list-style: none; + color: var(--vscode-input-placeholderForeground); font-size: 80%; } \ No newline at end of file diff --git a/ide/packages/print/src/Toggle.tsx b/ide/packages/print/src/Toggle.tsx index 9be6c7e..4adb3af 100644 --- a/ide/packages/print/src/Toggle.tsx +++ b/ide/packages/print/src/Toggle.tsx @@ -1,4 +1,3 @@ -import classNames from "classnames"; import React, { useState } from "react"; import "./Toggle.css"; @@ -13,14 +12,17 @@ export const Toggle = ({ const [expanded, setExpanded] = useState(false); return ( // biome-ignore lint/a11y/useKeyWithClickEvents: TODO -
{ + e.preventDefault(); e.stopPropagation(); - setExpanded(!expanded); + setExpanded(e => !e); }} > - {expanded ? : {summary}} -
+ {summary} + + ); }; diff --git a/ide/packages/print/src/private/ty.tsx b/ide/packages/print/src/private/ty.tsx index bec2f22..e1b1717 100644 --- a/ide/packages/print/src/private/ty.tsx +++ b/ide/packages/print/src/private/ty.tsx @@ -109,7 +109,6 @@ export const PrintTy = ({ o }: { o: Ty }) => { const allowProjection = useContext(AllowProjectionSubst); if (allowProjection && projectedId !== undefined) { const projectedValue = tyCtx.interner[projectedId]; - console.info("Printing alias instead!"); return ; }