lemma/evaluation/
branch_semantics.rs

1//! Single source of truth for branch and veto decision semantics.
2//!
3//! The tree evaluator consults [`condition_outcome`] for piecewise unless-arm
4//! conditions and logical operands (`and` / `or`). One rule: a vetoed condition
5//! propagates its veto; a `true` boolean is [`BranchOutcome::Taken`]; a `false`
6//! boolean is [`BranchOutcome::NotTaken`]. Connectives interpret those outcomes
7//! via their absorbing / identity literals; this module does not.
8
9use crate::computation::OperationResult;
10use crate::planning::semantics::ValueKind;
11
12/// Outcome of inspecting a branch condition or a boolean operand.
13#[derive(Debug, Clone)]
14pub enum BranchOutcome {
15    /// The boolean was `true`.
16    Taken,
17    /// The boolean was `false`.
18    NotTaken,
19    /// This result becomes the value of the enclosing computation (vetoes
20    /// that propagate).
21    Propagate(OperationResult),
22}
23
24/// Read the boolean out of a non-vetoed result. Planning guarantees boolean
25/// operands in these positions; anything else is a compiler bug and crashes.
26fn boolean_value(result: &OperationResult, context: &str) -> bool {
27    match result {
28        OperationResult::Value(literal) => match &literal.value {
29            ValueKind::Boolean(boolean) => *boolean,
30            other => panic!("BUG: {context} expected a boolean, got {other:?}"),
31        },
32        OperationResult::Veto(veto) => {
33            panic!("BUG: {context} inspected for a boolean while vetoed: {veto}")
34        }
35    }
36}
37
38/// How a piecewise unless-arm condition or a logical operand decides.
39///
40/// A vetoed condition propagates its veto as the enclosing result. A `true`
41/// boolean is [`BranchOutcome::Taken`]; a `false` boolean is
42/// [`BranchOutcome::NotTaken`].
43pub fn condition_outcome(condition: &OperationResult) -> BranchOutcome {
44    if condition.vetoed() {
45        return BranchOutcome::Propagate(condition.clone());
46    }
47    if boolean_value(condition, "branch condition") {
48        BranchOutcome::Taken
49    } else {
50        BranchOutcome::NotTaken
51    }
52}
53
54/// Where the Piecewise arm scan stopped. Arm 0 is the default; unless arms
55/// `1..arm_count` are scanned from the highest index down, like the evaluator.
56#[derive(Debug, Clone, Copy, PartialEq, Eq)]
57pub enum PiecewiseDecision {
58    /// Arm `arm` wins: every condition above it was `NotTaken`.
59    Taken { arm: usize },
60    /// Every unless condition was `NotTaken`; the default body wins.
61    Default,
62    /// The scan stopped at `arm`: its condition is not a settled boolean
63    /// (not evaluated yet, or vetoed). Conditions above it were `NotTaken`.
64    Undecided { arm: usize },
65}
66
67/// Scan unless-arm conditions high to low. `outcome(arm)` reports the
68/// condition's decision, or `None` when there is none to read.
69pub fn piecewise_decision(
70    arm_count: usize,
71    mut outcome: impl FnMut(usize) -> Option<BranchOutcome>,
72) -> PiecewiseDecision {
73    assert!(arm_count > 0, "BUG: empty piecewise");
74    for arm in (1..arm_count).rev() {
75        match outcome(arm) {
76            Some(BranchOutcome::Taken) => return PiecewiseDecision::Taken { arm },
77            Some(BranchOutcome::NotTaken) => continue,
78            Some(BranchOutcome::Propagate(_)) | None => {
79                return PiecewiseDecision::Undecided { arm };
80            }
81        }
82    }
83    PiecewiseDecision::Default
84}
85
86#[cfg(test)]
87mod tests {
88    use super::*;
89    use crate::computation::VetoType;
90
91    fn outcome_from(
92        list: &[Option<BranchOutcome>],
93    ) -> impl FnMut(usize) -> Option<BranchOutcome> + '_ {
94        move |arm| list[arm].clone()
95    }
96
97    #[test]
98    fn piecewise_decision_default_when_all_not_taken() {
99        let outcomes = [
100            None,
101            Some(BranchOutcome::NotTaken),
102            Some(BranchOutcome::NotTaken),
103        ];
104        assert_eq!(
105            piecewise_decision(3, outcome_from(&outcomes)),
106            PiecewiseDecision::Default
107        );
108    }
109
110    #[test]
111    fn piecewise_decision_highest_taken_wins() {
112        let outcomes = [None, Some(BranchOutcome::Taken), Some(BranchOutcome::Taken)];
113        assert_eq!(
114            piecewise_decision(3, outcome_from(&outcomes)),
115            PiecewiseDecision::Taken { arm: 2 }
116        );
117    }
118
119    #[test]
120    fn piecewise_decision_stops_at_unfilled_condition() {
121        let outcomes = [
122            None,
123            Some(BranchOutcome::Taken),
124            None,
125            Some(BranchOutcome::NotTaken),
126        ];
127        assert_eq!(
128            piecewise_decision(4, outcome_from(&outcomes)),
129            PiecewiseDecision::Undecided { arm: 2 }
130        );
131    }
132
133    #[test]
134    fn piecewise_decision_stops_at_vetoed_condition() {
135        let veto = OperationResult::Veto(VetoType::computation("no"));
136        let outcomes = [
137            None,
138            Some(BranchOutcome::Taken),
139            Some(BranchOutcome::Propagate(veto)),
140        ];
141        assert_eq!(
142            piecewise_decision(3, outcome_from(&outcomes)),
143            PiecewiseDecision::Undecided { arm: 2 }
144        );
145    }
146    use crate::planning::semantics::{DataPath, LiteralValue};
147
148    fn boolean(value: bool) -> OperationResult {
149        OperationResult::from_literal(LiteralValue::from_bool(value))
150    }
151
152    fn user_veto() -> OperationResult {
153        OperationResult::Veto(VetoType::UserDefined {
154            message: Some("blocked".to_string()),
155        })
156    }
157
158    fn missing_data_veto() -> OperationResult {
159        OperationResult::Veto(VetoType::missing_data(
160            DataPath::new(vec![], "x".to_string()),
161            None,
162        ))
163    }
164
165    #[test]
166    fn propagates_any_veto() {
167        assert!(matches!(
168            condition_outcome(&user_veto()),
169            BranchOutcome::Propagate(_)
170        ));
171        assert!(matches!(
172            condition_outcome(&missing_data_veto()),
173            BranchOutcome::Propagate(_)
174        ));
175    }
176
177    #[test]
178    fn boolean_decides_when_not_vetoed() {
179        assert!(matches!(
180            condition_outcome(&boolean(true)),
181            BranchOutcome::Taken
182        ));
183        assert!(matches!(
184            condition_outcome(&boolean(false)),
185            BranchOutcome::NotTaken
186        ));
187    }
188}
lemma/evaluation/branch_semantics.rs

lemma/evaluation/
branch_semantics.rs
