sdml_core/model/constraints/formal/
mod.rs1use 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#[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
24impl 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 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 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
141mod 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};