1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub struct AndFact {
6 pub facts: Vec<AtomicFact>,
7 pub line_file: LineFile,
8}
9
10impl AndFact {
11 pub fn new(facts: Vec<AtomicFact>, line_file: LineFile) -> Self {
12 AndFact { facts, line_file }
13 }
14 pub fn line_file(&self) -> LineFile {
15 self.line_file.clone()
16 }
17}
18
19#[derive(Clone)]
20pub struct ChainFact {
21 pub objs: Vec<Obj>,
22 pub prop_names: Vec<AtomicName>,
23 pub line_file: LineFile,
24}
25
26impl ChainFact {
27 pub fn new(objs: Vec<Obj>, prop_names: Vec<AtomicName>, line_file: LineFile) -> Self {
28 ChainFact {
29 objs,
30 prop_names,
31 line_file,
32 }
33 }
34 pub fn line_file(&self) -> LineFile {
35 self.line_file.clone()
36 }
37
38 pub fn facts(&self) -> Result<Vec<AtomicFact>, RuntimeError> {
39 if self.objs.len() != self.prop_names.len() + 1 {
40 return Err(
41 NewAtomicFactRuntimeError(RuntimeErrorStruct::new(
42 None,
43 format!(
44 "the number of objects ({}) is not equal to the number of property names ({}) + 1",
45 self.objs.len(),
46 self.prop_names.len(),
47 ),
48 default_line_file(),
49 None,
50 vec![],
51 ))
52 .into(),
53 );
54 }
55
56 let mut facts = Vec::with_capacity(self.prop_names.len());
57 for (i, _) in self.prop_names.iter().enumerate() {
58 let prop_name = self.prop_names[i].clone();
59 let left_obj = self.objs[i].clone();
60 let right_obj = self.objs[i + 1].clone();
61 let atomic_fact = AtomicFact::to_atomic_fact(
62 prop_name,
63 true,
64 vec![left_obj, right_obj],
65 self.line_file.clone(),
66 );
67 facts.push(atomic_fact?);
68 }
69 Ok(facts)
70 }
71}
72
73#[derive(Clone)]
74pub enum ChainAtomicFact {
75 AtomicFact(AtomicFact),
76 ChainFact(ChainFact),
77}
78
79impl fmt::Display for ChainAtomicFact {
80 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
81 match self {
82 ChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
83 ChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
84 }
85 }
86}
87
88#[derive(Clone)]
89pub enum AndChainAtomicFact {
90 AtomicFact(AtomicFact),
91 AndFact(AndFact),
92 ChainFact(ChainFact),
93}
94
95impl AndChainAtomicFact {
96 pub fn line_file(&self) -> LineFile {
97 match self {
98 AndChainAtomicFact::AtomicFact(a) => a.line_file(),
99 AndChainAtomicFact::AndFact(a) => a.line_file(),
100 AndChainAtomicFact::ChainFact(c) => c.line_file(),
101 }
102 }
103
104 pub fn with_new_line_file(self, line_file: LineFile) -> Self {
105 match self {
106 AndChainAtomicFact::AtomicFact(a) => {
107 AndChainAtomicFact::AtomicFact(a.with_new_line_file(line_file))
108 }
109 AndChainAtomicFact::AndFact(af) => AndChainAtomicFact::AndFact(AndFact::new(
110 af.facts
111 .into_iter()
112 .map(|x| x.with_new_line_file(line_file.clone()))
113 .collect(),
114 line_file,
115 )),
116 AndChainAtomicFact::ChainFact(cf) => {
117 AndChainAtomicFact::ChainFact(ChainFact::new(cf.objs, cf.prop_names, line_file))
118 }
119 }
120 }
121
122 pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
123 if from == to {
124 return self;
125 }
126 match self {
127 AndChainAtomicFact::AtomicFact(a) => {
128 AndChainAtomicFact::AtomicFact(a.replace_bound_identifier(from, to))
129 }
130 AndChainAtomicFact::AndFact(af) => AndChainAtomicFact::AndFact(AndFact::new(
131 af.facts
132 .into_iter()
133 .map(|x| x.replace_bound_identifier(from, to))
134 .collect(),
135 af.line_file,
136 )),
137 AndChainAtomicFact::ChainFact(cf) => AndChainAtomicFact::ChainFact(ChainFact::new(
138 cf.objs
139 .into_iter()
140 .map(|o| Obj::replace_bound_identifier(o, from, to))
141 .collect(),
142 cf.prop_names,
143 cf.line_file,
144 )),
145 }
146 }
147}
148
149impl From<AtomicFact> for AndChainAtomicFact {
150 fn from(atomic_fact: AtomicFact) -> Self {
151 AndChainAtomicFact::AtomicFact(atomic_fact)
152 }
153}
154
155impl From<GreaterEqualFact> for AndChainAtomicFact {
156 fn from(f: GreaterEqualFact) -> Self {
157 AtomicFact::from(f).into()
158 }
159}
160
161impl fmt::Display for AndFact {
162 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
163 write!(
164 f,
165 "{}",
166 vec_to_string_with_sep(&self.facts, format!(" {} ", AND))
167 )
168 }
169}
170
171impl AndFact {
172 pub fn key(&self) -> String {
173 vec_to_string_with_sep(
174 &self.facts.iter().map(|a| a.key()).collect::<Vec<_>>(),
175 format!(" {} ", AND),
176 )
177 }
178
179 pub fn get_args_from_fact(&self) -> Vec<Obj> {
180 let mut result: Vec<Obj> = Vec::new();
181 for atomic_fact in self.facts.iter() {
182 let args_from_atomic_fact = atomic_fact.get_args_from_fact();
183 for arg in args_from_atomic_fact {
184 result.push(arg);
185 }
186 }
187 result
188 }
189}
190
191impl fmt::Display for ChainFact {
192 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
193 let mut s = self.objs[0].to_string();
194 for (i, obj) in self.objs[1..].iter().enumerate() {
195 if is_comparison_str(&self.prop_names[i].to_string()) {
196 s.push_str(&format!(" {} {}", self.prop_names[i], obj));
197 } else {
198 s.push_str(&format!(" {}{} {}", FACT_PREFIX, self.prop_names[i], obj));
199 }
200 }
201 write!(f, "{}", s)
202 }
203}
204
205impl ChainFact {
206 pub fn key(&self) -> String {
207 vec_to_string_with_sep(
208 &self
209 .prop_names
210 .iter()
211 .map(|p| p.to_string())
212 .collect::<Vec<_>>(),
213 format!(" {} ", AND),
214 )
215 }
216
217 pub fn get_args_from_fact(&self) -> Vec<Obj> {
218 let mut result: Vec<Obj> = Vec::new();
219 for obj in self.objs.iter() {
220 result.push(obj.clone());
221 }
222 result
223 }
224}
225
226impl fmt::Display for AndChainAtomicFact {
227 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
228 match self {
229 AndChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
230 AndChainAtomicFact::AndFact(a) => write!(f, "{}", a),
231 AndChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
232 }
233 }
234}
235
236impl AndChainAtomicFact {
237 pub fn key(&self) -> String {
238 match self {
239 AndChainAtomicFact::AtomicFact(a) => a.key(),
240 AndChainAtomicFact::AndFact(a) => a.key(),
241 AndChainAtomicFact::ChainFact(c) => c.key(),
242 }
243 }
244}
245
246impl From<AndChainAtomicFact> for ExistOrAndChainAtomicFact {
247 fn from(f: AndChainAtomicFact) -> Self {
248 match f {
249 AndChainAtomicFact::AtomicFact(a) => ExistOrAndChainAtomicFact::AtomicFact(a),
250 AndChainAtomicFact::AndFact(a) => ExistOrAndChainAtomicFact::AndFact(a),
251 AndChainAtomicFact::ChainFact(c) => ExistOrAndChainAtomicFact::ChainFact(c),
252 }
253 }
254}
255
256impl AndChainAtomicFact {
257 pub fn get_args_from_fact(&self) -> Vec<Obj> {
258 match self {
259 AndChainAtomicFact::AtomicFact(atomic_fact) => atomic_fact.get_args_from_fact(),
260 AndChainAtomicFact::AndFact(and_fact) => and_fact.get_args_from_fact(),
261 AndChainAtomicFact::ChainFact(chain_fact) => chain_fact.get_args_from_fact(),
262 }
263 }
264}