litex/execute/
exec_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_stmt(&mut self, stmt: &Stmt) -> Result<StmtResult, RuntimeError> {
5        match stmt {
6            Stmt::DefLetStmt(d) => self.exec_let_stmt(d),
7            Stmt::DefPropStmt(d) => self.exec_def_prop_stmt(d),
8            Stmt::DefAbstractPropStmt(d) => self.exec_def_abstract_prop_stmt(d),
9            Stmt::HaveObjInNonemptySetStmt(d) => {
10                self.exec_have_obj_in_nonempty_set_or_param_type_stmt(d)
11            }
12            Stmt::HaveObjEqualStmt(d) => self.exec_have_obj_equal_stmt(d),
13            Stmt::HaveByExistStmt(d) => self.exec_have_exist_obj_stmt(d),
14            Stmt::HaveFnEqualStmt(d) => self.exec_have_fn_equal_stmt(d),
15            Stmt::HaveFnEqualCaseByCaseStmt(d) => self.exec_have_fn_equal_case_by_case_stmt(d),
16            Stmt::HaveFnByInducStmt(d) => self.exec_have_fn_by_induc_stmt(d),
17            Stmt::HaveFnByForallExistUniqueStmt(d) => {
18                self.exec_have_fn_by_forall_exist_unique_stmt(d)
19            }
20            Stmt::DefTemplateStmt(d) => self.exec_def_template_stmt(d),
21            Stmt::DefAlgoStmt(d) => self.exec_def_algo_stmt(d),
22            Stmt::KnowStmt(know_stmt) => self.exec_know_stmt(know_stmt),
23            Stmt::Fact(fact) => self.exec_fact(fact),
24            Stmt::ClaimStmt(s) => self.exec_claim_stmt(s),
25            Stmt::ProveStmt(s) => self.exec_prove_stmt(s),
26            Stmt::ImportStmt(s) => self.exec_import_stmt(s),
27            Stmt::DoNothingStmt(s) => self.exec_do_nothing_stmt(s),
28            Stmt::ClearStmt(s) => self.exec_clear_stmt(s),
29            Stmt::RunFileStmt(s) => self.exec_run_file_stmt(s),
30            Stmt::RunFileInStd(s) => self.exec_run_file_in_std(s),
31            Stmt::EvalStmt(s) => self.exec_eval_stmt(s),
32            Stmt::EvalByStmt(s) => self.exec_eval_by_stmt(s),
33            Stmt::WitnessExistFact(s) => self.exec_witness_exist_fact(s),
34            Stmt::WitnessNonemptySet(s) => self.exec_witness_nonempty_set(s),
35            Stmt::ByCasesStmt(s) => self.exec_by_cases_stmt(s),
36            Stmt::ByContraStmt(s) => self.exec_by_contra_stmt(s),
37            Stmt::ByEnumerateFiniteSetStmt(s) => self.exec_by_enumerate_finite_set_stmt(s),
38            Stmt::ByInducStmt(s) => self.exec_by_induc_stmt(s),
39            Stmt::ByForStmt(s) => self.exec_by_for_stmt(s),
40            Stmt::ByExtensionStmt(s) => self.exec_by_extension_stmt(s),
41            Stmt::ByFnAsSetStmt(s) => self.exec_by_fn_stmt(s),
42            Stmt::ByTupleAsSetStmt(s) => self.exec_by_tuple_stmt(s),
43            Stmt::ByFnSetAsSetStmt(s) => self.exec_by_fn_set_stmt(s),
44            Stmt::ByClosedRangeAsCasesStmt(s) => self.exec_by_closed_range_as_cases_stmt(s),
45            Stmt::ByTransitivePropStmt(s) => self.exec_by_transitive_prop_stmt(s),
46            Stmt::BySymmetricPropStmt(s) => self.exec_by_symmetric_prop_stmt(s),
47            Stmt::ByReflexivePropStmt(s) => self.exec_by_reflexive_prop_stmt(s),
48            Stmt::ByAntisymmetricPropStmt(s) => self.exec_by_antisymmetric_prop_stmt(s),
49            Stmt::DefStructStmt(s) => self.exec_def_struct_stmt(s),
50        }
51    }
52
53    pub fn stmt_unsupported(stmt: Stmt) -> Result<StmtResult, RuntimeError> {
54        Err(short_exec_error(
55            stmt,
56            "unimplemented".to_string(),
57            None,
58            vec![],
59        ))
60    }
61}
litex/execute/exec_stmt.rs

litex/execute/
exec_stmt.rs
