litex/execute/
exec_have_fn_equal_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_have_fn_equal_stmt(
5        &mut self,
6        have_fn_equal_stmt: &HaveFnEqualStmt,
7    ) -> Result<StmtResult, RuntimeError> {
8        let fn_set_stored = FnSet::from_body(have_fn_equal_stmt.equal_to_anonymous_fn.body.clone())
9            .map_err(|e| {
10                short_exec_error(
11                    have_fn_equal_stmt.clone().into(),
12                    "have_fn_equal_stmt: build fn set for storage failed".to_string(),
13                    Some(e),
14                    vec![],
15                )
16            })?;
17
18        self.have_fn_equal_stmt_verify_well_defined(have_fn_equal_stmt, &fn_set_stored)
19            .map_err(|e| {
20                short_exec_error(
21                    have_fn_equal_stmt.clone().into(),
22                    "have_fn_equal_stmt: verify well-defined failed".to_string(),
23                    Some(e),
24                    vec![],
25                )
26            })?;
27
28        let infer_result =
29            self.store_have_fn_equal_stmt_facts(have_fn_equal_stmt, &fn_set_stored)?;
30
31        Ok(
32            (NonFactualStmtSuccess::new(have_fn_equal_stmt.clone().into(), infer_result, vec![]))
33                .into(),
34        )
35    }
36
37    fn store_have_fn_equal_stmt_facts(
38        &mut self,
39        have_fn_equal_stmt: &HaveFnEqualStmt,
40        fn_set_stored: &FnSet,
41    ) -> Result<InferResult, RuntimeError> {
42        self.store_free_param_or_identifier_name(
43            &have_fn_equal_stmt.name,
44            ParamObjType::Identifier,
45        )?;
46
47        let function_identifier_obj: Obj = Identifier::new(have_fn_equal_stmt.name.clone()).into();
48        let function_set_obj = fn_set_stored.clone().into();
49        let function_in_function_set_fact = InFact::new(
50            function_identifier_obj.clone(),
51            function_set_obj,
52            have_fn_equal_stmt.line_file.clone(),
53        )
54        .into();
55
56        let infer_result = self
57            .verify_well_defined_and_store_and_infer_with_default_verify_state(
58                function_in_function_set_fact,
59            )
60            .map_err(|store_fact_error| {
61                short_exec_error(
62                    have_fn_equal_stmt.clone().into(),
63                    "",
64                    Some(store_fact_error),
65                    vec![],
66                )
67            })?;
68
69        let stmt_lf = have_fn_equal_stmt.line_file.clone();
70        self.register_known_objs_in_fn_sets_for_element_body(
71            &function_identifier_obj,
72            fn_set_stored.body.clone(),
73            Some((*have_fn_equal_stmt.equal_to_anonymous_fn.equal_to).clone()),
74            stmt_lf.clone(),
75            stmt_lf,
76        );
77
78        let function_equals_anonymous_fn_fact: AtomicFact = EqualFact::new(
79            function_identifier_obj,
80            have_fn_equal_stmt.equal_to_anonymous_fn.clone().into(),
81            have_fn_equal_stmt.line_file.clone(),
82        )
83        .into();
84        let _ = self
85            .store_atomic_fact_without_well_defined_verified_and_infer(
86                function_equals_anonymous_fn_fact,
87            )
88            .map_err(|store_fact_error| {
89                short_exec_error(
90                    have_fn_equal_stmt.clone().into(),
91                    "",
92                    Some(store_fact_error),
93                    vec![],
94                )
95            })?;
96
97        Ok(infer_result)
98    }
99
100    fn have_fn_equal_stmt_verify_well_defined(
101        &mut self,
102        have_fn_equal_stmt: &HaveFnEqualStmt,
103        fn_set_stored: &FnSet,
104    ) -> Result<(), RuntimeError> {
105        self.run_in_local_env(|rt| {
106            rt.have_fn_equal_stmt_verify_well_defined_body(have_fn_equal_stmt, fn_set_stored)
107        })
108    }
109
110    fn have_fn_equal_stmt_verify_well_defined_body(
111        &mut self,
112        have_fn_equal_stmt: &HaveFnEqualStmt,
113        fn_set_stored: &FnSet,
114    ) -> Result<(), RuntimeError> {
115        let verify_state = VerifyState::new(0, false);
116
117        self.verify_obj_well_defined_and_store_cache(
118            &have_fn_equal_stmt.equal_to_anonymous_fn.clone().into(),
119            &verify_state,
120        )
121        .map_err(|well_defined_error| {
122            short_exec_error(
123                have_fn_equal_stmt.clone().into(),
124                "",
125                Some(well_defined_error),
126                vec![],
127            )
128        })?;
129
130        let function_set_obj = fn_set_stored.clone().into();
131        self.verify_obj_well_defined_and_store_cache(&function_set_obj, &verify_state)
132            .map_err(|well_defined_error| {
133                short_exec_error(
134                    have_fn_equal_stmt.clone().into(),
135                    "",
136                    Some(well_defined_error),
137                    vec![],
138                )
139            })?;
140
141        let verify_result = self
142            .run_in_local_env(|rt| {
143                for param_def_with_set in have_fn_equal_stmt
144                    .equal_to_anonymous_fn
145                    .body
146                    .params_def_with_set
147                    .iter()
148                {
149                    rt.define_params_with_set(param_def_with_set)?;
150                }
151                for dom_fact in have_fn_equal_stmt
152                    .equal_to_anonymous_fn
153                    .body
154                    .dom_facts
155                    .iter()
156                {
157                    let _ = rt
158                        .store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
159                            dom_fact.clone(),
160                        )?;
161                }
162                let equal_to_in_ret_set_atomic_fact = InFact::new(
163                    (*have_fn_equal_stmt.equal_to_anonymous_fn.equal_to).clone(),
164                    (*have_fn_equal_stmt.equal_to_anonymous_fn.body.ret_set).clone(),
165                    have_fn_equal_stmt.line_file.clone(),
166                )
167                .into();
168                rt.verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
169            })
170            .map_err(|verify_error| {
171                short_exec_error(
172                    have_fn_equal_stmt.clone().into(),
173                    "",
174                    Some(verify_error),
175                    vec![],
176                )
177            })?;
178        if verify_result.is_unknown() {
179            let msg = format!(
180                "have_fn_equal_stmt: {} is not in return set {}",
181                have_fn_equal_stmt.equal_to_anonymous_fn.equal_to,
182                have_fn_equal_stmt.equal_to_anonymous_fn.body.ret_set
183            );
184            return Err(short_exec_error(
185                have_fn_equal_stmt.clone().into(),
186                msg,
187                None,
188                vec![],
189            ));
190        }
191
192        Ok(())
193    }
194}
litex/execute/exec_have_fn_equal_stmt.rs

litex/execute/
exec_have_fn_equal_stmt.rs
