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