lemma/planning/
explanation.rs

1//! Explanation API types built during evaluation.
2//!
3//! Planning ships THE DAG (`NormalForm` nodes with optional fold `origin`).
4//! Evaluation walks that DAG — following non-piecewise origins for structure;
5//! piecewise origins supply cause records without re-entering live arm control —
6//! and fills these nodes for the response.
7//!
8//! Bound data narration is `Data` with a required `display` string.
9//! Structural mentions of paths that were never looked up are `DataUnused`
10//! (no display field) — distinct from a Missing-data veto on a live leaf walk.
11//!
12//! `Piecewise` is eval-internal only. It must be lowered to Rule causes +
13//! winner children before any API serialize.
14
15use crate::planning::semantics::{DataPath, RulePath};
16use serde::{Serialize, Serializer};
17
18pub(crate) fn serialize_rule_path_as_name<S>(
19    path: &RulePath,
20    serializer: S,
21) -> Result<S::Ok, S::Error>
22where
23    S: Serializer,
24{
25    serializer.serialize_str(&path.rule)
26}
27
28pub(crate) fn serialize_data_path_as_name<S>(
29    path: &DataPath,
30    serializer: S,
31) -> Result<S::Ok, S::Error>
32where
33    S: Serializer,
34{
35    serializer.serialize_str(&path.input_key())
36}
37
38#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
39#[serde(tag = "type", rename_all = "snake_case")]
40pub enum ExplanationNode {
41    Rule {
42        #[serde(serialize_with = "serialize_rule_path_as_name")]
43        name: RulePath,
44        #[serde(serialize_with = "serialize_option_string")]
45        result: Option<String>,
46        body: String,
47        #[serde(skip_serializing_if = "Vec::is_empty")]
48        causes: Vec<Cause>,
49        #[serde(skip_serializing_if = "Vec::is_empty")]
50        children: Vec<ExplanationNode>,
51    },
52    Compose {
53        expression: String,
54        operands: Vec<ExplanationNode>,
55    },
56    /// Evaluated / bound data narration. `display` is always the looked-up value or veto text.
57    Data {
58        #[serde(serialize_with = "serialize_data_path_as_name")]
59        name: DataPath,
60        display: String,
61    },
62    /// Structural mention of a data path that was not looked up for this cause
63    /// (short-circuit skip or static record narration without a binding).
64    DataUnused {
65        #[serde(serialize_with = "serialize_data_path_as_name")]
66        name: DataPath,
67    },
68    Conversion {
69        expression: String,
70        steps: Vec<SerializedConversionTraceStep>,
71        operands: Vec<ExplanationNode>,
72    },
73    Veto {
74        #[serde(skip_serializing_if = "Option::is_none")]
75        message: Option<String>,
76    },
77    /// Planning/eval only. Never reaches the API — lowered to causes + winner first.
78    Piecewise {
79        #[serde(serialize_with = "forbid_piecewise_serialize")]
80        arms: Vec<PiecewiseArm>,
81    },
82}
83
84#[derive(Debug, Clone, PartialEq, Eq)]
85pub struct PiecewiseArm {
86    pub condition: ExplanationNode,
87    pub result: ExplanationNode,
88    /// Plan-time truth of the condition after constant-fold / unless-force.
89    /// `None` means the condition still needs runtime evaluation.
90    pub static_condition: Option<bool>,
91    /// Cause.value when `static_condition` is `Some`. True for held arms and
92    /// narrated flipped comparison facts; false for bare / and-false static miss.
93    pub static_cause_value: Option<bool>,
94}
95
96fn forbid_piecewise_serialize<S: Serializer>(
97    _: &Vec<PiecewiseArm>,
98    _: S,
99) -> Result<S::Ok, S::Error> {
100    panic!("BUG: Piecewise must be lowered before serialize")
101}
102
103fn serialize_option_string<S>(value: &Option<String>, serializer: S) -> Result<S::Ok, S::Error>
104where
105    S: Serializer,
106{
107    match value {
108        Some(s) => serializer.serialize_str(s),
109        None => serializer.serialize_none(),
110    }
111}
112
113#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
114pub struct Cause {
115    pub condition: String,
116    pub value: String,
117    #[serde(skip_serializing_if = "Vec::is_empty")]
118    pub children: Vec<ExplanationNode>,
119}
120
121#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
122#[serde(rename_all = "snake_case")]
123pub enum ConversionTraceRole {
124    Outcome,
125    Rule,
126    Source,
127}
128
129#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
130pub struct SerializedConversionTraceStep {
131    pub(crate) role: ConversionTraceRole,
132    pub(crate) text: String,
133}
lemma/planning/explanation.rs

lemma/planning/
explanation.rs
