Skip to main content

lemma/evaluation/
explanations.rs

1//! Root explanation type and formatting.
2//!
3//! The root `Explanation` (with `result: OperationResult`) is built once per
4//! requested rule from its narrated Rule node. The tree types (`ExplanationNode`,
5//! `Cause`, `SerializedConversionTraceStep`) live in `planning::explanation`;
6//! `evaluation::narration` builds them from the filled value table.
7
8use crate::computation::{OperationResult, VetoType};
9use crate::planning::semantics::{LemmaType, RulePath};
10use serde::Serialize;
11use std::sync::Arc;
12
13// Re-export tree types for use within the evaluation module
14pub use crate::planning::explanation::{
15    Cause, ConversionTraceRole, ExplanationNode, SerializedConversionTraceStep,
16};
17
18#[derive(Debug, Clone)]
19pub struct Explanation {
20    pub name: RulePath,
21    pub result: OperationResult,
22    /// Type of [`Self::result`] for measure/ratio display (binding unit, decimals).
23    pub result_type: Arc<LemmaType>,
24    pub body: String,
25    pub causes: Vec<Cause>,
26    pub children: Vec<ExplanationNode>,
27}
28
29impl Serialize for Explanation {
30    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
31    where
32        S: serde::Serializer,
33    {
34        ExplanationNode::Rule {
35            name: self.name.clone(),
36            result: Some(format_operation_result(
37                &self.result,
38                self.result_type.as_ref(),
39            )),
40            body: self.body.clone(),
41            causes: self.causes.clone(),
42            children: self.children.clone(),
43        }
44        .serialize(serializer)
45    }
46}
47
48pub(crate) fn format_operation_result(result: &OperationResult, result_type: &LemmaType) -> String {
49    match result {
50        OperationResult::Value(value) => value.display_value_with_type(result_type),
51        OperationResult::Veto(VetoType::UserDefined { message: None }) => String::new(),
52        OperationResult::Veto(veto) => veto.to_string(),
53    }
54}
55
56pub fn format_explanation(explanation: &Explanation) -> String {
57    let mut lines = Vec::new();
58    let result_display =
59        format_operation_result(&explanation.result, explanation.result_type.as_ref());
60    lines.push(format!("{}: {}", explanation.name.rule, result_display));
61    let mut ctx = FormatContext {
62        lines: &mut lines,
63        indent: String::new(),
64    };
65    ctx.render_rule_contents(
66        &result_display,
67        &explanation.body,
68        &explanation.causes,
69        &explanation.children,
70    );
71    lines.join("\n")
72}
73
74#[derive(Copy, Clone)]
75enum Connector {
76    Branch,
77    Last,
78}
79
80struct FormatContext<'a> {
81    lines: &'a mut Vec<String>,
82    indent: String,
83}
84
85impl<'a> FormatContext<'a> {
86    fn push_line(&mut self, connector: Connector, text: &str) {
87        self.lines.push(format!(
88            "{}{} {text}",
89            self.indent,
90            connector_str(connector)
91        ));
92    }
93
94    fn child_indent(&self, connector: Connector) -> String {
95        match connector {
96            Connector::Branch => format!("{}│  ", self.indent),
97            Connector::Last => format!("{}   ", self.indent),
98        }
99    }
100
101    fn render_rule_contents(
102        &mut self,
103        result_display: &str,
104        body: &str,
105        causes: &[Cause],
106        children: &[ExplanationNode],
107    ) {
108        let body_shown = !body.is_empty() && body != result_display;
109        let total = causes.len() + usize::from(body_shown);
110        let mut index = 0;
111
112        for cause in causes {
113            index += 1;
114            let connector = if index == total {
115                Connector::Last
116            } else {
117                Connector::Branch
118            };
119            let value = cause.value.as_str();
120            let line = if value == "true" {
121                cause.condition.clone()
122            } else {
123                format!("{} is {}", cause.condition, value)
124            };
125            self.push_line(connector, &line);
126            let child_indent = self.child_indent(connector);
127            let mut child_ctx = FormatContext {
128                lines: self.lines,
129                indent: child_indent,
130            };
131            child_ctx.render_cause_children(cause, value, &line);
132        }
133
134        if body_shown {
135            self.push_line(Connector::Last, body);
136            let child_indent = self.child_indent(Connector::Last);
137            let mut child_ctx = FormatContext {
138                lines: self.lines,
139                indent: child_indent,
140            };
141            child_ctx.render_nodes(children, Some(body));
142        } else if !children.is_empty() {
143            self.render_nodes(children, None);
144        }
145    }
146
147    /// Cause children for ASCII: omit bare literals and Data that only restates
148    /// a `name is display` cause line (JSON keeps the structured child).
149    fn render_cause_children(&mut self, cause: &Cause, value: &str, line: &str) {
150        let visible: Vec<&ExplanationNode> = cause
151            .children
152            .iter()
153            .filter(|node| !is_bare_literal_compose(node))
154            .filter(|node| !data_restates_true_cause_line(node, value, line))
155            .collect();
156        let len = visible.len();
157        for (i, node) in visible.into_iter().enumerate() {
158            let connector = if i + 1 == len {
159                Connector::Last
160            } else {
161                Connector::Branch
162            };
163            self.render_node(node, connector, None);
164        }
165    }
166
167    fn render_nodes(&mut self, nodes: &[ExplanationNode], parent_body: Option<&str>) {
168        let visible: Vec<&ExplanationNode> = nodes
169            .iter()
170            .filter(|node| !is_bare_literal_compose(node))
171            .collect();
172        let len = visible.len();
173        for (i, node) in visible.into_iter().enumerate() {
174            let connector = if i + 1 == len {
175                Connector::Last
176            } else {
177                Connector::Branch
178            };
179            self.render_node(node, connector, parent_body);
180        }
181    }
182
183    fn render_conversion_contents(
184        &mut self,
185        steps: &[SerializedConversionTraceStep],
186        operands: &[ExplanationNode],
187    ) {
188        let visible_operands: Vec<&ExplanationNode> = operands
189            .iter()
190            .filter(|node| !is_bare_literal_compose(node))
191            .collect();
192        let total = steps.len() + visible_operands.len();
193        let mut index = 0;
194        for step in steps {
195            index += 1;
196            let connector = if index == total {
197                Connector::Last
198            } else {
199                Connector::Branch
200            };
201            self.push_line(connector, &step.text);
202        }
203        for operand in visible_operands {
204            index += 1;
205            let connector = if index == total {
206                Connector::Last
207            } else {
208                Connector::Branch
209            };
210            self.render_node(operand, connector, None);
211        }
212    }
213
214    fn render_node(
215        &mut self,
216        node: &ExplanationNode,
217        connector: Connector,
218        parent_body: Option<&str>,
219    ) {
220        match node {
221            ExplanationNode::Rule {
222                name,
223                result,
224                body,
225                causes,
226                children,
227            } => {
228                let result_str = result
229                    .as_deref()
230                    .expect("BUG: ExplanationNode::Rule.result not filled by eval");
231                self.push_line(connector, &format!("{}: {result_str}", name.rule));
232                let child_indent = self.child_indent(connector);
233                let mut child_ctx = FormatContext {
234                    lines: self.lines,
235                    indent: child_indent,
236                };
237                child_ctx.render_rule_contents(result_str, body, causes, children);
238            }
239            ExplanationNode::Compose {
240                expression,
241                operands,
242            } => {
243                if parent_body.is_some_and(|body| body == expression) {
244                    self.render_nodes(operands, None);
245                } else {
246                    self.push_line(connector, expression);
247                    let child_indent = self.child_indent(connector);
248                    let mut child_ctx = FormatContext {
249                        lines: self.lines,
250                        indent: child_indent,
251                    };
252                    child_ctx.render_nodes(operands, None);
253                }
254            }
255            ExplanationNode::Data { name, display } => {
256                if name.data.is_empty() {
257                    self.push_line(connector, display);
258                } else {
259                    self.push_line(connector, &format!("{name}: {display}"));
260                }
261            }
262            ExplanationNode::DataUnused { name } => {
263                self.push_line(connector, &name.to_string());
264            }
265            ExplanationNode::Conversion {
266                expression,
267                steps,
268                operands,
269            } => {
270                let expression_is_parent_body = parent_body.is_some_and(|body| body == expression);
271                if expression_is_parent_body {
272                    let steps_without_outcome: Vec<SerializedConversionTraceStep> = steps
273                        .iter()
274                        .filter(|step| !matches!(step.role, ConversionTraceRole::Outcome))
275                        .cloned()
276                        .collect();
277                    self.render_conversion_contents(&steps_without_outcome, operands);
278                } else {
279                    self.push_line(connector, expression);
280                    let child_indent = self.child_indent(connector);
281                    let mut child_ctx = FormatContext {
282                        lines: self.lines,
283                        indent: child_indent,
284                    };
285                    child_ctx.render_conversion_contents(steps, operands);
286                }
287            }
288            ExplanationNode::Veto { message } => {
289                let text = match message.as_deref() {
290                    Some(msg) if !msg.is_empty() => format!("veto \"{msg}\""),
291                    _ => "veto".to_string(),
292                };
293                self.push_line(connector, &text);
294            }
295        }
296    }
297}
298
299fn connector_str(connector: Connector) -> &'static str {
300    match connector {
301        Connector::Branch => "├─",
302        Connector::Last => "└─",
303    }
304}
305
306/// Bare literal compose: expression text already names it; ASCII omits the node.
307fn is_bare_literal_compose(node: &ExplanationNode) -> bool {
308    matches!(node, ExplanationNode::Compose { operands, .. } if operands.is_empty())
309}
310
311/// `code is NL` already states the binding; ASCII skips child `code: NL`.
312/// Flipped / inequality cause lines do not match `{key} is {display}`.
313fn data_restates_true_cause_line(node: &ExplanationNode, value: &str, line: &str) -> bool {
314    if value != "true" {
315        return false;
316    }
317    match node {
318        ExplanationNode::Data { name, display } => {
319            line == format!("{} is {display}", name.input_key())
320        }
321        _ => false,
322    }
323}