1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub enum Stmt {
6 Fact(Fact),
7 DefLetStmt(DefLetStmt),
8 DefPropStmt(DefPropStmt),
9 DefAbstractPropStmt(DefAbstractPropStmt),
10 HaveObjInNonemptySetStmt(HaveObjInNonemptySetOrParamTypeStmt),
11 HaveObjEqualStmt(HaveObjEqualStmt),
12 HaveByExistStmt(HaveByExistStmt),
13 HaveFnEqualStmt(HaveFnEqualStmt),
14 HaveFnEqualCaseByCaseStmt(HaveFnEqualCaseByCaseStmt),
15 HaveFnByInducStmt(HaveFnByInducStmt),
16 DefStructStmt(DefStructStmt),
17 DefFamilyStmt(DefFamilyStmt),
18 DefAlgoStmt(DefAlgoStmt),
19 ClaimStmt(ClaimStmt),
20 KnowStmt(KnowStmt),
21 ProveStmt(ProveStmt),
22 ImportStmt(ImportStmt),
23 DoNothingStmt(DoNothingStmt),
24 RunFileStmt(RunFileStmt),
25 EvalStmt(EvalStmt),
26 WitnessExistFact(WitnessExistFact),
27 WitnessNonemptySet(WitnessNonemptySet),
28 ByCasesStmt(ByCasesStmt),
29 ByContraStmt(ByContraStmt),
30 ByEnumerateFiniteSetStmt(ByEnumerateFiniteSetStmt),
31 ByInducStmt(ByInducStmt),
32 ByForStmt(ByForStmt),
33 ByExtensionStmt(ByExtensionStmt),
34 ByFnStmt(ByFnStmt),
35 ByFamilyStmt(ByFamilyStmt),
36 ByStructStmt(ByStructStmt),
37 ByTuple(ByTupleStmt),
38 ByFnSetStmt(ByFnSetStmt),
39 ByFiniteSeqSetStmt(ByFiniteSeqSetStmt),
40 BySeqSetStmt(BySeqSetStmt),
41 ByMatrixSetStmt(ByMatrixSetStmt),
42 ByEnumerateClosedRangeStmt(ByEnumerateClosedRangeStmt),
43}
44
45#[derive(Clone)]
46pub struct ByEnumerateClosedRangeStmt {
47 pub element: Obj,
48 pub closed_range: ClosedRange,
49 pub line_file: LineFile,
50}
51
52impl fmt::Display for ByEnumerateClosedRangeStmt {
53 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
54 write!(
55 f,
56 "{} {} {}{}{}{}, {}{}{}: {}",
57 BY,
58 ENUMERATE,
59 CLOSED_RANGE,
60 LEFT_BRACE,
61 self.closed_range.start,
62 COMMA,
63 self.closed_range.end,
64 RIGHT_BRACE,
65 COLON,
66 self.element
67 )
68 }
69}
70
71impl ByEnumerateClosedRangeStmt {
72 pub fn new(element: Obj, closed_range: ClosedRange, line_file: LineFile) -> Self {
73 ByEnumerateClosedRangeStmt {
74 element,
75 closed_range,
76 line_file,
77 }
78 }
79}
80
81#[derive(Clone)]
82pub struct ByFiniteSeqSetStmt {
83 pub finite_seq_set: FiniteSeqSet,
84 pub line_file: LineFile,
85}
86
87impl fmt::Display for ByFiniteSeqSetStmt {
88 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
89 let o: Obj = self.finite_seq_set.clone().into();
90 write!(f, "{} {}{} {}", BY, FINITE_SEQ, COLON, o)
91 }
92}
93
94impl ByFiniteSeqSetStmt {
95 pub fn new(finite_seq_set: FiniteSeqSet, line_file: LineFile) -> Self {
96 ByFiniteSeqSetStmt {
97 finite_seq_set,
98 line_file,
99 }
100 }
101}
102
103#[derive(Clone)]
104pub struct BySeqSetStmt {
105 pub seq_set: SeqSet,
106 pub line_file: LineFile,
107}
108
109impl fmt::Display for BySeqSetStmt {
110 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
111 let o: Obj = self.seq_set.clone().into();
112 write!(f, "{} {}{} {}", BY, SEQ, COLON, o)
113 }
114}
115
116impl BySeqSetStmt {
117 pub fn new(seq_set: SeqSet, line_file: LineFile) -> Self {
118 BySeqSetStmt { seq_set, line_file }
119 }
120}
121
122#[derive(Clone)]
123pub struct ByMatrixSetStmt {
124 pub matrix_set: MatrixSet,
125 pub line_file: LineFile,
126}
127
128impl fmt::Display for ByMatrixSetStmt {
129 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
130 let o: Obj = self.matrix_set.clone().into();
131 write!(f, "{} {}{} {}", BY, MATRIX, COLON, o)
132 }
133}
134
135impl ByMatrixSetStmt {
136 pub fn new(matrix_set: MatrixSet, line_file: LineFile) -> Self {
137 ByMatrixSetStmt {
138 matrix_set,
139 line_file,
140 }
141 }
142}
143
144impl fmt::Debug for Stmt {
145 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
146 write!(f, "{}", self)
147 }
148}
149
150impl fmt::Display for Stmt {
151 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
152 match self {
153 Stmt::Fact(x) => write!(f, "{}", x),
154 Stmt::DefLetStmt(x) => write!(f, "{}", x),
155 Stmt::DefPropStmt(x) => write!(f, "{}", x),
156 Stmt::DefAbstractPropStmt(x) => write!(f, "{}", x),
157 Stmt::HaveObjInNonemptySetStmt(x) => write!(f, "{}", x),
158 Stmt::HaveObjEqualStmt(x) => write!(f, "{}", x),
159 Stmt::HaveByExistStmt(x) => write!(f, "{}", x),
160 Stmt::HaveFnEqualStmt(x) => write!(f, "{}", x),
161 Stmt::HaveFnEqualCaseByCaseStmt(x) => write!(f, "{}", x),
162 Stmt::HaveFnByInducStmt(x) => write!(f, "{}", x),
163 Stmt::DefStructStmt(x) => write!(f, "{}", x),
164 Stmt::DefFamilyStmt(x) => write!(f, "{}", x),
165 Stmt::DefAlgoStmt(x) => write!(f, "{}", x),
166 Stmt::ClaimStmt(x) => write!(f, "{}", x),
167 Stmt::KnowStmt(x) => write!(f, "{}", x),
168 Stmt::ProveStmt(x) => write!(f, "{}", x),
169 Stmt::ImportStmt(x) => write!(f, "{}", x),
170 Stmt::DoNothingStmt(x) => write!(f, "{}", x),
171 Stmt::RunFileStmt(x) => write!(f, "{}", x),
172 Stmt::EvalStmt(x) => write!(f, "{}", x),
173 Stmt::WitnessExistFact(x) => write!(f, "{}", x),
174 Stmt::WitnessNonemptySet(x) => write!(f, "{}", x),
175 Stmt::ByCasesStmt(x) => write!(f, "{}", x),
176 Stmt::ByContraStmt(x) => write!(f, "{}", x),
177 Stmt::ByEnumerateFiniteSetStmt(x) => write!(f, "{}", x),
178 Stmt::ByInducStmt(x) => write!(f, "{}", x),
179 Stmt::ByForStmt(x) => write!(f, "{}", x),
180 Stmt::ByExtensionStmt(x) => write!(f, "{}", x),
181 Stmt::ByFnStmt(x) => write!(f, "{}", x),
182 Stmt::ByFamilyStmt(x) => write!(f, "{}", x),
183 Stmt::ByStructStmt(x) => write!(f, "{}", x),
184 Stmt::ByTuple(x) => write!(f, "{}", x),
185 Stmt::ByFnSetStmt(x) => write!(f, "{}", x),
186 Stmt::ByFiniteSeqSetStmt(x) => write!(f, "{}", x),
187 Stmt::BySeqSetStmt(x) => write!(f, "{}", x),
188 Stmt::ByMatrixSetStmt(x) => write!(f, "{}", x),
189 Stmt::ByEnumerateClosedRangeStmt(x) => write!(f, "{}", x),
190 }
191 }
192}
193
194impl Stmt {
195 pub fn line_file(&self) -> LineFile {
196 match self {
197 Stmt::Fact(fact) => fact.line_file(),
198 Stmt::DefLetStmt(stmt) => stmt.line_file.clone(),
199 Stmt::DefPropStmt(stmt) => stmt.line_file.clone(),
200 Stmt::DefAbstractPropStmt(stmt) => stmt.line_file.clone(),
201 Stmt::HaveObjInNonemptySetStmt(stmt) => stmt.line_file.clone(),
202 Stmt::HaveObjEqualStmt(stmt) => stmt.line_file.clone(),
203 Stmt::HaveByExistStmt(stmt) => stmt.line_file.clone(),
204 Stmt::HaveFnEqualStmt(stmt) => stmt.line_file.clone(),
205 Stmt::HaveFnEqualCaseByCaseStmt(stmt) => stmt.line_file.clone(),
206 Stmt::HaveFnByInducStmt(stmt) => stmt.line_file.clone(),
207 Stmt::DefStructStmt(stmt) => stmt.line_file.clone(),
208 Stmt::DefFamilyStmt(stmt) => stmt.line_file.clone(),
209 Stmt::DefAlgoStmt(stmt) => stmt.line_file.clone(),
210 Stmt::ClaimStmt(stmt) => stmt.line_file.clone(),
211 Stmt::KnowStmt(stmt) => stmt.line_file.clone(),
212 Stmt::ProveStmt(stmt) => stmt.line_file.clone(),
213 Stmt::ImportStmt(stmt) => stmt.line_file(),
214 Stmt::DoNothingStmt(stmt) => stmt.line_file.clone(),
215 Stmt::RunFileStmt(stmt) => stmt.line_file.clone(),
216 Stmt::EvalStmt(stmt) => stmt.line_file.clone(),
217 Stmt::WitnessExistFact(stmt) => stmt.line_file.clone(),
218 Stmt::WitnessNonemptySet(stmt) => stmt.line_file.clone(),
219 Stmt::ByCasesStmt(stmt) => stmt.line_file.clone(),
220 Stmt::ByContraStmt(stmt) => stmt.line_file.clone(),
221 Stmt::ByEnumerateFiniteSetStmt(stmt) => stmt.line_file.clone(),
222 Stmt::ByInducStmt(stmt) => stmt.line_file.clone(),
223 Stmt::ByForStmt(stmt) => stmt.line_file.clone(),
224 Stmt::ByExtensionStmt(stmt) => stmt.line_file.clone(),
225 Stmt::ByFnStmt(stmt) => stmt.line_file.clone(),
226 Stmt::ByFamilyStmt(stmt) => stmt.line_file.clone(),
227 Stmt::ByStructStmt(stmt) => stmt.line_file.clone(),
228 Stmt::ByTuple(stmt) => stmt.line_file.clone(),
229 Stmt::ByFnSetStmt(stmt) => stmt.line_file.clone(),
230 Stmt::ByFiniteSeqSetStmt(stmt) => stmt.line_file.clone(),
231 Stmt::BySeqSetStmt(stmt) => stmt.line_file.clone(),
232 Stmt::ByMatrixSetStmt(stmt) => stmt.line_file.clone(),
233 Stmt::ByEnumerateClosedRangeStmt(stmt) => stmt.line_file.clone(),
234 }
235 }
236
237 pub fn stmt_type_name(&self) -> String {
238 match self {
239 Stmt::Fact(_) => "Fact".to_string(),
240 Stmt::DefLetStmt(stmt) => stmt.stmt_type_name(),
241 Stmt::DefPropStmt(stmt) => stmt.stmt_type_name(),
242 Stmt::DefAbstractPropStmt(stmt) => stmt.stmt_type_name(),
243 Stmt::HaveObjInNonemptySetStmt(stmt) => stmt.stmt_type_name(),
244 Stmt::HaveObjEqualStmt(stmt) => stmt.stmt_type_name(),
245 Stmt::HaveByExistStmt(stmt) => stmt.stmt_type_name(),
246 Stmt::HaveFnEqualStmt(stmt) => stmt.stmt_type_name(),
247 Stmt::HaveFnEqualCaseByCaseStmt(stmt) => stmt.stmt_type_name(),
248 Stmt::HaveFnByInducStmt(stmt) => stmt.stmt_type_name(),
249 Stmt::DefStructStmt(stmt) => stmt.stmt_type_name(),
250 Stmt::DefFamilyStmt(stmt) => stmt.stmt_type_name(),
251 Stmt::DefAlgoStmt(stmt) => stmt.stmt_type_name(),
252 Stmt::ClaimStmt(stmt) => stmt.stmt_type_name(),
253 Stmt::KnowStmt(stmt) => stmt.stmt_type_name(),
254 Stmt::ProveStmt(stmt) => stmt.stmt_type_name(),
255 Stmt::ImportStmt(stmt) => stmt.stmt_type_name(),
256 Stmt::DoNothingStmt(stmt) => stmt.stmt_type_name(),
257 Stmt::RunFileStmt(stmt) => stmt.stmt_type_name(),
258 Stmt::EvalStmt(stmt) => stmt.stmt_type_name(),
259 Stmt::WitnessExistFact(stmt) => stmt.stmt_type_name(),
260 Stmt::WitnessNonemptySet(stmt) => stmt.stmt_type_name(),
261 Stmt::ByCasesStmt(stmt) => stmt.stmt_type_name(),
262 Stmt::ByContraStmt(stmt) => stmt.stmt_type_name(),
263 Stmt::ByEnumerateFiniteSetStmt(stmt) => stmt.stmt_type_name(),
264 Stmt::ByInducStmt(stmt) => stmt.stmt_type_name(),
265 Stmt::ByForStmt(stmt) => stmt.stmt_type_name(),
266 Stmt::ByExtensionStmt(stmt) => stmt.stmt_type_name(),
267 Stmt::ByFnStmt(stmt) => stmt.stmt_type_name(),
268 Stmt::ByFamilyStmt(stmt) => stmt.stmt_type_name(),
269 Stmt::ByStructStmt(stmt) => stmt.stmt_type_name(),
270 Stmt::ByTuple(stmt) => stmt.stmt_type_name(),
271 Stmt::ByFnSetStmt(stmt) => stmt.stmt_type_name(),
272 Stmt::ByFiniteSeqSetStmt(stmt) => stmt.stmt_type_name(),
273 Stmt::BySeqSetStmt(stmt) => stmt.stmt_type_name(),
274 Stmt::ByMatrixSetStmt(stmt) => stmt.stmt_type_name(),
275 Stmt::ByEnumerateClosedRangeStmt(stmt) => stmt.stmt_type_name(),
276 }
277 }
278}
279
280impl From<Fact> for Stmt {
281 fn from(v: Fact) -> Self {
282 Stmt::Fact(v)
283 }
284}
285
286impl From<DefLetStmt> for Stmt {
287 fn from(v: DefLetStmt) -> Self {
288 Stmt::DefLetStmt(v)
289 }
290}
291
292impl From<DefPropStmt> for Stmt {
293 fn from(v: DefPropStmt) -> Self {
294 Stmt::DefPropStmt(v)
295 }
296}
297
298impl From<DefAbstractPropStmt> for Stmt {
299 fn from(v: DefAbstractPropStmt) -> Self {
300 Stmt::DefAbstractPropStmt(v)
301 }
302}
303
304impl From<HaveObjInNonemptySetOrParamTypeStmt> for Stmt {
305 fn from(v: HaveObjInNonemptySetOrParamTypeStmt) -> Self {
306 Stmt::HaveObjInNonemptySetStmt(v)
307 }
308}
309
310impl From<HaveObjEqualStmt> for Stmt {
311 fn from(v: HaveObjEqualStmt) -> Self {
312 Stmt::HaveObjEqualStmt(v)
313 }
314}
315
316impl From<HaveByExistStmt> for Stmt {
317 fn from(v: HaveByExistStmt) -> Self {
318 Stmt::HaveByExistStmt(v)
319 }
320}
321
322impl From<HaveFnEqualStmt> for Stmt {
323 fn from(v: HaveFnEqualStmt) -> Self {
324 Stmt::HaveFnEqualStmt(v)
325 }
326}
327
328impl From<HaveFnEqualCaseByCaseStmt> for Stmt {
329 fn from(v: HaveFnEqualCaseByCaseStmt) -> Self {
330 Stmt::HaveFnEqualCaseByCaseStmt(v)
331 }
332}
333
334impl From<HaveFnByInducStmt> for Stmt {
335 fn from(v: HaveFnByInducStmt) -> Self {
336 Stmt::HaveFnByInducStmt(v)
337 }
338}
339
340impl From<DefStructStmt> for Stmt {
341 fn from(v: DefStructStmt) -> Self {
342 Stmt::DefStructStmt(v)
343 }
344}
345
346impl From<DefFamilyStmt> for Stmt {
347 fn from(v: DefFamilyStmt) -> Self {
348 Stmt::DefFamilyStmt(v)
349 }
350}
351
352impl From<DefAlgoStmt> for Stmt {
353 fn from(v: DefAlgoStmt) -> Self {
354 Stmt::DefAlgoStmt(v)
355 }
356}
357
358impl From<ClaimStmt> for Stmt {
359 fn from(v: ClaimStmt) -> Self {
360 Stmt::ClaimStmt(v)
361 }
362}
363
364impl From<KnowStmt> for Stmt {
365 fn from(v: KnowStmt) -> Self {
366 Stmt::KnowStmt(v)
367 }
368}
369
370impl From<ProveStmt> for Stmt {
371 fn from(v: ProveStmt) -> Self {
372 Stmt::ProveStmt(v)
373 }
374}
375
376impl From<ImportStmt> for Stmt {
377 fn from(v: ImportStmt) -> Self {
378 Stmt::ImportStmt(v)
379 }
380}
381
382impl From<DoNothingStmt> for Stmt {
383 fn from(v: DoNothingStmt) -> Self {
384 Stmt::DoNothingStmt(v)
385 }
386}
387
388impl From<RunFileStmt> for Stmt {
389 fn from(v: RunFileStmt) -> Self {
390 Stmt::RunFileStmt(v)
391 }
392}
393
394impl From<EvalStmt> for Stmt {
395 fn from(v: EvalStmt) -> Self {
396 Stmt::EvalStmt(v)
397 }
398}
399
400impl From<WitnessExistFact> for Stmt {
401 fn from(v: WitnessExistFact) -> Self {
402 Stmt::WitnessExistFact(v)
403 }
404}
405
406impl From<WitnessNonemptySet> for Stmt {
407 fn from(v: WitnessNonemptySet) -> Self {
408 Stmt::WitnessNonemptySet(v)
409 }
410}
411
412impl From<ByCasesStmt> for Stmt {
413 fn from(v: ByCasesStmt) -> Self {
414 Stmt::ByCasesStmt(v)
415 }
416}
417
418impl From<ByContraStmt> for Stmt {
419 fn from(v: ByContraStmt) -> Self {
420 Stmt::ByContraStmt(v)
421 }
422}
423
424impl From<ByEnumerateFiniteSetStmt> for Stmt {
425 fn from(v: ByEnumerateFiniteSetStmt) -> Self {
426 Stmt::ByEnumerateFiniteSetStmt(v)
427 }
428}
429
430impl From<ByInducStmt> for Stmt {
431 fn from(v: ByInducStmt) -> Self {
432 Stmt::ByInducStmt(v)
433 }
434}
435
436impl From<ByForStmt> for Stmt {
437 fn from(v: ByForStmt) -> Self {
438 Stmt::ByForStmt(v)
439 }
440}
441
442impl From<ByExtensionStmt> for Stmt {
443 fn from(v: ByExtensionStmt) -> Self {
444 Stmt::ByExtensionStmt(v)
445 }
446}
447
448impl From<ByFnStmt> for Stmt {
449 fn from(v: ByFnStmt) -> Self {
450 Stmt::ByFnStmt(v)
451 }
452}
453
454impl From<ByFamilyStmt> for Stmt {
455 fn from(v: ByFamilyStmt) -> Self {
456 Stmt::ByFamilyStmt(v)
457 }
458}
459
460impl From<ByStructStmt> for Stmt {
461 fn from(v: ByStructStmt) -> Self {
462 Stmt::ByStructStmt(v)
463 }
464}
465
466impl From<ByTupleStmt> for Stmt {
467 fn from(v: ByTupleStmt) -> Self {
468 Stmt::ByTuple(v)
469 }
470}
471
472impl From<ByFnSetStmt> for Stmt {
473 fn from(v: ByFnSetStmt) -> Self {
474 Stmt::ByFnSetStmt(v)
475 }
476}
477
478impl From<ByFiniteSeqSetStmt> for Stmt {
479 fn from(v: ByFiniteSeqSetStmt) -> Self {
480 Stmt::ByFiniteSeqSetStmt(v)
481 }
482}
483
484impl From<BySeqSetStmt> for Stmt {
485 fn from(v: BySeqSetStmt) -> Self {
486 Stmt::BySeqSetStmt(v)
487 }
488}
489
490impl From<ByMatrixSetStmt> for Stmt {
491 fn from(v: ByMatrixSetStmt) -> Self {
492 Stmt::ByMatrixSetStmt(v)
493 }
494}
495
496impl From<ByEnumerateClosedRangeStmt> for Stmt {
497 fn from(v: ByEnumerateClosedRangeStmt) -> Self {
498 Stmt::ByEnumerateClosedRangeStmt(v)
499 }
500}