From cda0077bdaf377edfef103ffa012952ffa81b776 Mon Sep 17 00:00:00 2001 From: Gavin Gray Date: Mon, 26 Feb 2024 15:29:01 +0100 Subject: [PATCH] Intern candidates and results in proof tree. --- crates/argus/src/proof_tree/interners.rs | 220 ++++++++++++++++++ crates/argus/src/proof_tree/mod.rs | 57 +++-- crates/argus/src/proof_tree/serialize.rs | 143 ++---------- crates/argus/src/ts.rs | 2 + ide/packages/panoptes/src/File.tsx | 10 +- .../panoptes/src/TreeView/BottomUp.tsx | 2 +- ide/packages/panoptes/src/TreeView/Node.tsx | 21 +- .../panoptes/src/TreeView/TreeInfo.ts | 22 +- 8 files changed, 304 insertions(+), 173 deletions(-) create mode 100644 crates/argus/src/proof_tree/interners.rs diff --git a/crates/argus/src/proof_tree/interners.rs b/crates/argus/src/proof_tree/interners.rs new file mode 100644 index 0000000..de2a332 --- /dev/null +++ b/crates/argus/src/proof_tree/interners.rs @@ -0,0 +1,220 @@ +use std::{ + cmp::{Eq, PartialEq}, + hash::Hash, +}; + +use index_vec::{Idx, IndexVec}; +use rustc_data_structures::{fx::FxHashMap as HashMap, stable_hasher::Hash64}; +use rustc_hir::def_id::DefId; +use rustc_infer::infer::InferCtxt; +use rustc_trait_selection::{ + solve::inspect::{InspectCandidate, InspectGoal}, + traits::{ + solve, + solve::{inspect::ProbeKind, CandidateSource}, + }, +}; + +use super::*; +use crate::{ext::TyCtxtExt, types::intermediate::EvaluationResult}; + +#[derive(Default)] +struct Interner { + values: IndexVec, + keys: HashMap, +} + +impl Interner +where + K: PartialEq + Eq + Hash, + I: Idx, +{ + fn default() -> Self { + Self { + values: IndexVec::default(), + keys: HashMap::default(), + } + } + + fn get(&mut self, key: K) -> Option { + self.keys.get(&key).cloned() + } + + fn insert(&mut self, k: K, d: D) -> I { + let idx = self.values.push(d); + self.keys.insert(k, idx); + idx + } + + fn insert_no_key(&mut self, d: D) -> I { + self.values.push(d) + } +} + +pub struct Interners { + goals: Interner<(Hash64, ResultIdx), GoalIdx, GoalData>, + candidates: Interner, + results: Interner, +} + +#[derive(PartialEq, Eq, Hash)] +enum CanKey { + Impl(DefId), + ParamEnv(usize), + Str(&'static str), +} + +impl Interners { + pub fn default() -> Self { + Self { + goals: Interner::default(), + candidates: Interner::default(), + results: Interner::default(), + } + } + + pub fn take( + self, + ) -> ( + IndexVec, + IndexVec, + IndexVec, + ) { + ( + self.goals.values, + self.candidates.values, + self.results.values, + ) + } + + pub fn mk_result_node(&mut self, result: EvaluationResult) -> Node { + Node::Result(self.intern_result(result)) + } + + pub fn mk_goal_node<'tcx>(&mut self, goal: &InspectGoal<'_, 'tcx>) -> Node { + let infcx = goal.infcx(); + let result_idx = self.intern_result(goal.result()); + let goal = goal.goal(); + let goal_idx = self.intern_goal(infcx, &goal, result_idx); + Node::Goal(goal_idx, result_idx) + } + + pub fn mk_candidate_node<'tcx>( + &mut self, + candidate: &InspectCandidate<'_, 'tcx>, + ) -> Node { + let can_idx = match candidate.kind() { + ProbeKind::Root { .. } => self.intern_can_string("root"), + ProbeKind::NormalizedSelfTyAssembly => { + self.intern_can_string("normalized-self-ty-asm") + } + ProbeKind::UnsizeAssembly => self.intern_can_string("unsize-asm"), + ProbeKind::CommitIfOk => self.intern_can_string("commit-if-ok"), + ProbeKind::UpcastProjectionCompatibility => { + self.intern_can_string("upcase-proj-compat") + } + ProbeKind::MiscCandidate { .. } => self.intern_can_string("misc"), + ProbeKind::TraitCandidate { source, .. } => match source { + CandidateSource::BuiltinImpl(_built_impl) => { + self.intern_can_string("builtin") + } + CandidateSource::AliasBound => self.intern_can_string("alias-bound"), + // The only two we really care about. + CandidateSource::ParamEnv(idx) => self.intern_can_param_env(idx), + + CandidateSource::Impl(def_id) => { + self.intern_impl(candidate.infcx(), def_id) + } + }, + }; + + Node::Candidate(can_idx) + } + + fn intern_result(&mut self, result: EvaluationResult) -> ResultIdx { + if let Some(result_idx) = self.results.get(result) { + return result_idx; + } + + self.results.insert(result, ResultData(result)) + } + + fn intern_goal<'tcx>( + &mut self, + infcx: &InferCtxt<'tcx>, + goal: &solve::Goal<'tcx, ty::Predicate<'tcx>>, + result_idx: ResultIdx, + ) -> GoalIdx { + let goal = infcx.resolve_vars_if_possible(*goal); + let hash = infcx.predicate_hash(&goal.predicate); + let hash = (hash, result_idx); + if let Some(goal_idx) = self.goals.get(hash) { + return goal_idx; + } + + let necessity = infcx.guess_predicate_necessity(&goal.predicate); + let num_vars = + serialize::var_counter::count_vars(infcx.tcx, goal.predicate); + let is_lhs_ty_var = goal.predicate.is_lhs_ty_var(); + let goal_value = serialize_to_value(infcx, &GoalPredicateDef(goal)) + .expect("failed to serialize goal"); + + self.goals.insert(hash, GoalData { + value: goal_value, + necessity, + num_vars, + is_lhs_ty_var, + + #[cfg(debug_assertions)] + debug_comparison: format!("{:?}", goal.predicate.kind().skip_binder()), + }) + } + + fn intern_can_string(&mut self, s: &'static str) -> CandidateIdx { + if let Some(i) = self.candidates.get(CanKey::Str(s)) { + return i; + } + + self.candidates.insert(CanKey::Str(s), s.into()) + } + + fn intern_can_param_env(&mut self, idx: usize) -> CandidateIdx { + if let Some(i) = self.candidates.get(CanKey::ParamEnv(idx)) { + return i; + } + + self + .candidates + .insert(CanKey::ParamEnv(idx), CandidateData::ParamEnv(idx)) + } + + fn intern_impl(&mut self, infcx: &InferCtxt, def_id: DefId) -> CandidateIdx { + if let Some(i) = self.candidates.get(CanKey::Impl(def_id)) { + return i; + } + + let tcx = infcx.tcx; + + // First, try to get an impl header from the def_id ty + if let Some(header) = tcx.get_impl_header(def_id) { + return self.candidates.insert( + CanKey::Impl(def_id), + CandidateData::new_impl_header(infcx, &header), + ); + } + + // Second, try to get the span of the impl or just default to a fallback. + let string = tcx + .span_of_impl(def_id) + .map(|sp| { + tcx + .sess + .source_map() + .span_to_snippet(sp) + .unwrap_or_else(|_| "failed to find impl".to_string()) + }) + .unwrap_or_else(|symb| format!("foreign impl from: {}", symb.as_str())); + + self.candidates.insert_no_key(CandidateData::from(string)) + } +} diff --git a/crates/argus/src/proof_tree/mod.rs b/crates/argus/src/proof_tree/mod.rs index 5e874c2..4e73edb 100644 --- a/crates/argus/src/proof_tree/mod.rs +++ b/crates/argus/src/proof_tree/mod.rs @@ -1,6 +1,7 @@ //! Proof tree types sent to the Argus frontend. pub mod ext; +pub(self) mod interners; pub(super) mod serialize; pub mod topology; @@ -26,7 +27,9 @@ use crate::{ crate::define_idx! { usize, ProofNodeIdx, - GoalIdx + GoalIdx, + CandidateIdx, + ResultIdx } // FIXME: Nodes shouldn't be PartialEq, or Eq. They are currently @@ -38,29 +41,15 @@ crate::define_idx! { #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export))] pub enum Node { - Result( - #[serde(with = "EvaluationResultDef")] - #[cfg_attr(feature = "testing", ts(type = "EvaluationResult"))] - EvaluationResult, - ), - Candidate(Candidate), - Goal( - GoalIdx, - #[serde(with = "EvaluationResultDef")] - #[cfg_attr(feature = "testing", ts(type = "EvaluationResult"))] - EvaluationResult, - ), + Result(ResultIdx), + Candidate(CandidateIdx), + Goal(GoalIdx, ResultIdx), } #[derive(Serialize, Clone, Debug, PartialEq, Eq)] #[cfg_attr(feature = "testing", derive(TS))] #[cfg_attr(feature = "testing", ts(export))] -pub struct Goal {} - -#[derive(Serialize, Clone, Debug, PartialEq, Eq)] -#[cfg_attr(feature = "testing", derive(TS))] -#[cfg_attr(feature = "testing", ts(export))] -pub enum Candidate { +pub enum CandidateData { Impl( #[cfg_attr(feature = "testing", ts(type = "ImplHeader"))] serde_json::Value, ), @@ -69,6 +58,15 @@ pub enum Candidate { Any(String), } +#[derive(Serialize, Clone, Debug, PartialEq, Eq)] +#[cfg_attr(feature = "testing", derive(TS))] +#[cfg_attr(feature = "testing", ts(export))] +pub struct ResultData( + #[serde(with = "EvaluationResultDef")] + #[cfg_attr(feature = "testing", ts(type = "EvaluationResult"))] + EvaluationResult, +); + #[derive(Serialize, Debug, Clone)] #[serde(rename_all = "camelCase")] #[cfg_attr(feature = "testing", derive(TS))] @@ -95,9 +93,16 @@ pub struct SerializedTree { #[cfg_attr(feature = "testing", ts(type = "Node[]"))] pub nodes: IndexVec, + #[cfg_attr(feature = "testing", ts(type = "GoalData[]"))] pub goals: IndexVec, + #[cfg_attr(feature = "testing", ts(type = "CandidateData[]"))] + pub candidates: IndexVec, + + #[cfg_attr(feature = "testing", ts(type = "ResultData[]"))] + pub results: IndexVec, + pub topology: TreeTopology, pub error_leaves: Vec, pub unnecessary_roots: HashSet, @@ -113,31 +118,25 @@ pub struct ProofCycle(Vec); // ---------------------------------------- // impls -impl Candidate { +impl CandidateData { fn new_impl_header<'tcx>( infcx: &InferCtxt<'tcx>, impl_: &ImplHeader<'tcx>, ) -> Self { let impl_ = serialize_to_value(infcx, impl_).expect("couldn't serialize impl header"); - Self::Impl(impl_) } - - // TODO: we should pass the ParamEnv here for certainty. - fn new_param_env(idx: usize) -> Self { - Self::ParamEnv(idx) - } } -impl From<&'static str> for Candidate { +impl From<&'static str> for CandidateData { fn from(value: &'static str) -> Self { value.to_string().into() } } -impl From for Candidate { +impl From for CandidateData { fn from(value: String) -> Self { - Candidate::Any(value) + Self::Any(value) } } diff --git a/crates/argus/src/proof_tree/serialize.rs b/crates/argus/src/proof_tree/serialize.rs index 530758a..5d35317 100644 --- a/crates/argus/src/proof_tree/serialize.rs +++ b/crates/argus/src/proof_tree/serialize.rs @@ -3,63 +3,15 @@ use std::{collections::HashSet, ops::ControlFlow}; use anyhow::{bail, Result}; use ext::{CandidateExt, EvaluationResultExt}; use index_vec::IndexVec; -use rustc_data_structures::{fx::FxHashMap as HashMap, stable_hasher::Hash64}; use rustc_hir::def_id::DefId; use rustc_infer::infer::InferCtxt; use rustc_middle::ty::Predicate; use rustc_trait_selection::{ - solve::inspect::{ - InspectCandidate, InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor, - }, + solve::inspect::{InspectGoal, ProofTreeInferCtxtExt, ProofTreeVisitor}, traits::solve, }; -use super::*; -use crate::{ext::TyCtxtExt, types::intermediate::EvaluationResult}; - -#[derive(Default)] -struct GoalInterner { - goals: IndexVec, - keys: HashMap, -} - -impl GoalInterner { - pub fn intern<'tcx>( - &mut self, - infcx: &InferCtxt<'tcx>, - goal: &solve::Goal<'tcx, ty::Predicate<'tcx>>, - ) -> GoalIdx { - let goal = infcx.resolve_vars_if_possible(*goal); - let hash = infcx.predicate_hash(&goal.predicate); - if let Some(goal_idx) = self.keys.get(&hash) { - return *goal_idx; - } - - let necessity = infcx.guess_predicate_necessity(&goal.predicate); - let num_vars = - serialize::var_counter::count_vars(infcx.tcx, goal.predicate); - let is_lhs_ty_var = goal.predicate.is_lhs_ty_var(); - let goal_value = serialize_to_value(infcx, &GoalPredicateDef(goal)) - .expect("failed to serialize goal"); - - let idx = self.goals.push(GoalData { - value: goal_value, - necessity, - num_vars, - is_lhs_ty_var, - - #[cfg(debug_assertions)] - debug_comparison: format!("{:?}", goal.predicate.kind().skip_binder()), - }); - - self.keys.insert(hash, idx); - idx - } - - pub fn take_goals(self) -> IndexVec { - self.goals - } -} +use super::{interners::Interners, *}; pub struct SerializedTreeVisitor { pub def_id: DefId, @@ -70,7 +22,7 @@ pub struct SerializedTreeVisitor { pub error_leaves: Vec, pub unnecessary_roots: HashSet, pub cycle: Option, - interner: GoalInterner, + interners: Interners, } impl SerializedTreeVisitor { @@ -84,7 +36,7 @@ impl SerializedTreeVisitor { error_leaves: Vec::default(), unnecessary_roots: HashSet::default(), cycle: None, - interner: Default::default(), + interners: Interners::default(), } } @@ -96,16 +48,20 @@ impl SerializedTreeVisitor { error_leaves, unnecessary_roots, cycle, - interner, + interners, .. } = self else { bail!("missing root node!"); }; + let (goals, candidates, results) = interners.take(); + Ok(SerializedTree { root, - goals: interner.take_goals(), + goals, + candidates, + results, nodes, topology, error_leaves, @@ -115,9 +71,9 @@ impl SerializedTreeVisitor { } // TODO: cycle detection is too expensive for large trees, and strictly - // comparing the JSON values is a bad idea in general. We should wait - // until the new trait solver has some mechanism for detecting cycles - // and piggy back off that. + // comparing the JSON values is a bad idea in general. (This is what comparing + // interned keys does essentially). We should wait until the new trait solver + // has some mechanism for detecting cycles and piggy back off that. fn check_for_cycle_from(&mut self, from: ProofNodeIdx) { if self.cycle.is_some() { return; @@ -138,73 +94,6 @@ impl SerializedTreeVisitor { self.cycle = Some(to_root.into()); } } - - fn mk_goal_node<'tcx>(&mut self, goal: &InspectGoal<'_, 'tcx>) -> Node { - let infcx = goal.infcx(); - let result = goal.result(); - let goal = goal.goal(); - let goal_idx = self.interner.intern(infcx, &goal); - Node::Goal(goal_idx, result) - } -} - -impl Node { - fn from_candidate<'tcx>( - candidate: &InspectCandidate<'_, 'tcx>, - _def_id: DefId, - ) -> Self { - use rustc_trait_selection::traits::solve::{ - inspect::ProbeKind, CandidateSource, - }; - - let can = match candidate.kind() { - ProbeKind::Root { .. } => "root".into(), - ProbeKind::NormalizedSelfTyAssembly => "normalized-self-ty-asm".into(), - ProbeKind::UnsizeAssembly => "unsize-asm".into(), - ProbeKind::CommitIfOk => "commit-if-ok".into(), - ProbeKind::UpcastProjectionCompatibility => "upcase-proj-compat".into(), - ProbeKind::MiscCandidate { .. } => "misc".into(), - ProbeKind::TraitCandidate { source, .. } => match source { - CandidateSource::BuiltinImpl(_built_impl) => "builtin".into(), - CandidateSource::AliasBound => "alias-bound".into(), - // The only two we really care about. - CandidateSource::ParamEnv(idx) => Candidate::new_param_env(idx), - CandidateSource::Impl(def_id) => { - Self::from_impl(candidate.infcx(), def_id) - } - }, - }; - - Node::Candidate(can) - } - - fn from_impl(infcx: &InferCtxt, def_id: DefId) -> Candidate { - let tcx = infcx.tcx; - // First, try to get an impl header from the def_id ty - tcx - .get_impl_header(def_id) - .map(|header| Candidate::new_impl_header(infcx, &header)) - // Second, scramble to find a suitable span, or some error string. - .unwrap_or_else(|| { - tcx - .span_of_impl(def_id) - .map(|sp| { - tcx - .sess - .source_map() - .span_to_snippet(sp) - .unwrap_or_else(|_| "failed to find impl".to_string()) - }) - .unwrap_or_else(|symb| { - format!("foreign impl from: {}", symb.as_str()) - }) - .into() - }) - } - - fn from_result(result: &EvaluationResult) -> Self { - Node::Result(result.clone()) - } } impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor { @@ -214,7 +103,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor { &mut self, goal: &InspectGoal<'_, 'tcx>, ) -> ControlFlow { - let here_node = self.mk_goal_node(goal); + let here_node = self.interners.mk_goal_node(goal); let here_idx = self.nodes.push(here_node.clone()); @@ -235,7 +124,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor { self.previous = Some(here_idx); for c in goal.candidates() { - let here_candidate = Node::from_candidate(&c, self.def_id); + let here_candidate = self.interners.mk_candidate_node(&c); let candidate_idx = self.nodes.push(here_candidate); let prev_idx = if c.is_informative_probe() { @@ -250,7 +139,7 @@ impl<'tcx> ProofTreeVisitor<'tcx> for SerializedTreeVisitor { if self.topology.is_leaf(prev_idx) { let result = goal.result(); - let leaf = Node::from_result(&result); + let leaf = self.interners.mk_result_node(result); let leaf_idx = self.nodes.push(leaf); self.topology.add(prev_idx, leaf_idx); if !result.is_yes() { diff --git a/crates/argus/src/ts.rs b/crates/argus/src/ts.rs index 4519d54..7fffca5 100644 --- a/crates/argus/src/ts.rs +++ b/crates/argus/src/ts.rs @@ -20,6 +20,8 @@ fn export_bindings_indices() { pty::ProofNodeIdx, pty::GoalIdx, + pty::CandidateIdx, + pty::ResultIdx, } } diff --git a/ide/packages/panoptes/src/File.tsx b/ide/packages/panoptes/src/File.tsx index 7446362..ad712b9 100644 --- a/ide/packages/panoptes/src/File.tsx +++ b/ide/packages/panoptes/src/File.tsx @@ -25,7 +25,7 @@ import React, { import BodyInfo from "./BodyInfo"; import "./File.css"; import { CollapsibleElement } from "./TreeView/Directory"; -import { Result } from "./TreeView/Node"; +import { ResultRaw } from "./TreeView/Node"; import TreeApp from "./TreeView/TreeApp"; import { WaitingOn } from "./WaitingOn"; import { @@ -131,7 +131,7 @@ const ObligationCard = ({ onMouseEnter={addHighlight} onMouseLeave={removeHighlight} > - + ); @@ -158,7 +158,7 @@ const ObligationFromIdx = ({ idx }: { idx: ObligationIdx }) => { const ObligationResultFromIdx = ({ idx }: { idx: ObligationIdx }) => { const bodyInfo = useContext(BodyInfoContext)!; const o = bodyInfo.getObligation(idx); - return ; + return ; }; const MethodLookupTable = ({ lookup }: { lookup: MethodLookupIdx }) => { @@ -274,10 +274,10 @@ const ObligationBody = ({ bodyInfo }: { bodyInfo: BodyInfo }) => { ); const header = ( - + <> {bodyName} {errCount > 0 ? ({errCount}) : null} - + ); const openChildren = bodyInfo.hash === highlightedObligation.value?.bodyIdx; diff --git a/ide/packages/panoptes/src/TreeView/BottomUp.tsx b/ide/packages/panoptes/src/TreeView/BottomUp.tsx index 70de336..4e57fa8 100644 --- a/ide/packages/panoptes/src/TreeView/BottomUp.tsx +++ b/ide/packages/panoptes/src/TreeView/BottomUp.tsx @@ -108,7 +108,7 @@ const BottomUp = () => { const node = tree.node(view.root); if ("Goal" in node) { const goal = tree.goal(node.Goal[0]); - const result = node.Goal[1]; + const result = tree.result(node.Goal[1]); return result === "no" || result === "maybe-overflow" || !goal.isLhsTyVar; } else { // Leaves should only be goals... diff --git a/ide/packages/panoptes/src/TreeView/Node.tsx b/ide/packages/panoptes/src/TreeView/Node.tsx index 8e33745..7974019 100644 --- a/ide/packages/panoptes/src/TreeView/Node.tsx +++ b/ide/packages/panoptes/src/TreeView/Node.tsx @@ -1,7 +1,8 @@ import { - Candidate as CandidateTy, + CandidateIdx, EvaluationResult, Node as NodeTy, + ResultIdx, } from "@argus/common/bindings"; import React, { useContext } from "react"; @@ -10,7 +11,7 @@ import { IcoAmbiguous, IcoCheck, IcoError, IcoLoop } from "../Icons"; import { PrintGoal, PrintImplHeader } from "../print/print"; import { TreeContext } from "./Context"; -export const Result = ({ result }: { result: EvaluationResult }) => { +export const ResultRaw = ({ result }: { result: EvaluationResult }) => { return result === "yes" ? ( Proved true}> @@ -38,7 +39,15 @@ export const Result = ({ result }: { result: EvaluationResult }) => { ); }; -export const Candidate = ({ candidate }: { candidate: CandidateTy }) => { +export const Result = ({ idx }: { idx: ResultIdx }) => { + const tree = useContext(TreeContext)!; + const result = tree.result(idx); + return ; +}; + +export const Candidate = ({ idx }: { idx: CandidateIdx }) => { + const tree = useContext(TreeContext)!; + const candidate = tree.candidate(idx); if ("Any" in candidate) { return candidate.Any; } else if ("Impl" in candidate) { @@ -53,16 +62,16 @@ export const Candidate = ({ candidate }: { candidate: CandidateTy }) => { export const Node = ({ node }: { node: NodeTy }) => { const treeInfo = useContext(TreeContext)!; if ("Result" in node) { - return ; + return ; } else if ("Goal" in node) { return ( <> - + ); } else if ("Candidate" in node) { - return ; + return ; } else { throw new Error("Unknown node type", node); } diff --git a/ide/packages/panoptes/src/TreeView/TreeInfo.ts b/ide/packages/panoptes/src/TreeView/TreeInfo.ts index 4cd4032..e324cc2 100644 --- a/ide/packages/panoptes/src/TreeView/TreeInfo.ts +++ b/ide/packages/panoptes/src/TreeView/TreeInfo.ts @@ -1,7 +1,10 @@ import { + CandidateData, + CandidateIdx, EvaluationResult, GoalIdx, ProofNodeIdx, + ResultIdx, SerializedTree, TreeTopology, } from "@argus/common/bindings"; @@ -99,7 +102,8 @@ export class TreeInfo { return "remove-tree"; } } else if ("Candidate" in node) { - if ("Any" in node.Candidate) { + const candidate = this.candidate(node.Candidate); + if ("Any" in candidate) { return "remove-node"; } else { return "keep"; @@ -126,6 +130,10 @@ export class TreeInfo { return this.tree.nodes[n]; } + public candidate(n: CandidateIdx): CandidateData { + return this.tree.candidates[n]; + } + public goal(n: GoalIdx) { return this.tree.goals[n]; } @@ -138,12 +146,16 @@ export class TreeInfo { return this.view.topology.children[n] ?? []; } - public result(n: ProofNodeIdx): EvaluationResult | undefined { + public result(n: ResultIdx): EvaluationResult { + return this.tree.results[n]; + } + + public nodeResult(n: ProofNodeIdx): EvaluationResult | undefined { const node = this.node(n); if ("Result" in node) { - return node.Result; + return this.result(node.Result); } else if ("Goal" in node) { - return node.Goal[1]; + return this.result(node.Goal[1]); } else { return undefined; } @@ -194,7 +206,7 @@ export class TreeInfo { const sortErrorsFirst = (leaf: ProofNodeIdx) => { const node = this.tree.nodes[leaf]; if ("Result" in node) { - switch (node.Result) { + switch (this.result(node.Result)) { case "no": return 0; case "maybe-overflow":