1use crate::computation::{OperationResult, VetoType};
9use crate::planning::semantics::{LemmaType, RulePath};
10use serde::Serialize;
11use std::sync::Arc;
12
13pub 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 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 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
306fn is_bare_literal_compose(node: &ExplanationNode) -> bool {
308 matches!(node, ExplanationNode::Compose { operands, .. } if operands.is_empty())
309}
310
311fn 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}