diff --git a/client/src/types/derivation-nodes.ts b/client/src/types/derivation-nodes.ts index 3b6b8ae..f06386c 100644 --- a/client/src/types/derivation-nodes.ts +++ b/client/src/types/derivation-nodes.ts @@ -1,6 +1,11 @@ // Type definitions used in refinement errors for expanding node simplifications -export type DerivationNode = ValDerivationNode | VarDerivationNode | BinaryDerivationNode | UnaryDerivationNode; +export type DerivationNode = + | ValDerivationNode + | VarDerivationNode + | BinaryDerivationNode + | UnaryDerivationNode + | IteDerivationNode; export type ValDerivationNode = { value: any; @@ -22,3 +27,9 @@ export type UnaryDerivationNode = { op: string; operand: ValDerivationNode; } + +export type IteDerivationNode = { + condition: ValDerivationNode; + thenBranch: ValDerivationNode; + elseBranch: ValDerivationNode; +} diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts index fcd6897..e8ad46c 100644 --- a/client/src/webview/views/diagnostics/derivation-nodes.ts +++ b/client/src/webview/views/diagnostics/derivation-nodes.ts @@ -65,6 +65,14 @@ function renderJsonTree( return node.op === "-" ? `${node.op}(${operandHtml})` : `${node.op}${operandHtml}`; } + // IteDerivationNode + if ("condition" in node && "thenBranch" in node && "elseBranch" in node) { + const conditionHtml = renderJsonTree(error, node.condition, errorId, `${path}.condition`, expandedPaths); + const thenBranchHtml = renderJsonTree(error, node.thenBranch, errorId, `${path}.thenBranch`, expandedPaths); + const elseBranchHtml = renderJsonTree(error, node.elseBranch, errorId, `${path}.elseBranch`, expandedPaths); + return `${conditionHtml} ? ${thenBranchHtml} : ${elseBranchHtml}`; + } + // fallback return `${JSON.stringify(node)}`; } @@ -114,7 +122,7 @@ export function renderDerivationNode(error: RefinementError, node: ValDerivation return /*html*/ `