1use crate::computation::{OperationResult, VetoType};
9use crate::planning::semantics::{LemmaType, RulePath};
10use crate::planning::unit_family::FamilyUnitCatalog;
11use crate::result_value::{
12 rule_result_value_failure_message, rule_result_value_from_literal, RuleResultValue,
13 RuleResultValueFailure,
14};
15use serde::Serialize;
16use std::sync::Arc;
17
18pub use crate::planning::explanation::{
20 Cause, ConversionTraceRole, ExplanationNode, SerializedConversionTraceStep,
21};
22
23#[derive(Debug, Clone)]
24pub struct Explanation {
25 pub name: RulePath,
26 pub result: OperationResult,
27 pub result_type: Arc<LemmaType>,
29 pub(crate) family_units: Arc<FamilyUnitCatalog>,
31 pub body: String,
32 pub causes: Vec<Cause>,
33 pub children: Vec<ExplanationNode>,
34}
35
36impl Serialize for Explanation {
37 fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
38 where
39 S: serde::Serializer,
40 {
41 ExplanationNode::Rule {
42 name: self.name.clone(),
43 result: explanation_result_value(
44 &self.result,
45 self.result_type.as_ref(),
46 &self.family_units,
47 ),
48 body: self.body.clone(),
49 causes: self.causes.clone(),
50 children: self.children.clone(),
51 }
52 .serialize(serializer)
53 }
54}
55
56pub(crate) fn format_operation_result(result: &OperationResult, result_type: &LemmaType) -> String {
57 match result {
58 OperationResult::Value(bound) => bound.to_literal().display_value_with_type(result_type),
59 OperationResult::Veto(VetoType::UserDefined { message: None }) => String::new(),
60 OperationResult::Veto(veto) => veto.to_string(),
61 }
62}
63
64pub(crate) fn explanation_result_value(
66 result: &OperationResult,
67 lemma_type: &LemmaType,
68 family_units: &FamilyUnitCatalog,
69) -> RuleResultValue {
70 match result {
71 OperationResult::Value(bound) => {
72 match rule_result_value_from_literal(&bound.to_literal(), lemma_type, family_units) {
73 Ok(value) => value,
74 Err(RuleResultValueFailure::DecimalLimit) => RuleResultValue {
76 result: Some(
77 rule_result_value_failure_message(RuleResultValueFailure::DecimalLimit)
78 .to_string(),
79 ),
80 ..RuleResultValue::default()
81 },
82 Err(failure) => panic!(
83 "BUG: settled explanation value failed rule_result_value_from_literal: {}",
84 rule_result_value_failure_message(failure)
85 ),
86 }
87 }
88 OperationResult::Veto(VetoType::UserDefined { message: None }) => RuleResultValue {
89 result: Some(String::new()),
90 ..RuleResultValue::default()
91 },
92 OperationResult::Veto(veto) => RuleResultValue {
93 result: Some(veto.to_string()),
94 ..RuleResultValue::default()
95 },
96 }
97}
98
99pub fn format_explanation(explanation: &Explanation) -> String {
100 let mut lines = Vec::new();
101 let result_line = explanation_result_value(
102 &explanation.result,
103 explanation.result_type.as_ref(),
104 &explanation.family_units,
105 )
106 .result
107 .expect("BUG: root explanation must carry result");
108 lines.push(format!("{}: {}", explanation.name, result_line));
109 let mut ctx = FormatContext {
110 lines: &mut lines,
111 indent: String::new(),
112 };
113 ctx.render_rule_contents(
114 &result_line,
115 &explanation.body,
116 &explanation.causes,
117 &explanation.children,
118 );
119 lines.join("\n")
120}
121
122#[derive(Copy, Clone)]
123enum Connector {
124 Branch,
125 Last,
126}
127
128struct FormatContext<'a> {
129 lines: &'a mut Vec<String>,
130 indent: String,
131}
132
133impl FormatContext<'_> {
134 fn push_line(&mut self, connector: Connector, text: &str) {
135 self.lines.push(format!(
136 "{}{} {}",
137 self.indent,
138 connector_str(connector),
139 text
140 ));
141 }
142
143 fn child_indent(&self, connector: Connector) -> String {
144 match connector {
145 Connector::Branch => format!("{}│ ", self.indent),
146 Connector::Last => format!("{} ", self.indent),
147 }
148 }
149
150 fn render_rule_contents(
151 &mut self,
152 result_line: &str,
153 body: &str,
154 causes: &[Cause],
155 children: &[ExplanationNode],
156 ) {
157 let body_shown = !body.is_empty() && body != result_line;
158 let total = causes.len() + usize::from(body_shown);
159 let mut index = 0;
160
161 for cause in causes {
162 index += 1;
163 let connector = if index == total {
164 Connector::Last
165 } else {
166 Connector::Branch
167 };
168 let value = cause.value.as_str();
169 let line = if value == "true" {
170 cause.condition.clone()
171 } else {
172 format!("{} is {}", cause.condition, value)
173 };
174 self.push_line(connector, &line);
175 let child_indent = self.child_indent(connector);
176 let mut child_ctx = FormatContext {
177 lines: self.lines,
178 indent: child_indent,
179 };
180 child_ctx.render_cause_children(cause, value, &line);
181 }
182
183 if body_shown {
184 self.push_line(Connector::Last, body);
185 let child_indent = self.child_indent(Connector::Last);
186 let mut child_ctx = FormatContext {
187 lines: self.lines,
188 indent: child_indent,
189 };
190 child_ctx.render_nodes(children, Some(body));
191 } else if !children.is_empty() {
192 self.render_nodes(children, None);
193 }
194 }
195
196 fn render_cause_children(&mut self, cause: &Cause, value: &str, line: &str) {
199 let visible: Vec<&ExplanationNode> = cause
200 .children
201 .iter()
202 .filter(|node| !is_bare_literal_compose(node))
203 .filter(|node| !data_restates_true_cause_line(node, value, line))
204 .collect();
205 let len = visible.len();
206 for (i, node) in visible.into_iter().enumerate() {
207 let connector = if i + 1 == len {
208 Connector::Last
209 } else {
210 Connector::Branch
211 };
212 self.render_node(node, connector, None);
213 }
214 }
215
216 fn render_nodes(&mut self, nodes: &[ExplanationNode], parent_body: Option<&str>) {
217 let visible: Vec<&ExplanationNode> = nodes
218 .iter()
219 .filter(|node| !is_bare_literal_compose(node))
220 .collect();
221 let len = visible.len();
222 for (i, node) in visible.into_iter().enumerate() {
223 let connector = if i + 1 == len {
224 Connector::Last
225 } else {
226 Connector::Branch
227 };
228 self.render_node(node, connector, parent_body);
229 }
230 }
231
232 fn render_conversion_contents(
233 &mut self,
234 steps: &[SerializedConversionTraceStep],
235 operands: &[ExplanationNode],
236 ) {
237 let visible_operands: Vec<&ExplanationNode> = operands
238 .iter()
239 .filter(|node| !is_bare_literal_compose(node))
240 .collect();
241 let total = steps.len() + visible_operands.len();
242 let mut index = 0;
243 for step in steps {
244 index += 1;
245 let connector = if index == total {
246 Connector::Last
247 } else {
248 Connector::Branch
249 };
250 self.push_line(connector, &step.text);
251 }
252 for operand in visible_operands {
253 index += 1;
254 let connector = if index == total {
255 Connector::Last
256 } else {
257 Connector::Branch
258 };
259 self.render_node(operand, connector, None);
260 }
261 }
262
263 fn render_node(
264 &mut self,
265 node: &ExplanationNode,
266 connector: Connector,
267 parent_body: Option<&str>,
268 ) {
269 match node {
270 ExplanationNode::Rule {
271 name,
272 result,
273 body,
274 causes,
275 children,
276 } => {
277 let result_str = result
278 .result
279 .as_deref()
280 .expect("BUG: ExplanationNode::Rule.result.result not filled by eval");
281 self.push_line(connector, &format!("{name}: {result_str}"));
282 let child_indent = self.child_indent(connector);
283 let mut child_ctx = FormatContext {
284 lines: self.lines,
285 indent: child_indent,
286 };
287 child_ctx.render_rule_contents(result_str, body, causes, children);
288 }
289 ExplanationNode::Compose {
290 expression,
291 operands,
292 ..
293 } => {
294 if parent_body.is_some_and(|body| body == expression) {
295 self.render_nodes(operands, None);
296 } else {
297 self.push_line(connector, expression);
298 let child_indent = self.child_indent(connector);
299 let mut child_ctx = FormatContext {
300 lines: self.lines,
301 indent: child_indent,
302 };
303 child_ctx.render_nodes(operands, None);
304 }
305 }
306 ExplanationNode::Data { name, result } => {
307 let result_str = result
308 .result
309 .as_deref()
310 .expect("BUG: ExplanationNode::Data.result.result not filled by eval");
311 if name.data.is_empty() {
312 self.push_line(connector, result_str);
313 } else {
314 self.push_line(connector, &format!("{name}: {result_str}"));
315 }
316 }
317 ExplanationNode::DataUnused { name } => {
318 self.push_line(connector, &name.to_string());
319 }
320 ExplanationNode::Conversion {
321 expression,
322 steps,
323 operands,
324 } => {
325 let expression_is_parent_body = parent_body.is_some_and(|body| body == expression);
326 if expression_is_parent_body {
327 let steps_without_outcome: Vec<SerializedConversionTraceStep> = steps
328 .iter()
329 .filter(|step| !matches!(step.role, ConversionTraceRole::Outcome))
330 .cloned()
331 .collect();
332 self.render_conversion_contents(&steps_without_outcome, operands);
333 } else {
334 self.push_line(connector, expression);
335 let child_indent = self.child_indent(connector);
336 let mut child_ctx = FormatContext {
337 lines: self.lines,
338 indent: child_indent,
339 };
340 child_ctx.render_conversion_contents(steps, operands);
341 }
342 }
343 ExplanationNode::Veto { message } => {
344 let text = match message.as_deref() {
345 Some(msg) if !msg.is_empty() => format!("veto \"{msg}\""),
346 _ => "veto".to_string(),
347 };
348 self.push_line(connector, &text);
349 }
350 }
351 }
352}
353
354fn connector_str(connector: Connector) -> &'static str {
355 match connector {
356 Connector::Branch => "├─",
357 Connector::Last => "└─",
358 }
359}
360
361fn is_bare_literal_compose(node: &ExplanationNode) -> bool {
363 matches!(node, ExplanationNode::Compose { operands, .. } if operands.is_empty())
364}
365
366fn data_restates_true_cause_line(node: &ExplanationNode, value: &str, line: &str) -> bool {
369 if value != "true" {
370 return false;
371 }
372 match node {
373 ExplanationNode::Data {
374 name,
375 result: node_result,
376 } => {
377 let result_str = node_result
378 .result
379 .as_deref()
380 .expect("BUG: Data node must carry result");
381 line == format!("{} is {result_str}", name.input_key())
382 }
383 _ => false,
384 }
385}