diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index 1b9ebdb..86e084b 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx @@ -2,6 +2,7 @@ import { ProofNodeIdx, TreeTopology } from "@argus/common/bindings"; import _ from "lodash"; import React, { useContext } from "react"; +import { mean, mode, searchObject, stdDev } from "../utilities/func"; import { TreeContext } from "./Context"; import { CollapsibleElement, DirRecursive } from "./Directory"; import { TreeInfo, TreeView } from "./TreeInfo"; @@ -117,39 +118,120 @@ const BottomUp = () => { return curr; }; - const leaves = _.compact(_.map(tree.errorLeaves(), n => liftTo(n, "Goal"))); - const invertedViews = invertViewWithRoots(leaves, tree); - const groupedAndViews = _.groupBy(invertedViews, v => - liftTo(v.root, "Candidate") + const leaves = _.uniq( + _.compact(_.map(tree.errorLeaves(), n => liftTo(n, "Goal"))) ); + const failedGroups = _.groupBy(leaves, leaf => tree.parent(leaf)); + + // Operations on groups of errors + const numMainUninferred = (group: ProofNodeIdx[]) => + _.reduce( + group, + (acc, leaf) => + acc + + (() => { + const node = tree.node(leaf); + if ("Goal" in node) { + const goal = tree.goal(node.Goal); + return goal.isMainTv ? 1 : 0; + } else { + return 0; + } + })(), + 0 + ); + + const getNumPrincipaled = (group: ProofNodeIdx[]) => + group.length - numMainUninferred(group); + + const sortByNPT = (group: ProofNodeIdx[]) => -getNumPrincipaled(group); + + const sortByNPTRatio = (group: ProofNodeIdx[]) => + group.length / getNumPrincipaled(group); + + const sortByDepth = (group: ProofNodeIdx[]) => + -_.max(_.map(group, leaf => tree.depth(leaf)))!; + + const takeN = (n: number) => (groups: ProofNodeIdx[][]) => + [_.take(groups, n), _.tail(groups)] as [ProofNodeIdx[][], ProofNodeIdx[][]]; + + const takeAll = (groups: ProofNodeIdx[][]) => + [groups, []] as [ProofNodeIdx[][], ProofNodeIdx[][]]; + + // HACK: this crappy heuristic needs to be replaced with a proper analysis. + const [sortStrategy, firstFilter] = (() => { + const npts = _.map(failedGroups, getNumPrincipaled); + const meanNPT = mean(npts); + const stdDevNPT = stdDev(npts, meanNPT); + const onlyHigh = _.filter(npts, npt => npt > meanNPT + stdDevNPT); + if (onlyHigh.length > 0) { + return [sortByNPT, takeN(onlyHigh.length)]; + } + + const nptRatioEq = _.filter( + failedGroups, + group => group.length === getNumPrincipaled(group) + ); + if (nptRatioEq.length > 0) { + return [sortByNPTRatio, takeN(nptRatioEq.length)]; + } + + return [sortByDepth, takeAll]; + })(); + + const sortedGroups = _.sortBy(_.values(failedGroups), [ + // Getting the right group is important but it's not precise. + // We currently use the following metrics. + // + // 1. The number of obligations whose "principle types" are known (NPT). + // What this entails is that in an obligation such as `TYPE: TRAIT`, + // neither TYPE nor TRAIT is an unresolved type variable `_`. + // + // We use this number, NPT, to find groups whose NPT is more than + // one standard deviation from the mean. This is useful when trait impls are + // macro generated for varying arities, larger arities have a high number of + // unresolved type variables. + // + // The above is useful, until it isn't. Then, we can use tha ratio + // of group size vs the NPT. This favors smaller groups with more + // concrete types. + // + // 2. Depth of the group. Generally, deep obligations are "more interesting." + sortStrategy, + ]); + + const [importantGroups, rest] = firstFilter(sortedGroups); // 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( - _.values(groupedAndViews), - views => - _.every(views, view => { - const node = tree.node(view.root); - if ("Goal" in node) { - const goal = tree.goal(node.Goal); - const result = tree.result(goal.result); - return ( - !goal.isMainTv && (result === "no" || result === "maybe-overflow") - ); - } else { - // Leaves should only be goals... - throw new Error(`Leaves should only be goals ${node}`); - } - }) + const [argusRecommendedLeaves, others] = _.partition( + _.flatten(importantGroups), + leaf => { + const node = tree.node(leaf); + if ("Goal" in node) { + const goal = tree.goal(node.Goal); + const result = tree.result(goal.result); + return ( + !goal.isMainTv && (result === "no" || result === "maybe-overflow") + ); + } else { + // Leaves should only be goals... + throw new Error(`Leaves should only be goals ${node}`); + } + } ); + const hiddenLeaves = _.concat(_.flatten(rest), others); + const argusViews = invertViewWithRoots(argusRecommendedLeaves, tree); + const otherViews = invertViewWithRoots(hiddenLeaves, tree); + const LeafElement = ({ leaf }: { leaf: TreeViewWithRoot }) => ( ); const recommendedSortedViews = tree.sortByRecommendedOrder( - _.flatten(argusRecommended), + _.flatten(argusViews), v => v.root ); const recommended = _.map(recommendedSortedViews, (leaf, i) => ( @@ -161,9 +243,7 @@ const BottomUp = () => { Other failures ...} Children={() => - _.map(_.flatten(others), (leaf, i) => ( - - )) + _.map(otherViews, (leaf, i) => ) } /> ); diff --git a/ide/packages/panoptes/src/TreeView/TopDown.tsx b/ide/packages/panoptes/src/TreeView/TopDown.tsx index 1f6dc4c..4d908a9 100644 --- a/ide/packages/panoptes/src/TreeView/TopDown.tsx +++ b/ide/packages/panoptes/src/TreeView/TopDown.tsx @@ -84,10 +84,10 @@ const TopDown = () => { 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 => { + // const node = tree.node(k); + // return "Goal" in node && tree.goal(node.Goal).isMainTv ? 1 : 0; + // }, k => { switch (tree.nodeResult(k)) { case "no": diff --git a/ide/packages/panoptes/src/TreeView/TreeInfo.ts b/ide/packages/panoptes/src/TreeView/TreeInfo.ts index fe32ea8..2991c42 100644 --- a/ide/packages/panoptes/src/TreeView/TreeInfo.ts +++ b/ide/packages/panoptes/src/TreeView/TreeInfo.ts @@ -133,6 +133,15 @@ export class TreeInfo { return this.tree.nodes[n]; } + public depth(n: ProofNodeIdx) { + return this.pathToRoot(n).path.length; + } + + public goalOfNode(n: ProofNodeIdx) { + const node = this.node(n); + return "Goal" in node ? this.goal(node.Goal) : undefined; + } + public candidate(n: CandidateIdx): CandidateData { return this.tree.candidates[n]; } @@ -241,7 +250,13 @@ export class TreeInfo { const leaf = f(t); const pathToRoot = this.pathToRoot(leaf); const len = pathToRoot.path.length; - return -len; + const numVars = _.reduce( + pathToRoot.path, + (sum, k) => sum + this.inferVars(k), + 0 + ); + + return numVars / len; }; const bubbleTraitClauses = (t: T) => { diff --git a/ide/packages/panoptes/src/utilities/func.ts b/ide/packages/panoptes/src/utilities/func.ts index ff12f46..404f9c1 100644 --- a/ide/packages/panoptes/src/utilities/func.ts +++ b/ide/packages/panoptes/src/utilities/func.ts @@ -110,3 +110,33 @@ export function isHiddenObl(o: { necessity: string; result: string }) { o.necessity === "Yes" || (o.necessity === "OnError" && o.result === "no") ); } + +export function searchObject(obj: any, target: any) { + for (let key in obj) { + if (obj[key] === target) { + return true; + } + + if (typeof obj[key] === "object" && obj[key] !== null) { + if (searchObject(obj[key], target)) { + return true; + } + } + } + + return obj === target; +} + +export function mean(arr: number[]) { + return _.sum(arr) / arr.length; +} + +export function mode(arr: number[]) { + const counts = _.countBy(arr); + const max = _.max(_.values(counts)); + return _.findKey(counts, v => v === max); +} + +export function stdDev(arr: number[], avg: number) { + return Math.sqrt(_.sum(_.map(arr, n => Math.pow(n - avg, 2))) / arr.length); +}