From 07457fc9795c77076bffadca7238e1053d4c888a Mon Sep 17 00:00:00 2001 From: Gavin Gray Date: Mon, 19 Feb 2024 16:59:20 +0100 Subject: [PATCH] Hiding extra information in the IDE, sorting trees. --- crates/argus/src/ext.rs | 14 ++ crates/argus/src/proof_tree/mod.rs | 28 ++-- crates/argus/src/serialize/const.rs | 42 ++++-- crates/argus/src/serialize/mod.rs | 31 +++- crates/argus/src/serialize/path/mod.rs | 12 ++ ide/packages/extension/src/ctx.ts | 6 +- .../panoptes/src/TreeView/BottomUp.tsx | 66 +++++++-- .../panoptes/src/TreeView/TopDown.tsx | 39 ++++- .../panoptes/src/TreeView/TreeInfo.ts | 136 ++++++++++++------ ide/packages/panoptes/src/print/print.tsx | 13 +- .../panoptes/src/print/private/const.tsx | 14 +- ide/packages/panoptes/src/utilities/func.ts | 2 +- 12 files changed, 297 insertions(+), 106 deletions(-) diff --git a/crates/argus/src/ext.rs b/crates/argus/src/ext.rs index 95c3bfc..5fb7144 100644 --- a/crates/argus/src/ext.rs +++ b/crates/argus/src/ext.rs @@ -43,6 +43,8 @@ pub trait PredicateExt { fn is_rhs_lang_item(&self, tcx: &TyCtxt) -> bool; fn is_trait_pred_rhs(&self, def_id: DefId) -> bool; + + fn is_lhs_ty_var(&self) -> bool; } impl PredicateExt for Predicate<'_> { @@ -66,6 +68,18 @@ impl PredicateExt for Predicate<'_> { trait_predicate.def_id() == def_id }) } + + fn is_lhs_ty_var(&self) -> bool { + match self.kind().skip_binder() { + ty::PredicateKind::Clause(ty::ClauseKind::Trait(trait_predicate)) => { + trait_predicate.self_ty().is_ty_var() + } + ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives( + ty::OutlivesPredicate(ty, _), + )) => ty.is_ty_var(), + _ => false, + } + } } pub trait StableHash<'__ctx, 'tcx>: diff --git a/crates/argus/src/proof_tree/mod.rs b/crates/argus/src/proof_tree/mod.rs index 8b9114d..583d404 100644 --- a/crates/argus/src/proof_tree/mod.rs +++ b/crates/argus/src/proof_tree/mod.rs @@ -16,8 +16,8 @@ pub use topology::*; use ts_rs::TS; use crate::{ - ext::InferCtxtExt, - serialize::{serialize_to_value, ty::Goal__PredicateDef}, + ext::{InferCtxtExt, PredicateExt}, + serialize::{safe::GoalPredicateDef, serialize_to_value}, types::{ intermediate::{EvaluationResult, EvaluationResultDef}, ImplHeader, ObligationNecessity, @@ -63,10 +63,13 @@ pub struct Goal { #[cfg_attr(feature = "testing", ts(type = "EvaluationResult"))] result: EvaluationResult, - // TODO: remove this is only for debugging - debug_comparison: String, necessity: ObligationNecessity, num_vars: usize, + is_lhs_ty_var: bool, + + #[cfg(debug_assertions)] + #[cfg_attr(feature = "testing", ts(type = "string | undefined"))] + debug_comparison: String, } #[derive(Serialize, Clone, Debug, PartialEq, Eq)] @@ -115,24 +118,21 @@ impl Goal { goal: &solve::Goal<'tcx, ty::Predicate<'tcx>>, result: EvaluationResult, ) -> Self { - #[derive(Serialize)] - struct Wrapper<'a, 'tcx: 'a>( - #[serde(with = "Goal__PredicateDef")] - &'a solve::Goal<'tcx, ty::Predicate<'tcx>>, - ); - // TODO remove after deubbing - let debug_comparison = format!("{:?}", goal.predicate.kind().skip_binder()); let necessity = infcx.guess_predicate_necessity(&goal.predicate); let num_vars = serialize::var_counter::count_vars(infcx.tcx, goal.predicate); - let goal = serialize_to_value(infcx, &Wrapper(goal)) + let goal_value = serialize_to_value(infcx, &GoalPredicateDef(*goal)) .expect("failed to serialize goal"); + Self { - goal, + goal: goal_value, result, - debug_comparison, necessity, num_vars, + is_lhs_ty_var: goal.predicate.is_lhs_ty_var(), + + #[cfg(debug_assertions)] + debug_comparison: format!("{:?}", goal.predicate.kind().skip_binder()), } } } diff --git a/crates/argus/src/serialize/const.rs b/crates/argus/src/serialize/const.rs index 61288ef..4a2817c 100644 --- a/crates/argus/src/serialize/const.rs +++ b/crates/argus/src/serialize/const.rs @@ -170,17 +170,28 @@ impl ParamConstDef { #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export, rename = "UnevaluatedConst"))] #[serde(tag = "type")] -enum UnevaluatedConstKind<'tcx> { - ValuePath { data: path::ValuePathWithArgs<'tcx> }, - AnonSnippet { data: String }, +enum UnevaluatedConstDef<'tcx> { + ValuePath { + data: path::ValuePathWithArgs<'tcx>, + }, + AnonSnippet { + data: String, + }, + AnonLocation { + #[serde(with = "SymbolDef")] + #[cfg_attr(feature = "testing", ts(type = "Symbol"))] + krate: Symbol, + + path: path::BasicPathNoArgs<'tcx>, + }, } -impl<'tcx> From<&UnevaluatedConst<'tcx>> for UnevaluatedConstKind<'tcx> { - fn from(value: &UnevaluatedConst<'tcx>) -> Self { +impl<'tcx> UnevaluatedConstDef<'tcx> { + fn new(value: &UnevaluatedConst<'tcx>) -> Self { let infcx = get_dynamic_ctx(); let UnevaluatedConst { def, args } = value; match infcx.tcx.def_kind(def) { - DefKind::Const | DefKind::AssocConst => UnevaluatedConstKind::ValuePath { + DefKind::Const | DefKind::AssocConst => Self::ValuePath { data: path::ValuePathWithArgs::new(*def, args), }, DefKind::AnonConst => { @@ -188,26 +199,31 @@ impl<'tcx> From<&UnevaluatedConst<'tcx>> for UnevaluatedConstKind<'tcx> { && let span = infcx.tcx.def_span(def) && let Ok(snip) = infcx.tcx.sess.source_map().span_to_snippet(span) { - UnevaluatedConstKind::AnonSnippet { data: snip } + Self::AnonSnippet { data: snip } } else { - todo!() + // Do not call `print_value_path` as if a parent of this anon const is an impl it will + // attempt to print out the impl trait ref i.e. `::{constant#0}`. This would + // cause printing to enter an infinite recursion if the anon const is in the self type i.e. + // `impl Default for [T; 32 - 1 - 1 - 1] {` + // where we would try to print `<[T; /* print `constant#0` again */] as Default>::{constant#0}` + Self::AnonLocation { + krate: infcx.tcx.crate_name(def.krate), + path: path::BasicPathNoArgs::new(*def), + } } } defkind => panic!("unexpected defkind {:?} {:?}", defkind, value), } } -} -pub struct UnevaluatedConstDef; -impl UnevaluatedConstDef { - pub fn serialize<'tcx, S>( + pub fn serialize( value: &UnevaluatedConst<'tcx>, s: S, ) -> Result where S: serde::Serializer, { - UnevaluatedConstKind::from(value).serialize(s) + Self::new(value).serialize(s) } } diff --git a/crates/argus/src/serialize/mod.rs b/crates/argus/src/serialize/mod.rs index 4b44184..c7fb48b 100644 --- a/crates/argus/src/serialize/mod.rs +++ b/crates/argus/src/serialize/mod.rs @@ -170,15 +170,42 @@ define_helper!( pub(crate) mod safe { use rustc_hir::def_id::DefId; + use rustc_trait_selection::traits::solve; + #[cfg(feature = "testing")] + use ts_rs::TS; use super::*; #[derive(Serialize)] - pub struct PathDefNoArgs(#[serde(with = "path::PathDefNoArgs")] pub DefId); + #[cfg_attr(feature = "testing", derive(TS))] + #[cfg_attr(feature = "testing", ts(export))] + #[cfg_attr(feature = "testing", ts(rename = "GoalPredicateDefSafeWrapper"))] + pub struct GoalPredicateDef<'tcx>( + #[serde(with = "ty::Goal__PredicateDef")] + #[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))] + pub solve::Goal<'tcx, rustc_ty::Predicate<'tcx>>, + ); + + #[derive(Serialize)] + #[cfg_attr(feature = "testing", derive(TS))] + #[cfg_attr(feature = "testing", ts(export))] + #[cfg_attr(feature = "testing", ts(rename = "PathDefNoArgsSafeWrapper"))] + pub struct PathDefNoArgs( + #[serde(with = "path::PathDefNoArgs")] + #[cfg_attr(feature = "testing", ts(type = "PathDefNoArgs"))] + pub DefId, + ); #[derive(Serialize)] + #[cfg_attr(feature = "testing", derive(TS))] + #[cfg_attr(feature = "testing", ts(export))] + #[cfg_attr( + feature = "testing", + ts(rename = "TraitRefPrintOnlyTraitPathDefSafeWrapper") + )] pub struct TraitRefPrintOnlyTraitPathDef<'tcx>( #[serde(with = "ty::TraitRefPrintOnlyTraitPathDef")] - pub rustc_ty::TraitRef<'tcx>, + #[cfg_attr(feature = "testing", ts(type = "TraitRefPrintOnlyTraitPath"))] + pub rustc_ty::TraitRef<'tcx>, ); } diff --git a/crates/argus/src/serialize/path/mod.rs b/crates/argus/src/serialize/path/mod.rs index febc783..f871978 100644 --- a/crates/argus/src/serialize/path/mod.rs +++ b/crates/argus/src/serialize/path/mod.rs @@ -62,6 +62,18 @@ impl<'tcx> ValuePathWithArgs<'tcx> { } } +#[derive(Serialize)] +#[cfg_attr(feature = "testing", derive(TS))] +#[cfg_attr(feature = "testing", ts(export))] +// Useful in scenarios when using a `ValuePathXXX` would cause the +// pretty printer to enter an infinite loop. +pub struct BasicPathNoArgs<'tcx>(DefinedPath<'tcx>); +impl<'tcx> BasicPathNoArgs<'tcx> { + pub fn new(def_id: DefId) -> Self { + Self(PathBuilder::compile_value_path(def_id, &[])) + } +} + #[derive(Serialize)] #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export))] diff --git a/ide/packages/extension/src/ctx.ts b/ide/packages/extension/src/ctx.ts index 3779431..ac4c776 100644 --- a/ide/packages/extension/src/ctx.ts +++ b/ide/packages/extension/src/ctx.ts @@ -392,11 +392,7 @@ class BackendCache { // NOTE: the returned value should be an array of a single tree, however, // it is possible that no tree is returned. (Yes, but I'm working on it.) - const tree = _.filter(res.value, t => t !== undefined) as Array< - SerializedTree | undefined - >; - - const tree0 = tree[0]; + const tree0 = _.compact(res.value)[0]; if (tree0 === undefined) { return; } diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index f2dc197..029d25e 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx @@ -3,11 +3,16 @@ import _ from "lodash"; import React, { useContext } from "react"; import { TreeContext } from "./Context"; -import { DirRecursive } from "./Directory"; +import { CollapsibleElement, DirRecursive } from "./Directory"; const BottomUp = () => { const tree = useContext(TreeContext)!; - const leaves = _.map(tree.errorNodes(), leaf => { + const getParent = (idx: ProofNodeIdx) => { + let p = tree.parent(idx); + return p !== undefined ? [p] : []; + }; + + const leaves = _.map(tree.errorNodesRecommendedOrder(), leaf => { let curr: ProofNodeIdx | undefined = leaf; while (curr !== undefined && !("Goal" in tree.node(curr))) { curr = tree.parent(curr); @@ -15,22 +20,53 @@ const BottomUp = () => { return curr; }); - const getParent = (idx: ProofNodeIdx) => { - let p = tree.parent(idx); - return p !== undefined ? [p] : []; + // The "Argus recommended" errors are shown expanded, and the + // "others" are collapsed. Argus recommended errors are the ones + // that failed or are ambiguous with a concrete type on the LHS. + const [argusRecommended, others] = _.partition(_.compact(leaves), leaf => { + const node = tree.node(leaf); + if ("Goal" in node) { + const goal = node.Goal.data; + return ( + goal.result === "no" || + goal.result === "maybe-overflow" || + !goal.isLhsTyVar + ); + } else { + // Leaves should only be goals... + return false; + } + }); + + const LeafElement = ({ leaf }: { leaf: ProofNodeIdx }) => { + return ( + + ); }; - return _.map(leaves, (leaf, i) => - leaf === undefined ? ( - "" - ) : ( - ( + + )); + + const fallbacks = + others.length === 0 ? null : ( + Other failures ...} + Children={() => ( + <> + {_.map(others, (leaf, i) => ( + + ))} + + )} /> - ) + ); + + return ( + <> + {recommended} + {fallbacks} + ); }; diff --git a/ide/packages/panoptes/src/TreeView/TopDown.tsx b/ide/packages/panoptes/src/TreeView/TopDown.tsx index 763c68f..17ff733 100644 --- a/ide/packages/panoptes/src/TreeView/TopDown.tsx +++ b/ide/packages/panoptes/src/TreeView/TopDown.tsx @@ -1,4 +1,4 @@ -import { ProofNodeIdx } from "@argus/common/bindings"; +import { Candidate, Goal, ProofNodeIdx } from "@argus/common/bindings"; import _ from "lodash"; import React, { useContext } from "react"; @@ -7,7 +7,42 @@ import { DirRecursive } from "./Directory"; const TopDown = () => { const tree = useContext(TreeContext)!; - const getChildren = (idx: ProofNodeIdx) => tree.children(idx); + + const getGoalChildren = (kids: ProofNodeIdx[]) => { + // Sort the candidates by the #infer vars / height of the tree + return _.sortBy(kids, k => { + const inferVars = tree.inferVars(k); + const height = tree.maxHeigh(k); + return inferVars / height; + }); + }; + + const getCandidateChildren = (kids: ProofNodeIdx[]) => { + return _.sortBy(kids, k => { + switch (tree.result(k) ?? "yes") { + case "no": + return 0; + case "maybe-overflow": + return 1; + case "maybe-ambiguity": + return 2; + case "yes": + return 3; + } + }); + }; + + const getChildren = (idx: ProofNodeIdx) => { + const node = tree.node(idx); + const kids = tree.children(idx); + if ("Goal" in node) { + return getGoalChildren(kids); + } else if ("Candidate" in node) { + return getCandidateChildren(kids); + } else { + return []; + } + }; return ( ); diff --git a/ide/packages/panoptes/src/TreeView/TreeInfo.ts b/ide/packages/panoptes/src/TreeView/TreeInfo.ts index 4daa4ed..33357e9 100644 --- a/ide/packages/panoptes/src/TreeView/TreeInfo.ts +++ b/ide/packages/panoptes/src/TreeView/TreeInfo.ts @@ -1,4 +1,5 @@ import { + EvaluationResult, ProofNodeIdx, SerializedTree, TreeTopology, @@ -15,6 +16,54 @@ interface Path { path: T[]; d: D; } +function makeTreeView( + root: ProofNodeIdx, + cf: (n: ProofNodeIdx) => ControlFlow, + childrenOf: (n: ProofNodeIdx) => ProofNodeIdx[] +): TreeView { + const children: MultiRecord = {}; + const parent: Record = {}; + const addChildRel = (from: ProofNodeIdx, to: ProofNodeIdx) => { + if (children[from]) { + children[from].push(to); + } else { + children[from] = [to]; + } + if (parent[to]) { + throw new Error("parent already set"); + } + parent[to] = from; + }; + + const iterate = (curr: ProofNodeIdx, prev?: ProofNodeIdx) => { + const kids = childrenOf(curr); + let newPrev = prev; + switch (cf(curr)) { + case "keep": { + if (prev !== undefined) { + addChildRel(prev, curr); + } + newPrev = curr; + break; + } + case "remove-node": + break; + case "remove-tree": + return; + } + _.forEach(kids, kid => iterate(kid, newPrev)); + }; + + iterate(root); + + if (children[root] === undefined) { + throw new Error("Root has no children"); + } + + return { + topology: { children, parent }, + }; +} export interface TreeView { topology: TreeTopology; @@ -25,6 +74,8 @@ type ControlFlow = "keep" | "remove-tree" | "remove-node"; export class TreeInfo { private view: TreeView; + private maxHeight: Map; + private numInferVars: Map; public constructor(private readonly tree: SerializedTree) { const childrenOf = (n: ProofNodeIdx) => { @@ -48,8 +99,10 @@ export class TreeInfo { return "keep"; } }; + this.view = makeTreeView(tree.root, cf, childrenOf); - console.debug("Tree abstracted view", this.view); + this.maxHeight = new Map(); + this.numInferVars = new Map(); } get topology(): TreeTopology { @@ -72,6 +125,17 @@ export class TreeInfo { return this.view.topology.children[n] ?? []; } + public result(n: ProofNodeIdx): EvaluationResult | undefined { + const node = this.node(n); + if ("Result" in node) { + return node.Result.data; + } else if ("Goal" in node) { + return node.Goal.data.result; + } else { + return undefined; + } + } + public pathToRoot(from: ProofNodeIdx): Path { const path = [from]; let current = from; @@ -108,6 +172,11 @@ export class TreeInfo { allLeaves, leaf => this.view.topology.parent[leaf] !== undefined ); + return viewLeaves; + } + + public errorNodesRecommendedOrder(): ProofNodeIdx[] { + const viewLeaves = this.errorNodes(); const sortErrorsFirst = (leaf: ProofNodeIdx) => { const node = this.tree.nodes[leaf]; @@ -147,55 +216,32 @@ export class TreeInfo { return recommendedOrder; } -} -function makeTreeView( - root: ProofNodeIdx, - cf: (n: ProofNodeIdx) => ControlFlow, - childrenOf: (n: ProofNodeIdx) => ProofNodeIdx[] -): TreeView { - const children: MultiRecord = {}; - const parent: Record = {}; - const addChildRel = (from: ProofNodeIdx, to: ProofNodeIdx) => { - if (children[from]) { - children[from].push(to); - } else { - children[from] = [to]; - } - if (parent[to]) { - throw new Error("parent already set"); + public inferVars(n: ProofNodeIdx): number { + const current = this.numInferVars.get(n); + if (current !== undefined) { + return current; } - parent[to] = from; - }; + const node = this.tree.nodes[n]; + const niv = _.reduce( + this.children(n), + (sum, k) => sum + this.inferVars(k), + "Goal" in node ? node.Goal.data.numVars : 0 + ); + this.numInferVars.set(n, niv); + return niv; + } - const iterate = (curr: ProofNodeIdx, prev?: ProofNodeIdx) => { - const kids = childrenOf(curr); - let newPrev = prev; - switch (cf(curr)) { - case "keep": { - if (prev !== undefined) { - addChildRel(prev, curr); - } - newPrev = curr; - break; - } - case "remove-node": - break; - case "remove-tree": - return; + public maxHeigh(n: ProofNodeIdx): number { + const current = this.maxHeight.get(n); + if (current !== undefined) { + return current; } - _.forEach(kids, kid => iterate(kid, newPrev)); - }; - - iterate(root); - - if (children[root] === undefined) { - throw new Error("Root has no children"); + const childHeights = _.map(this.children(n), k => this.maxHeigh(k)); + const height = 1 + (_.max(childHeights) ?? 0); + this.maxHeight.set(n, height); + return height; } - - return { - topology: { children, parent }, - }; } export default TreeInfo; diff --git a/ide/packages/panoptes/src/print/print.tsx b/ide/packages/panoptes/src/print/print.tsx index f258d5e..0cfd687 100644 --- a/ide/packages/panoptes/src/print/print.tsx +++ b/ide/packages/panoptes/src/print/print.tsx @@ -17,10 +17,9 @@ import { import { PrintTy as UnsafePrintTy } from "./private/ty"; // NOTE: please Please PLEASE wrap all printing components in this -// PrintWithFallback. Pretty printing is still a fragile process and -// I can never be sure if it's working correctly or not. -// -// Nothing should ever be imported from the 'private' directory except +// `PrintWithFallback`. Pretty printing is still a fragile process and +// I don't have full confidence in it yet. +// Nothing should be imported from the 'private' directory except // from within this file. export const PrintWithFallback = ({ object, @@ -81,10 +80,14 @@ export const PrintImplHeader = ({ impl }: { impl: any }) => { }; export const PrintGoal = ({ o }: { o: Goal }) => { + const debugString = + o.debugComparison === undefined ? null : ( +
{o.debugComparison}
+ ); const Content = () => ( <> - {/*
{o.debugComparison}
*/} + {debugString} ); return ; diff --git a/ide/packages/panoptes/src/print/private/const.tsx b/ide/packages/panoptes/src/print/private/const.tsx index 0e55d38..e571782 100644 --- a/ide/packages/panoptes/src/print/private/const.tsx +++ b/ide/packages/panoptes/src/print/private/const.tsx @@ -7,7 +7,7 @@ import { } from "@argus/common/bindings"; import React from "react"; -import { PrintValuePath } from "./path"; +import { PrintDefPath, PrintValuePath } from "./path"; import { PrintExpr, PrintValueTree } from "./term"; import { PrintBoundVariable, PrintSymbol } from "./ty"; @@ -57,9 +57,15 @@ const PrintUnevaluatedConst = ({ o }: { o: UnevaluatedConst }) => { case "AnonSnippet": { return o.data; } - // case "nonlocalpath": { - // throw new Error("todo"); - // } + case "AnonLocation": { + return ( + <> + + :: + + + ); + } default: throw new Error("Unknown unevaluated const kind", o); } diff --git a/ide/packages/panoptes/src/utilities/func.ts b/ide/packages/panoptes/src/utilities/func.ts index ba254ca..cd2796f 100644 --- a/ide/packages/panoptes/src/utilities/func.ts +++ b/ide/packages/panoptes/src/utilities/func.ts @@ -45,7 +45,7 @@ export function makeHighlightPosters(range: CharRange, file: Filename) { return [addHighlight, removeHighlight]; } -export function anyElems(...lists: T[][]) { +export function anyElems(...lists: any[][]) { return _.some(lists, l => l.length > 0); }