sdml_core/model/constraints/formal/
mod.rs

1use crate::{
2    load::ModuleLoader,
3    model::{check::Validate, modules::Module, HasBody, HasSourceSpan, References, Span},
4    store::ModuleStore,
5};
6
7#[cfg(feature = "serde")]
8use serde::{Deserialize, Serialize};
9
10// ------------------------------------------------------------------------------------------------
11// Public Types ❱ Constraints ❱ Formal
12// ------------------------------------------------------------------------------------------------
13
14#[derive(Clone, Debug)]
15#[cfg_attr(feature = "serde", derive(Deserialize, Serialize))]
16pub struct FormalConstraint {
17    #[cfg_attr(feature = "serde", serde(skip_serializing_if = "Option::is_none"))]
18    span: Option<Span>,
19    #[cfg_attr(feature = "serde", serde(skip_serializing_if = "Vec::is_empty"))]
20    environment: Vec<EnvironmentDef>,
21    body: ConstraintSentence,
22}
23
24// ------------------------------------------------------------------------------------------------
25// Implementations ❱ Constraints ❱ FormalConstraint
26// ------------------------------------------------------------------------------------------------
27
28impl HasBody for FormalConstraint {
29    type Body = ConstraintSentence;
30
31    fn body(&self) -> &Self::Body {
32        &self.body
33    }
34
35    fn body_mut(&mut self) -> &mut Self::Body {
36        &mut self.body
37    }
38
39    fn set_body(&mut self, body: Self::Body) {
40        self.body = body;
41    }
42}
43
44impl HasSourceSpan for FormalConstraint {
45    fn with_source_span(self, span: Span) -> Self {
46        let mut self_mut = self;
47        self_mut.span = Some(span);
48        self_mut
49    }
50
51    fn source_span(&self) -> Option<&Span> {
52        self.span.as_ref()
53    }
54
55    fn set_source_span(&mut self, span: Span) {
56        self.span = Some(span);
57    }
58
59    fn unset_source_span(&mut self) {
60        self.span = None;
61    }
62}
63
64impl References for FormalConstraint {}
65
66impl Validate for FormalConstraint {
67    fn validate(
68        &self,
69        _top: &Module,
70        _cache: &impl ModuleStore,
71        _loader: &impl ModuleLoader,
72        _check_constraints: bool,
73    ) {
74        todo!()
75    }
76}
77
78impl FormalConstraint {
79    // --------------------------------------------------------------------------------------------
80    // Constructors
81    // --------------------------------------------------------------------------------------------
82
83    pub fn new<V>(body: V) -> Self
84    where
85        V: Into<ConstraintSentence>,
86    {
87        Self {
88            span: Default::default(),
89            environment: Default::default(),
90            body: body.into(),
91        }
92    }
93
94    pub fn with_definition<I>(self, definition: EnvironmentDef) -> Self {
95        let mut self_mut = self;
96        self_mut.environment.push(definition);
97        self_mut
98    }
99
100    pub fn with_environment(self, environment: Vec<EnvironmentDef>) -> Self {
101        let mut self_mut = self;
102        self_mut.environment = environment;
103        self_mut
104    }
105
106    // --------------------------------------------------------------------------------------------
107    // Fields
108    // --------------------------------------------------------------------------------------------
109
110    pub fn has_definitions(&self) -> bool {
111        !self.environment.is_empty()
112    }
113
114    pub fn definitions_len(&self) -> usize {
115        self.environment.len()
116    }
117
118    pub fn definitions(&self) -> impl Iterator<Item = &EnvironmentDef> {
119        self.environment.iter()
120    }
121
122    pub fn definitions_mut(&mut self) -> impl Iterator<Item = &mut EnvironmentDef> {
123        self.environment.iter_mut()
124    }
125
126    pub fn add_to_definitions<I>(&mut self, value: I)
127    where
128        I: Into<EnvironmentDef>,
129    {
130        self.environment.push(value.into())
131    }
132
133    pub fn extend_definitions<I>(&mut self, extension: I)
134    where
135        I: IntoIterator<Item = EnvironmentDef>,
136    {
137        self.environment.extend(extension)
138    }
139}
140
141// ------------------------------------------------------------------------------------------------
142// Modules
143// ------------------------------------------------------------------------------------------------
144
145mod sequences;
146pub use sequences::{MappingVariable, NamedVariables, SequenceBuilder, Variables};
147
148mod environments;
149pub use environments::{EnvironmentDef, EnvironmentDefBody};
150
151mod functions;
152pub use functions::{
153    FunctionCardinality, FunctionDef, FunctionParameter, FunctionSignature, FunctionType,
154    FunctionTypeReference,
155};
156
157mod sentences;
158pub use sentences::{
159    AtomicSentence, BinaryBooleanSentence, BooleanSentence, ConnectiveOperator, ConstraintSentence,
160    Equation, InequalityRelation, Inequation, QuantifiedSentence, QuantifiedVariable,
161    QuantifiedVariableBinding, Quantifier, SimpleSentence, UnaryBooleanSentence,
162};
163
164mod terms;
165pub use terms::{FunctionComposition, FunctionalTerm, Subject, Term};
166
167mod values;
168pub use values::{PredicateSequenceMember, PredicateValue, SequenceOfPredicateValues};