Alter heuristic for sorting BottomUp tree view.

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 }) => (
     <DirRecursive level={[leaf.root]} getNext={mkGetChildren(leaf)} />
   );
 
   const recommendedSortedViews = tree.sortByRecommendedOrder(
-    _.flatten(argusRecommended),
+    _.flatten(argusViews),
     v => v.root
   );
   const recommended = _.map(recommendedSortedViews, (leaf, i) => (
@@ -161,9 +243,7 @@ const BottomUp = () => {
       <CollapsibleElement
         info={<span>Other failures ...</span>}
         Children={() =>
-          _.map(_.flatten(others), (leaf, i) => (
-            <LeafElement key={i} leaf={leaf} />
-          ))
+          _.map(otherViews, (leaf, i) => <LeafElement key={i} leaf={leaf} />)
         }
       />
     );

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":

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) => {

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);
+}