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