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