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