lemma/planning/
explanation.rs

1//! Explanation wire 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 wire 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    UnitEquivalence {
78        text: String,
79    },
80    /// Planning/eval only. Never reaches wire — lowered to causes + winner first.
81    Piecewise {
82        #[serde(serialize_with = "forbid_piecewise_serialize")]
83        arms: Vec<PiecewiseArm>,
84    },
85}
86
87#[derive(Debug, Clone, PartialEq, Eq)]
88pub struct PiecewiseArm {
89    pub condition: ExplanationNode,
90    pub result: ExplanationNode,
91    /// Plan-time truth of the condition after constant-fold / unless-force.
92    /// `None` means the condition still needs runtime evaluation.
93    pub static_condition: Option<bool>,
94    /// Cause.value when `static_condition` is `Some`. True for held arms and
95    /// narrated flipped comparison facts; false for bare / and-false static miss.
96    pub static_cause_value: Option<bool>,
97}
98
99fn forbid_piecewise_serialize<S: Serializer>(
100    _: &Vec<PiecewiseArm>,
101    _: S,
102) -> Result<S::Ok, S::Error> {
103    panic!("BUG: Piecewise must be lowered before serialize")
104}
105
106fn serialize_option_string<S>(value: &Option<String>, serializer: S) -> Result<S::Ok, S::Error>
107where
108    S: Serializer,
109{
110    match value {
111        Some(s) => serializer.serialize_str(s),
112        None => serializer.serialize_none(),
113    }
114}
115
116#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
117pub struct Cause {
118    pub condition: String,
119    #[serde(serialize_with = "serialize_option_string")]
120    pub value: Option<String>,
121    #[serde(skip_serializing_if = "Vec::is_empty")]
122    pub children: Vec<ExplanationNode>,
123}
124
125#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
126#[serde(rename_all = "snake_case")]
127pub enum ConversionTraceRole {
128    Outcome,
129    Rule,
130    Source,
131}
132
133#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
134pub struct SerializedConversionTraceStep {
135    pub(crate) role: ConversionTraceRole,
136    pub(crate) text: String,
137}
lemma/planning/explanation.rs

lemma/planning/
explanation.rs
