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