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