Grouping top-down obligations by result.

ide/packages/panoptes/src/TreeView/TopDown.tsx

@@ -10,7 +10,7 @@ import {
   useInteractions,
 } from "@floating-ui/react";
 import classNames from "classnames";
-import _ from "lodash";
+import _, { sortBy } from "lodash";
 import React, { useContext, useState } from "react";
 
 import { IcoTreeDown } from "../Icons";
@@ -80,21 +80,16 @@ const TopDown = () => {
 
   // Sort the candidates by the #infer vars / height of the tree
   const getGoalChildren = (kids: ProofNodeIdx[]) =>
-    _.sortBy(kids, k => {
-      const inferVars = tree.inferVars(k);
-      const height = tree.maxHeigh(k);
-      return inferVars / height;
-    });
+    _.sortBy(kids, [k => -tree.maxHeight(k)]);
 
   const getCandidateChildren = (kids: ProofNodeIdx[]) =>
-    _.sortBy(
-      kids,
+    _.sortBy(_.uniq(kids), [
       k => {
         const node = tree.node(k);
         return "Goal" in node && tree.goal(node.Goal).isMainTv ? 1 : 0;
       },
       k => {
-        switch (tree.result(k) ?? "yes") {
+        switch (tree.nodeResult(k)) {
           case "no":
             return 0;
           case "maybe-overflow":
@@ -106,8 +101,8 @@ const TopDown = () => {
           default:
             return 4;
         }
-      }
-    );
+      },
+    ]);
 
   const getChildren = (idx: ProofNodeIdx) => {
     const node = tree.node(idx);

ide/packages/panoptes/src/TreeView/TreeInfo.ts

@@ -78,7 +78,7 @@ export interface TreeView {
 type ControlFlow = "keep" | "remove-tree" | "remove-node";
 
 export class TreeInfo {
-  private maxHeight: Map<ProofNodeIdx, number>;
+  private _maxHeight: Map<ProofNodeIdx, number>;
   private numInferVars: Map<ProofNodeIdx, number>;
 
   static new(tree: SerializedTree, showHidden: boolean = false) {
@@ -117,7 +117,7 @@ export class TreeInfo {
     readonly showHidden: boolean = false,
     readonly view: TreeView
   ) {
-    this.maxHeight = new Map();
+    this._maxHeight = new Map();
     this.numInferVars = new Map();
   }
 
@@ -282,14 +282,14 @@ export class TreeInfo {
     return niv;
   }
 
-  public maxHeigh(n: ProofNodeIdx): number {
-    const current = this.maxHeight.get(n);
+  public maxHeight(n: ProofNodeIdx): number {
+    const current = this._maxHeight.get(n);
     if (current !== undefined) {
       return current;
     }
-    const childHeights = _.map(this.children(n), k => this.maxHeigh(k));
+    const childHeights = _.map(this.children(n), k => this.maxHeight(k));
     const height = 1 + (_.max(childHeights) ?? 0);
-    this.maxHeight.set(n, height);
+    this._maxHeight.set(n, height);
     return height;
   }
 }