1use crate::prelude::*;
2use std::collections::HashMap;
3
4fn fn_set_equality_fact(left: &FnSet, right: &FnSet, line_file: LineFile) -> Fact {
5 EqualFact::new(left.clone().into(), right.clone().into(), line_file).into()
6}
7
8fn fn_set_equality_verify_error(
9 left: &FnSet,
10 right: &FnSet,
11 line_file: LineFile,
12 message: String,
13 cause: Option<RuntimeError>,
14) -> RuntimeError {
15 {
16 VerifyRuntimeError(RuntimeErrorStruct::new(
17 Some(fn_set_equality_fact(left, right, line_file.clone()).into_stmt()),
18 message,
19 line_file,
20 cause,
21 vec![],
22 ))
23 .into()
24 }
25}
26
27fn fn_set_equality_verified_by_builtin_rules_result(
28 left: &FnSet,
29 right: &FnSet,
30 line_file: LineFile,
31) -> StmtResult {
32 let stmt = fn_set_equality_fact(left, right, line_file);
33 StmtResult::FactualStmtSuccess(
34 FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
35 stmt,
36 "fnset equality: mutual implication of param sets, dom facts, and ret set".to_string(),
37 Vec::new(),
38 ),
39 )
40}
41
42impl Runtime {
43 pub fn verify_fn_set_with_params_equality_by_builtin_rules(
44 &mut self,
45 left: &FnSet,
46 right: &FnSet,
47 line_file: LineFile,
48 verify_state: &VerifyState,
49 ) -> Result<StmtResult, RuntimeError> {
50 if ParamGroupWithSet::number_of_params(&left.body.params_def_with_set)
51 != ParamGroupWithSet::number_of_params(&right.body.params_def_with_set)
52 {
53 return Ok((StmtUnknown::new()).into());
54 }
55
56 let left_implies_right = self.verify_fn_set_with_params_directionally_in_local_env(
57 left,
58 right,
59 line_file.clone(),
60 verify_state,
61 )?;
62 if !left_implies_right {
63 return Ok((StmtUnknown::new()).into());
64 }
65
66 let right_implies_left = self.verify_fn_set_with_params_directionally_in_local_env(
67 right,
68 left,
69 line_file.clone(),
70 verify_state,
71 )?;
72 if !right_implies_left {
73 return Ok((StmtUnknown::new()).into());
74 }
75
76 Ok(fn_set_equality_verified_by_builtin_rules_result(
77 left, right, line_file,
78 ))
79 }
80
81 fn verify_fn_set_with_params_directionally_in_local_env(
82 &mut self,
83 source: &FnSet,
84 target: &FnSet,
85 line_file: LineFile,
86 verify_state: &VerifyState,
87 ) -> Result<bool, RuntimeError> {
88 self.run_in_local_env(|rt| {
89 rt.verify_fn_set_with_params_directionally_in_local_env_body(
90 source,
91 target,
92 line_file,
93 verify_state,
94 )
95 })
96 }
97
98 fn verify_fn_set_with_params_directionally_in_local_env_body(
99 &mut self,
100 source: &FnSet,
101 target: &FnSet,
102 line_file: LineFile,
103 verify_state: &VerifyState,
104 ) -> Result<bool, RuntimeError> {
105 let target_flat_param_names =
106 ParamGroupWithSet::collect_param_names(&target.body.params_def_with_set);
107 let generated_param_names =
108 self.generate_random_unused_names(target_flat_param_names.len());
109 let source_param_to_generated_arg_map = self
110 .define_directional_source_fn_set_params_in_local_env(
111 source,
112 &generated_param_names,
113 target,
114 line_file.clone(),
115 )?;
116 let target_param_to_generated_arg_map = Self::build_param_to_generated_arg_map(
117 &target_flat_param_names,
118 &generated_param_names,
119 );
120
121 self.assume_directional_source_fn_set_dom_facts_in_local_env(
122 source,
123 &source_param_to_generated_arg_map,
124 target,
125 line_file.clone(),
126 )?;
127
128 if !self.verify_directional_target_fn_set_param_membership_facts(
129 source,
130 target,
131 &target_param_to_generated_arg_map,
132 line_file.clone(),
133 verify_state,
134 )? {
135 return Ok(false);
136 }
137
138 if !self.verify_directional_target_fn_set_dom_facts(
139 source,
140 target,
141 line_file.clone(),
142 &target_param_to_generated_arg_map,
143 verify_state,
144 )? {
145 return Ok(false);
146 }
147
148 let source_ret_set = self
149 .inst_obj(
150 &source.body.ret_set,
151 &source_param_to_generated_arg_map,
152 ParamObjType::FnSet,
153 )
154 .map_err(|e| {
155 fn_set_equality_verify_error(
156 source,
157 target,
158 line_file.clone(),
159 "failed to instantiate source ret set for fnset equality check".to_string(),
160 Some(e),
161 )
162 })?;
163 let target_ret_set = self
164 .inst_obj(
165 &target.body.ret_set,
166 &target_param_to_generated_arg_map,
167 ParamObjType::FnSet,
168 )
169 .map_err(|e| {
170 fn_set_equality_verify_error(
171 source,
172 target,
173 line_file.clone(),
174 "failed to instantiate target ret set for fnset equality check".to_string(),
175 Some(e),
176 )
177 })?;
178 let ret_equal_fact = EqualFact::new(source_ret_set, target_ret_set, line_file);
179 let ret_equal_result = self.verify_equal_fact(&ret_equal_fact, verify_state)?;
180 Ok(ret_equal_result.is_true())
181 }
182
183 fn build_param_to_generated_arg_map(
184 flat_param_names: &[String],
185 generated_param_names: &[String],
186 ) -> HashMap<String, Obj> {
187 let mut param_to_generated_arg_map: HashMap<String, Obj> =
188 HashMap::with_capacity(flat_param_names.len());
189 for (param_name, generated_param_name) in
190 flat_param_names.iter().zip(generated_param_names.iter())
191 {
192 param_to_generated_arg_map.insert(
193 param_name.clone(),
194 obj_for_bound_param_in_scope(generated_param_name.clone(), ParamObjType::FnSet),
195 );
196 }
197 param_to_generated_arg_map
198 }
199
200 pub(crate) fn fn_set_alpha_renamed_for_display_compare(
204 &self,
205 fn_set: &FnSetBody,
206 generated_flat_names: &[String],
207 ) -> Result<Obj, RuntimeError> {
208 let flat = ParamGroupWithSet::collect_param_names(&fn_set.params_def_with_set);
209 if flat.len() != generated_flat_names.len() {
210 return Err(
211 VerifyRuntimeError(RuntimeErrorStruct::new_with_just_msg("internal: fn_set alpha rename requires generated_flat_names len == flat param count"
212 .to_string()))
213 .into(),
214 );
215 }
216 let map = Self::build_param_to_generated_arg_map(&flat, generated_flat_names);
217 let mut new_params = Vec::with_capacity(fn_set.params_def_with_set.len());
218 let mut c_idx: usize = 0;
219 for g in fn_set.params_def_with_set.iter() {
220 let n = g.params.len();
221 let names = generated_flat_names[c_idx..c_idx + n].to_vec();
222 c_idx += n;
223 let new_set = self.inst_obj(g.set_obj(), &map, ParamObjType::FnSet)?;
224 new_params.push(ParamGroupWithSet::new(names, new_set));
225 }
226 let mut new_dom = Vec::with_capacity(fn_set.dom_facts.len());
227 for d in fn_set.dom_facts.iter() {
228 new_dom.push(self.inst_or_and_chain_atomic_fact(d, &map, ParamObjType::FnSet, None)?);
229 }
230 let new_ret = self.inst_obj(fn_set.ret_set.as_ref(), &map, ParamObjType::FnSet)?;
231 Ok(FnSet::new(new_params, new_dom, new_ret)?.into())
232 }
233
234 fn define_directional_source_fn_set_params_in_local_env(
235 &mut self,
236 source: &FnSet,
237 generated_param_names: &[String],
238 target: &FnSet,
239 line_file: LineFile,
240 ) -> Result<HashMap<String, Obj>, RuntimeError> {
241 let mut source_param_to_generated_arg_map: HashMap<String, Obj> =
242 HashMap::with_capacity(generated_param_names.len());
243 let mut flat_index: usize = 0;
244
245 for param_def_with_set in source.body.params_def_with_set.iter() {
246 let next_flat_index = flat_index + param_def_with_set.params.len();
247 let generated_names_for_current_group =
248 generated_param_names[flat_index..next_flat_index].to_vec();
249 let instantiated_param_set = self
250 .inst_obj(
251 param_def_with_set.set_obj(),
252 &source_param_to_generated_arg_map,
253 ParamObjType::FnSet,
254 )
255 .map_err(|e| {
256 fn_set_equality_verify_error(
257 source,
258 target,
259 line_file.clone(),
260 "failed to instantiate source fnset param set".to_string(),
261 Some(e),
262 )
263 })?;
264 let generated_param_def = ParamGroupWithSet::new(
265 generated_names_for_current_group.clone(),
266 instantiated_param_set,
267 );
268 self.define_params_with_set(&generated_param_def)
269 .map_err(|e| {
270 fn_set_equality_verify_error(
271 source,
272 target,
273 line_file.clone(),
274 "failed to define fresh params for directional fnset equality verification"
275 .to_string(),
276 Some(e),
277 )
278 })?;
279
280 for (source_param_name, generated_param_name) in param_def_with_set
281 .params
282 .iter()
283 .zip(generated_names_for_current_group.iter())
284 {
285 source_param_to_generated_arg_map.insert(
286 source_param_name.clone(),
287 obj_for_bound_param_in_scope(generated_param_name.clone(), ParamObjType::FnSet),
288 );
289 }
290 flat_index = next_flat_index;
291 }
292
293 Ok(source_param_to_generated_arg_map)
294 }
295
296 fn assume_directional_source_fn_set_dom_facts_in_local_env(
297 &mut self,
298 source: &FnSet,
299 source_param_to_generated_arg_map: &HashMap<String, Obj>,
300 target: &FnSet,
301 line_file: LineFile,
302 ) -> Result<(), RuntimeError> {
303 for dom_fact in source.body.dom_facts.iter() {
304 let instantiated_dom_fact = self
305 .inst_or_and_chain_atomic_fact(
306 dom_fact,
307 source_param_to_generated_arg_map,
308 ParamObjType::FnSet,
309 None,
310 )
311 .map_err(|e| {
312 fn_set_equality_verify_error(
313 source,
314 target,
315 line_file.clone(),
316 "failed to instantiate source fnset dom fact".to_string(),
317 Some(e),
318 )
319 })?;
320 self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
321 instantiated_dom_fact.into(),
322 )
323 .map_err(|e| {
324 fn_set_equality_verify_error(
325 source,
326 target,
327 line_file.clone(),
328 "failed to assume source fnset dom fact in local equality environment"
329 .to_string(),
330 Some(e),
331 )
332 })?;
333 }
334 Ok(())
335 }
336
337 fn verify_directional_target_fn_set_param_membership_facts(
338 &mut self,
339 source: &FnSet,
340 target: &FnSet,
341 target_param_to_generated_arg_map: &HashMap<String, Obj>,
342 line_file: LineFile,
343 verify_state: &VerifyState,
344 ) -> Result<bool, RuntimeError> {
345 for param_def_with_set in target.body.params_def_with_set.iter() {
346 let instantiated_param_type = ParamType::Obj(
347 self.inst_obj(
348 param_def_with_set.set_obj(),
349 target_param_to_generated_arg_map,
350 ParamObjType::FnSet,
351 )
352 .map_err(|e| {
353 fn_set_equality_verify_error(
354 source,
355 target,
356 line_file.clone(),
357 "failed to instantiate target fnset param set".to_string(),
358 Some(e),
359 )
360 })?,
361 );
362 for param_name in param_def_with_set.params.iter() {
363 let Some(generated_param_obj) =
364 target_param_to_generated_arg_map.get(param_name).cloned()
365 else {
366 return Err(fn_set_equality_verify_error(
367 source,
368 target,
369 line_file.clone(),
370 "internal error: missing generated param while verifying fnset equality"
371 .to_string(),
372 None,
373 ));
374 };
375 let verify_result = self.verify_obj_satisfies_param_type(
376 generated_param_obj,
377 &instantiated_param_type,
378 verify_state,
379 )?;
380 if !verify_result.is_true() {
381 return Ok(false);
382 }
383 }
384 }
385 Ok(true)
386 }
387
388 fn verify_directional_target_fn_set_dom_facts(
389 &mut self,
390 source: &FnSet,
391 target: &FnSet,
392 line_file: LineFile,
393 target_param_to_generated_arg_map: &HashMap<String, Obj>,
394 verify_state: &VerifyState,
395 ) -> Result<bool, RuntimeError> {
396 for dom_fact in target.body.dom_facts.iter() {
397 let instantiated_dom_fact = self
398 .inst_or_and_chain_atomic_fact(
399 dom_fact,
400 target_param_to_generated_arg_map,
401 ParamObjType::FnSet,
402 None,
403 )
404 .map_err(|e| {
405 fn_set_equality_verify_error(
406 source,
407 target,
408 line_file.clone(),
409 "failed to instantiate target fnset dom fact".to_string(),
410 Some(e),
411 )
412 })?;
413 let verify_result =
414 self.verify_or_and_chain_atomic_fact(&instantiated_dom_fact, verify_state)?;
415 if !verify_result.is_true() {
416 return Ok(false);
417 }
418 }
419 Ok(true)
420 }
421}