1use crate::prelude::*;
2
3use super::exec_have_fn_equal_shared::{
4 build_function_obj_with_param_names, param_defs_with_type_from_have_fn_clause,
5};
6
7impl Runtime {
8 pub fn exec_have_fn_equal_case_by_case_stmt(
9 &mut self,
10 have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
11 ) -> Result<StmtResult, RuntimeError> {
12 let fn_set_stored = self
13 .fn_set_from_fn_set_clause(&have_fn_equal_case_by_case_stmt.fn_set_clause)
14 .map_err(|e| {
15 short_exec_error(
16 have_fn_equal_case_by_case_stmt.clone().into(),
17 "have_fn_equal_case_by_case_stmt: build fn set for storage failed".to_string(),
18 Some(e),
19 vec![],
20 )
21 })?;
22
23 self.have_fn_equal_case_by_case_stmt_verify_well_defined(
24 have_fn_equal_case_by_case_stmt,
25 &fn_set_stored,
26 )
27 .map_err(|e| {
28 short_exec_error(
29 have_fn_equal_case_by_case_stmt.clone().into(),
30 "have_fn_equal_case_by_case_stmt: verify well-defined failed".to_string(),
31 Some(e),
32 vec![],
33 )
34 })?;
35
36 let infer_result = self.store_have_fn_equal_case_by_case_stmt_facts(
37 have_fn_equal_case_by_case_stmt,
38 &fn_set_stored,
39 )?;
40 Ok((NonFactualStmtSuccess::new(
41 have_fn_equal_case_by_case_stmt.clone().into(),
42 infer_result,
43 vec![],
44 ))
45 .into())
46 }
47
48 fn store_have_fn_equal_case_by_case_stmt_facts(
49 &mut self,
50 have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
51 fn_set_stored: &FnSet,
52 ) -> Result<InferResult, RuntimeError> {
53 self.store_free_param_or_identifier_name(
54 &have_fn_equal_case_by_case_stmt.name,
55 ParamObjType::Identifier,
56 )?;
57
58 let function_identifier_obj =
59 Identifier::new(have_fn_equal_case_by_case_stmt.name.clone()).into();
60 let function_set_obj = fn_set_stored.clone().into();
61 let function_in_function_set_fact = InFact::new(
62 function_identifier_obj,
63 function_set_obj,
64 have_fn_equal_case_by_case_stmt.line_file.clone(),
65 )
66 .into();
67
68 let mut infer_result = self
69 .verify_well_defined_and_store_and_infer_with_default_verify_state(
70 function_in_function_set_fact,
71 )
72 .map_err(|store_fact_error| {
73 short_exec_error(
74 have_fn_equal_case_by_case_stmt.clone().into(),
75 "",
76 Some(store_fact_error),
77 vec![],
78 )
79 })?;
80
81 let param_defs_with_type = param_defs_with_type_from_have_fn_clause(
82 &have_fn_equal_case_by_case_stmt.fn_set_clause,
83 );
84 let param_names = ParamGroupWithSet::collect_param_names(
85 &have_fn_equal_case_by_case_stmt
86 .fn_set_clause
87 .params_def_with_set,
88 );
89 let function_obj = build_function_obj_with_param_names(
90 &have_fn_equal_case_by_case_stmt.name,
91 ¶m_names,
92 );
93
94 for case_index in 0..have_fn_equal_case_by_case_stmt.cases.len() {
95 let case_fact = &have_fn_equal_case_by_case_stmt.cases[case_index];
96 let equal_to = &have_fn_equal_case_by_case_stmt.equal_tos[case_index];
97
98 let mut forall_dom_facts: Vec<Fact> = Vec::with_capacity(
99 have_fn_equal_case_by_case_stmt
100 .fn_set_clause
101 .dom_facts
102 .len()
103 + 1,
104 );
105 for dom_fact in have_fn_equal_case_by_case_stmt
106 .fn_set_clause
107 .dom_facts
108 .iter()
109 {
110 forall_dom_facts.push(dom_fact.clone().into());
111 }
112 forall_dom_facts.push(case_fact.clone().into());
113
114 let function_equals_equal_to_fact: AtomicFact = EqualFact::new(
115 function_obj.clone(),
116 equal_to.clone(),
117 have_fn_equal_case_by_case_stmt.line_file.clone(),
118 )
119 .into();
120 let forall_fact = ForallFact::new(
121 param_defs_with_type.clone(),
122 forall_dom_facts,
123 vec![function_equals_equal_to_fact.into()],
124 have_fn_equal_case_by_case_stmt.line_file.clone(),
125 )?;
126 let forall_as_fact = self
127 .inst_have_fn_forall_fact_for_store(forall_fact)
128 .map_err(|store_inst_error| {
129 short_exec_error(
130 have_fn_equal_case_by_case_stmt.clone().into(),
131 "have_fn_equal_case_by_case_stmt: inst forall for store failed".to_string(),
132 Some(store_inst_error),
133 vec![],
134 )
135 })?;
136
137 let forall_infer_result = self
138 .verify_well_defined_and_store_and_infer_with_default_verify_state(forall_as_fact)
139 .map_err(|store_fact_error| {
140 short_exec_error(
141 have_fn_equal_case_by_case_stmt.clone().into(),
142 "",
143 Some(store_fact_error),
144 vec![],
145 )
146 })?;
147 infer_result.new_infer_result_inside(forall_infer_result);
148 }
149
150 Ok(infer_result)
151 }
152
153 fn have_fn_equal_case_by_case_stmt_verify_well_defined(
154 &mut self,
155 have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
156 fn_set_stored: &FnSet,
157 ) -> Result<(), RuntimeError> {
158 if have_fn_equal_case_by_case_stmt.cases.len()
159 != have_fn_equal_case_by_case_stmt.equal_tos.len()
160 {
161 return Err(short_exec_error(
162 have_fn_equal_case_by_case_stmt.clone().into(),
163 "have_fn_equal_case_by_case_stmt: number of cases does not match number of equal_tos"
164 .to_string(),
165 None,
166 vec![],
167 ));
168 }
169
170 let function_set_obj = fn_set_stored.clone().into();
171 self.verify_obj_well_defined_and_store_cache(
172 &function_set_obj,
173 &VerifyState::new(0, false),
174 )
175 .map_err(|well_defined_error| {
176 short_exec_error(
177 have_fn_equal_case_by_case_stmt.clone().into(),
178 "",
179 Some(well_defined_error),
180 vec![],
181 )
182 })?;
183
184 for case_index in 0..have_fn_equal_case_by_case_stmt.cases.len() {
185 let case_fact = &have_fn_equal_case_by_case_stmt.cases[case_index];
186 let equal_to = &have_fn_equal_case_by_case_stmt.equal_tos[case_index];
187
188 self.run_in_local_env(|rt| {
189 rt.have_fn_equal_case_by_case_stmt_verify_well_defined_body(
190 have_fn_equal_case_by_case_stmt,
191 case_fact,
192 equal_to,
193 )
194 })?;
195 }
196
197 Ok(())
198 }
199
200 fn have_fn_equal_case_by_case_stmt_verify_well_defined_body(
201 &mut self,
202 have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt,
203 case_fact: &AndChainAtomicFact,
204 equal_to: &Obj,
205 ) -> Result<(), RuntimeError> {
206 let verify_state = VerifyState::new(0, false);
207 let case_fact_as_fact: Fact = case_fact.clone().into();
208
209 for param_def_with_set in have_fn_equal_case_by_case_stmt
210 .fn_set_clause
211 .params_def_with_set
212 .iter()
213 {
214 self.define_params_with_set(param_def_with_set)
215 .map_err(|define_params_error| {
216 short_exec_error(
217 have_fn_equal_case_by_case_stmt.clone().into(),
218 "",
219 Some(define_params_error),
220 vec![],
221 )
222 })?;
223 }
224
225 for dom_fact in have_fn_equal_case_by_case_stmt
226 .fn_set_clause
227 .dom_facts
228 .iter()
229 {
230 let _ = self
231 .store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
232 dom_fact.clone(),
233 )
234 .map_err(|store_fact_error| {
235 short_exec_error(
236 have_fn_equal_case_by_case_stmt.clone().into(),
237 "",
238 Some(store_fact_error),
239 vec![],
240 )
241 })?;
242 }
243
244 let _ = self
245 .verify_well_defined_and_store_and_infer_with_default_verify_state(case_fact_as_fact)
246 .map_err(|store_fact_error| {
247 short_exec_error(
248 have_fn_equal_case_by_case_stmt.clone().into(),
249 "",
250 Some(store_fact_error),
251 vec![],
252 )
253 })?;
254 self.verify_obj_well_defined_and_store_cache(equal_to, &verify_state)
255 .map_err(|well_defined_error| {
256 short_exec_error(
257 have_fn_equal_case_by_case_stmt.clone().into(),
258 "",
259 Some(well_defined_error),
260 vec![],
261 )
262 })?;
263
264 let equal_to_in_ret_set_atomic_fact = InFact::new(
265 equal_to.clone(),
266 have_fn_equal_case_by_case_stmt
267 .fn_set_clause
268 .ret_set
269 .clone(),
270 have_fn_equal_case_by_case_stmt.line_file.clone(),
271 )
272 .into();
273 let verify_result = self
274 .verify_atomic_fact(&equal_to_in_ret_set_atomic_fact, &verify_state)
275 .map_err(|verify_error| {
276 short_exec_error(
277 have_fn_equal_case_by_case_stmt.clone().into(),
278 "",
279 Some(verify_error),
280 vec![],
281 )
282 })?;
283 if verify_result.is_unknown() {
284 let msg = format!(
285 "have_fn_equal_case_by_case_stmt: {} is not in return set {} under case {}",
286 equal_to, have_fn_equal_case_by_case_stmt.fn_set_clause.ret_set, case_fact,
287 );
288 return Err(short_exec_error(
289 have_fn_equal_case_by_case_stmt.clone().into(),
290 msg,
291 None,
292 vec![],
293 ));
294 }
295
296 Ok(())
297 }
298}