1use crate::computation::{OperationResult, VetoType};
10use crate::planning::explanation::{ExplainedRule, ExplainedRuleId};
11use crate::planning::semantics::{LemmaType, RulePath};
12use crate::planning::unit_family::FamilyUnitCatalog;
13use crate::result_value::{
14 rule_result_value_failure_message, rule_result_value_from_literal, RuleResultValue,
15 RuleResultValueFailure,
16};
17use serde::Serialize;
18use std::collections::HashSet;
19use std::sync::Arc;
20
21pub use crate::planning::explanation::{
23 Cause, ConversionTraceRole, ExplanationNode, SerializedConversionTraceStep,
24};
25
26#[derive(Debug, Clone)]
27pub struct Explanation {
28 pub name: RulePath,
29 pub result: OperationResult,
30 pub result_type: Arc<LemmaType>,
32 pub(crate) family_units: Arc<FamilyUnitCatalog>,
34 pub body: String,
35 pub causes: Vec<Cause>,
36 pub children: Vec<ExplanationNode>,
37 pub rules: Vec<ExplainedRule>,
39}
40
41#[derive(Serialize)]
42struct ExplanationSer<'a> {
43 #[serde(rename = "type")]
44 kind: &'static str,
45 #[serde(serialize_with = "crate::planning::explanation::serialize_rule_path_as_name")]
46 name: &'a RulePath,
47 #[serde(flatten)]
48 result: RuleResultValue,
49 body: &'a str,
50 #[serde(skip_serializing_if = "<[_]>::is_empty")]
51 causes: &'a [Cause],
52 #[serde(skip_serializing_if = "<[_]>::is_empty")]
53 children: &'a [ExplanationNode],
54 #[serde(skip_serializing_if = "<[_]>::is_empty")]
55 rules: &'a [ExplainedRule],
56}
57
58impl Serialize for Explanation {
59 fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
60 where
61 S: serde::Serializer,
62 {
63 ExplanationSer {
64 kind: "rule",
65 name: &self.name,
66 result: explanation_result_value(
67 &self.result,
68 self.result_type.as_ref(),
69 &self.family_units,
70 ),
71 body: &self.body,
72 causes: self.causes.as_slice(),
73 children: self.children.as_slice(),
74 rules: self.rules.as_slice(),
75 }
76 .serialize(serializer)
77 }
78}
79
80pub(crate) fn format_operation_result(result: &OperationResult, result_type: &LemmaType) -> String {
81 match result {
82 OperationResult::Value(bound) => bound.to_literal().display_value_with_type(result_type),
83 OperationResult::Veto(VetoType::UserDefined { message: None }) => String::new(),
84 OperationResult::Veto(veto) => veto.to_string(),
85 }
86}
87
88pub(crate) fn explanation_result_value(
90 result: &OperationResult,
91 lemma_type: &LemmaType,
92 family_units: &FamilyUnitCatalog,
93) -> RuleResultValue {
94 match result {
95 OperationResult::Value(bound) => {
96 match rule_result_value_from_literal(&bound.to_literal(), lemma_type, family_units) {
97 Ok(value) => value,
98 Err(RuleResultValueFailure::DecimalLimit) => RuleResultValue {
100 result: Some(
101 rule_result_value_failure_message(RuleResultValueFailure::DecimalLimit)
102 .to_string(),
103 ),
104 ..RuleResultValue::default()
105 },
106 Err(failure) => panic!(
107 "BUG: settled explanation value failed rule_result_value_from_literal: {}",
108 rule_result_value_failure_message(failure)
109 ),
110 }
111 }
112 OperationResult::Veto(VetoType::UserDefined { message: None }) => RuleResultValue {
113 result: Some(String::new()),
114 ..RuleResultValue::default()
115 },
116 OperationResult::Veto(veto) => RuleResultValue {
117 result: Some(veto.to_string()),
118 ..RuleResultValue::default()
119 },
120 }
121}
122
123pub fn format_explanation(explanation: &Explanation) -> String {
124 let mut lines = Vec::new();
125 let result_line = explanation_result_value(
126 &explanation.result,
127 explanation.result_type.as_ref(),
128 &explanation.family_units,
129 )
130 .result
131 .expect("BUG: root explanation must carry result");
132 lines.push(format!("{}: {}", explanation.name, result_line));
133 let mut state = FormatState {
134 lines: &mut lines,
135 rules: &explanation.rules,
136 expanded: HashSet::new(),
137 stack: Vec::new(),
138 };
139 state.push_rule_contents(
140 &result_line,
141 &explanation.body,
142 &explanation.causes,
143 &explanation.children,
144 String::new(),
145 );
146 state.run();
147 lines.join("\n")
148}
149
150#[derive(Copy, Clone)]
151enum Connector {
152 Branch,
153 Last,
154 None,
156}
157
158enum ConversionSteps<'a> {
159 Borrowed(&'a [SerializedConversionTraceStep]),
160 Owned(Vec<SerializedConversionTraceStep>),
161}
162
163impl ConversionSteps<'_> {
164 fn as_slice(&self) -> &[SerializedConversionTraceStep] {
165 match self {
166 ConversionSteps::Borrowed(steps) => steps,
167 ConversionSteps::Owned(steps) => steps.as_slice(),
168 }
169 }
170}
171
172struct Siblings<'a> {
175 connected: Vec<&'a ExplanationNode>,
176 rows: Vec<&'a ExplanationNode>,
177}
178
179impl<'a> Siblings<'a> {
180 fn new(nodes: impl Iterator<Item = &'a ExplanationNode>) -> Self {
181 let mut connected = Vec::new();
182 let mut rows = Vec::new();
183 for node in nodes {
184 if is_bare_literal_compose(node) {
185 continue;
186 }
187 if matches!(node, ExplanationNode::Row { .. }) {
188 rows.push(node);
189 } else if !rows.is_empty() {
190 panic!("BUG: non-row explanation node follows a Row sibling");
191 } else {
192 connected.push(node);
193 }
194 }
195 Self { connected, rows }
196 }
197
198 fn len(&self) -> usize {
199 self.connected.len() + self.rows.len()
200 }
201}
202
203enum Work<'a> {
204 Line {
205 indent: String,
206 connector: Connector,
207 text: String,
208 },
209 RuleBody {
210 id: ExplainedRuleId,
211 result_line: String,
212 indent: String,
213 },
214 Nodes {
215 siblings: Siblings<'a>,
216 parent_body: Option<&'a str>,
217 indent: String,
218 next: usize,
219 },
220 CauseChildren {
221 children: Vec<&'a ExplanationNode>,
222 indent: String,
223 next: usize,
224 },
225 Conversion {
226 steps: ConversionSteps<'a>,
227 siblings: Siblings<'a>,
228 indent: String,
229 next: usize,
230 },
231}
232
233struct FormatState<'a> {
234 lines: &'a mut Vec<String>,
235 rules: &'a [ExplainedRule],
236 expanded: HashSet<ExplainedRuleId>,
237 stack: Vec<Work<'a>>,
238}
239
240impl<'a> FormatState<'a> {
241 fn push_line(&mut self, indent: &str, connector: Connector, text: &str) {
242 match connector {
243 Connector::None => self.lines.push(format!("{indent}{text}")),
244 Connector::Branch | Connector::Last => self
245 .lines
246 .push(format!("{indent}{} {text}", connector_str(connector))),
247 }
248 }
249
250 fn child_indent(indent: &str, connector: Connector) -> String {
251 match connector {
252 Connector::Branch => format!("{indent}│ "),
253 Connector::Last => format!("{indent} "),
254 Connector::None => format!("{indent} "),
255 }
256 }
257
258 fn rule_by_id(&self, id: ExplainedRuleId) -> &'a ExplainedRule {
259 self.rules
260 .iter()
261 .find(|rule| rule.id == id)
262 .unwrap_or_else(|| panic!("BUG: explanation missing rules entry for id {}", id.0))
263 }
264
265 fn push_rule_contents(
266 &mut self,
267 result_line: &str,
268 body: &'a str,
269 causes: &'a [Cause],
270 children: &'a [ExplanationNode],
271 indent: String,
272 ) {
273 let body_shown = !body.is_empty() && body != result_line;
274 let total = causes.len() + usize::from(body_shown);
275 if body_shown {
277 let child_indent = Self::child_indent(&indent, Connector::Last);
278 self.stack.push(Work::Nodes {
279 siblings: Siblings::new(children.iter()),
280 parent_body: Some(body),
281 indent: child_indent,
282 next: 0,
283 });
284 self.stack.push(Work::Line {
285 indent: indent.clone(),
286 connector: Connector::Last,
287 text: body.to_string(),
288 });
289 } else if !children.is_empty() {
290 self.stack.push(Work::Nodes {
291 siblings: Siblings::new(children.iter()),
292 parent_body: None,
293 indent: indent.clone(),
294 next: 0,
295 });
296 }
297 for (i, cause) in causes.iter().enumerate().rev() {
298 let connector = if i + 1 == total {
299 Connector::Last
300 } else {
301 Connector::Branch
302 };
303 let value = cause.value.as_str();
304 let line = if value == "true" {
305 cause.condition.clone()
306 } else {
307 format!("{} is {}", cause.condition, value)
308 };
309 let visible: Vec<&'a ExplanationNode> = cause
310 .children
311 .iter()
312 .filter(|node| !is_bare_literal_compose(node))
313 .filter(|node| !data_restates_true_cause_line(node, value, &line))
314 .collect();
315 let child_indent = Self::child_indent(&indent, connector);
316 self.stack.push(Work::CauseChildren {
317 children: visible,
318 indent: child_indent,
319 next: 0,
320 });
321 self.stack.push(Work::Line {
322 indent: indent.clone(),
323 connector,
324 text: line,
325 });
326 }
327 }
328
329 fn run(&mut self) {
330 while let Some(work) = self.stack.pop() {
331 match work {
332 Work::Line {
333 indent,
334 connector,
335 text,
336 } => self.push_line(&indent, connector, &text),
337 Work::RuleBody {
338 id,
339 result_line,
340 indent,
341 } => {
342 let rule = self.rule_by_id(id);
343 self.push_rule_contents(
344 &result_line,
345 rule.body.as_str(),
346 rule.causes.as_slice(),
347 rule.children.as_slice(),
348 indent,
349 );
350 }
351 Work::Nodes {
352 siblings,
353 parent_body,
354 indent,
355 next,
356 } => self.step_nodes(siblings, parent_body, indent, next),
357 Work::CauseChildren {
358 children,
359 indent,
360 next,
361 } => self.step_cause_children(children, indent, next),
362 Work::Conversion {
363 steps,
364 siblings,
365 indent,
366 next,
367 } => self.step_conversion(steps, siblings, indent, next),
368 }
369 }
370 }
371
372 fn step_nodes(
373 &mut self,
374 siblings: Siblings<'a>,
375 parent_body: Option<&'a str>,
376 indent: String,
377 next: usize,
378 ) {
379 if next >= siblings.len() {
380 return;
381 }
382 let connected_len = siblings.connected.len();
383 let (node, connector) = if next < connected_len {
384 let connector = if next + 1 == connected_len {
385 Connector::Last
386 } else {
387 Connector::Branch
388 };
389 (siblings.connected[next], connector)
390 } else {
391 (siblings.rows[next - connected_len], Connector::None)
392 };
393 self.stack.push(Work::Nodes {
394 siblings,
395 parent_body,
396 indent: indent.clone(),
397 next: next + 1,
398 });
399 self.emit_node(node, connector, parent_body, indent);
400 }
401
402 fn step_cause_children(
403 &mut self,
404 children: Vec<&'a ExplanationNode>,
405 indent: String,
406 next: usize,
407 ) {
408 if next >= children.len() {
409 return;
410 }
411 let connector = if next + 1 == children.len() {
412 Connector::Last
413 } else {
414 Connector::Branch
415 };
416 let node = children[next];
417 self.stack.push(Work::CauseChildren {
418 children,
419 indent: indent.clone(),
420 next: next + 1,
421 });
422 self.emit_node(node, connector, None, indent);
423 }
424
425 fn step_conversion(
426 &mut self,
427 steps: ConversionSteps<'a>,
428 siblings: Siblings<'a>,
429 indent: String,
430 next: usize,
431 ) {
432 let step_len = steps.as_slice().len();
433 let total = step_len + siblings.len();
434 if next >= total {
435 return;
436 }
437 let connector = if next + 1 == total {
438 Connector::Last
439 } else {
440 Connector::Branch
441 };
442 if next < step_len {
443 let text = steps.as_slice()[next].text.clone();
444 self.stack.push(Work::Conversion {
445 steps,
446 siblings,
447 indent: indent.clone(),
448 next: next + 1,
449 });
450 self.push_line(&indent, connector, &text);
451 return;
452 }
453 let op_index = next - step_len;
454 let connected_len = siblings.connected.len();
455 let (node, connector) = if op_index < connected_len {
456 (siblings.connected[op_index], connector)
457 } else {
458 (siblings.rows[op_index - connected_len], Connector::None)
459 };
460 self.stack.push(Work::Conversion {
461 steps,
462 siblings,
463 indent: indent.clone(),
464 next: next + 1,
465 });
466 self.emit_node(node, connector, None, indent);
467 }
468
469 fn emit_node(
470 &mut self,
471 node: &'a ExplanationNode,
472 connector: Connector,
473 parent_body: Option<&'a str>,
474 indent: String,
475 ) {
476 match node {
477 ExplanationNode::RuleRef { id, name, result } => {
478 let result_str = result
479 .result
480 .as_deref()
481 .expect("BUG: ExplanationNode::RuleRef.result.result not filled by eval");
482 if self.expanded.insert(*id) {
483 self.push_line(&indent, connector, &format!("{name}: {result_str}"));
484 self.stack.push(Work::RuleBody {
485 id: *id,
486 result_line: result_str.to_string(),
487 indent: Self::child_indent(&indent, connector),
488 });
489 } else {
490 self.push_line(
491 &indent,
492 connector,
493 &format!("{name}: {result_str} (see above)"),
494 );
495 }
496 }
497 ExplanationNode::Compose {
498 expression,
499 operands,
500 ..
501 } => {
502 if parent_body.is_some_and(|body| body == expression.as_str()) {
503 self.stack.push(Work::Nodes {
504 siblings: Siblings::new(operands.iter()),
505 parent_body: None,
506 indent,
507 next: 0,
508 });
509 } else {
510 self.push_line(&indent, connector, expression);
511 let child_indent = Self::child_indent(&indent, connector);
512 self.stack.push(Work::Nodes {
513 siblings: Siblings::new(operands.iter()),
514 parent_body: None,
515 indent: child_indent,
516 next: 0,
517 });
518 }
519 }
520 ExplanationNode::Data { name, result } => {
521 let result_str = result
522 .result
523 .as_deref()
524 .expect("BUG: ExplanationNode::Data.result.result not filled by eval");
525 if name.data.is_empty() {
526 self.push_line(&indent, connector, result_str);
527 } else {
528 self.push_line(&indent, connector, &format!("{name}: {result_str}"));
529 }
530 }
531 ExplanationNode::DataUnused { name } => {
532 self.push_line(&indent, connector, &name.to_string());
533 }
534 ExplanationNode::Conversion {
535 expression,
536 steps,
537 operands,
538 } => {
539 let expression_is_parent_body =
540 parent_body.is_some_and(|body| body == expression.as_str());
541 if expression_is_parent_body {
542 let owned: Vec<SerializedConversionTraceStep> = steps
543 .iter()
544 .filter(|step| !matches!(step.role, ConversionTraceRole::Outcome))
545 .cloned()
546 .collect();
547 self.stack.push(Work::Conversion {
548 steps: ConversionSteps::Owned(owned),
549 siblings: Siblings::new(operands.iter()),
550 indent,
551 next: 0,
552 });
553 } else {
554 self.push_line(&indent, connector, expression);
555 let child_indent = Self::child_indent(&indent, connector);
556 self.stack.push(Work::Conversion {
557 steps: ConversionSteps::Borrowed(steps),
558 siblings: Siblings::new(operands.iter()),
559 indent: child_indent,
560 next: 0,
561 });
562 }
563 }
564 ExplanationNode::Veto { message } => {
565 let text = match message.as_deref() {
566 Some(msg) if !msg.is_empty() => format!("veto \"{msg}\""),
567 _ => "veto".to_string(),
568 };
569 self.push_line(&indent, connector, &text);
570 }
571 ExplanationNode::Row {
572 number,
573 appended,
574 key,
575 fields,
576 } => {
577 let label = row_label(*number, *appended, key);
578 let child_indent = Self::child_indent(&indent, Connector::None);
579 if fields.len() == 1 {
580 match &fields[0] {
581 ExplanationNode::RuleRef { id, name, result } => {
582 let result_str = result
583 .result
584 .as_deref()
585 .expect("BUG: RuleRef.result.result not filled by eval");
586 if self.expanded.insert(*id) {
587 self.push_line(
588 &indent,
589 Connector::None,
590 &format!("{label} {name}: {result_str}"),
591 );
592 self.stack.push(Work::RuleBody {
593 id: *id,
594 result_line: result_str.to_string(),
595 indent: child_indent,
596 });
597 } else {
598 self.push_line(
599 &indent,
600 Connector::None,
601 &format!("{label} {name}: {result_str} (see above)"),
602 );
603 }
604 }
605 other => {
606 let field_line = field_headline(other);
607 self.push_line(
608 &indent,
609 Connector::None,
610 &format!("{label} {field_line}"),
611 );
612 }
613 }
614 } else {
615 self.push_line(&indent, Connector::None, &label);
616 self.stack.push(Work::Nodes {
617 siblings: Siblings::new(fields.iter()),
618 parent_body: None,
619 indent: child_indent,
620 next: 0,
621 });
622 }
623 }
624 ExplanationNode::Filter {
625 condition,
626 matched,
627 total,
628 children,
629 } => {
630 self.push_line(
631 &indent,
632 connector,
633 &format!("{matched} of {total} are {condition}"),
634 );
635 let child_indent = Self::child_indent(&indent, connector);
636 self.stack.push(Work::Nodes {
637 siblings: Siblings::new(children.iter()),
638 parent_body: None,
639 indent: child_indent,
640 next: 0,
641 });
642 }
643 }
644 }
645}
646
647fn row_label(number: usize, appended: bool, key: &[ExplanationNode]) -> String {
648 if key.is_empty() {
649 if appended {
650 format!("appended {number}.")
651 } else {
652 format!("{number}.")
653 }
654 } else {
655 let values: Vec<String> = key.iter().map(key_value_display).collect();
656 format!("[{}]", values.join(", "))
657 }
658}
659
660fn key_value_display(node: &ExplanationNode) -> String {
662 match node {
663 ExplanationNode::Data { result, .. } => {
664 if let Some(text) = &result.text {
665 format!("\"{text}\"")
666 } else {
667 result
668 .result
669 .as_deref()
670 .expect("BUG: row key Data must carry result")
671 .to_string()
672 }
673 }
674 other => panic!("BUG: row key node is {other:?}, not Data"),
675 }
676}
677
678fn field_headline(field: &ExplanationNode) -> String {
679 match field {
680 ExplanationNode::RuleRef { name, result, .. } => {
681 let result_str = result
682 .result
683 .as_deref()
684 .expect("BUG: RuleRef.result.result not filled by eval");
685 format!("{name}: {result_str}")
686 }
687 ExplanationNode::Data { name, result } => {
688 let result_str = result
689 .result
690 .as_deref()
691 .expect("BUG: Data.result.result not filled by eval");
692 if name.data.is_empty() {
693 result_str.to_string()
694 } else {
695 format!("{name}: {result_str}")
696 }
697 }
698 ExplanationNode::DataUnused { name } => name.to_string(),
699 ExplanationNode::Veto { message } => match message.as_deref() {
700 Some(msg) if !msg.is_empty() => format!("veto \"{msg}\""),
701 _ => "veto".to_string(),
702 },
703 other => panic!("BUG: row field headline for unexpected node {other:?}"),
704 }
705}
706
707fn connector_str(connector: Connector) -> &'static str {
708 match connector {
709 Connector::Branch => "├─",
710 Connector::Last => "└─",
711 Connector::None => "",
712 }
713}
714
715fn is_bare_literal_compose(node: &ExplanationNode) -> bool {
717 matches!(node, ExplanationNode::Compose { operands, .. } if operands.is_empty())
718}
719
720fn data_restates_true_cause_line(node: &ExplanationNode, value: &str, line: &str) -> bool {
723 if value != "true" {
724 return false;
725 }
726 match node {
727 ExplanationNode::Data {
728 name,
729 result: node_result,
730 } => {
731 let result_str = node_result
732 .result
733 .as_deref()
734 .expect("BUG: Data node must carry result");
735 line == format!("{} is {result_str}", name.input_key())
736 }
737 _ => false,
738 }
739}