lemma/inversion/
derived.rs

1//! Derived expressions for inversion
2//!
3//! Expressions created during solving have no source location.
4//! They are derived from plan expressions, not parsed from user input.
5//! Strong separation: Expression (planning) has source; DerivedExpression (inversion) does not.
6
7use crate::planning::semantics::{
8    ArithmeticComputation, ComparisonComputation, FactPath, LiteralValue, MathematicalComputation,
9    NegationType, RulePath, SemanticConversionTarget, VetoExpression,
10};
11use serde::{Deserialize, Serialize};
12use std::collections::HashSet;
13use std::sync::Arc;
14
15/// Expression derived during inversion/solving. No source location.
16#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
17pub struct DerivedExpression {
18    pub kind: DerivedExpressionKind,
19}
20
21impl DerivedExpression {
22    pub fn collect_fact_paths(&self, facts: &mut HashSet<FactPath>) {
23        self.kind.collect_fact_paths(facts);
24    }
25}
26
27#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
28#[serde(rename_all = "snake_case")]
29pub enum DerivedExpressionKind {
30    /// Boxed to keep enum size small (LiteralValue is large)
31    Literal(Box<LiteralValue>),
32    FactPath(FactPath),
33    RulePath(RulePath),
34    LogicalAnd(Arc<DerivedExpression>, Arc<DerivedExpression>),
35    Arithmetic(
36        Arc<DerivedExpression>,
37        ArithmeticComputation,
38        Arc<DerivedExpression>,
39    ),
40    Comparison(
41        Arc<DerivedExpression>,
42        ComparisonComputation,
43        Arc<DerivedExpression>,
44    ),
45    UnitConversion(Arc<DerivedExpression>, SemanticConversionTarget),
46    LogicalNegation(Arc<DerivedExpression>, NegationType),
47    MathematicalComputation(MathematicalComputation, Arc<DerivedExpression>),
48    Veto(VetoExpression),
49}
50
51impl DerivedExpressionKind {
52    fn collect_fact_paths(&self, facts: &mut HashSet<FactPath>) {
53        match self {
54            DerivedExpressionKind::FactPath(fp) => {
55                facts.insert(fp.clone());
56            }
57            DerivedExpressionKind::LogicalAnd(left, right)
58            | DerivedExpressionKind::Arithmetic(left, _, right)
59            | DerivedExpressionKind::Comparison(left, _, right) => {
60                left.collect_fact_paths(facts);
61                right.collect_fact_paths(facts);
62            }
63            DerivedExpressionKind::UnitConversion(inner, _)
64            | DerivedExpressionKind::LogicalNegation(inner, _)
65            | DerivedExpressionKind::MathematicalComputation(_, inner) => {
66                inner.collect_fact_paths(facts);
67            }
68            DerivedExpressionKind::Literal(_)
69            | DerivedExpressionKind::RulePath(_)
70            | DerivedExpressionKind::Veto(_) => {}
71        }
72    }
73}
lemma/inversion/derived.rs

lemma/inversion/
derived.rs
