From 3ccc92bdb96dbc964c5b1fef2b94e7033d6fac4b Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Sun, 29 Mar 2026 15:17:21 +0100
Subject: [PATCH] Add IteDerivationNode

---
 client/src/types/derivation-nodes.ts                | 13 ++++++++++++-
 .../webview/views/diagnostics/derivation-nodes.ts   | 10 +++++++++-
 client/src/webview/views/diagnostics/errors.ts      |  2 +-
 3 files changed, 22 insertions(+), 3 deletions(-)

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 `<span class="node-value">${JSON.stringify(node)}</span>`;
 }
@@ -114,7 +122,7 @@ export function renderDerivationNode(error: RefinementError, node: ValDerivation
     return /*html*/ `
         <div class="container derivation-container" data-error-id="${errorId}">
             <div style="flex: 1;">
-                ${renderJsonTree(error, node.origin || node, errorId, "root", expansions)}
+                ${renderJsonTree(error, node, errorId, "root", expansions)}
                 ${expansions.size === 0 ? '<span class="node-expand-indicator">&nbsp;(click to expand)</span>' : ''}
             </div>
             <button class="reset-btn derivation-reset-btn" data-error-id="${errorId}" ${expansions.size === 0 ? "disabled" : ""}>
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index da3f944..22b0743 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -31,7 +31,7 @@ export function renderErrors(errors: LJError[], expandedErrors: Set<number>): st
 const errorContentRenderers: Partial<Record<LJError['type'], (error: LJError) => string>> = {
     'refinement-error': (e: RefinementError) => /*html*/`
         ${e.customMessage ? renderSection('Message', e.customMessage) : ''}
-        ${renderSection('Expected', e.expected.value)}
+        ${renderCustomSection('Expected', renderDerivationNode(e, e.expected))}
         ${renderCustomSection('Found', renderDerivationNode(e, e.found))}
         ${e.counterexample ? renderSection('Counterexample', e.counterexample) : ''}
     `,