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