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