1use crate::prelude::*;
2use std::collections::HashMap;
3
4impl Runtime {
5 pub fn exec_def_algo_stmt(
6 &mut self,
7 def_algo_stmt: &DefAlgoStmt,
8 ) -> Result<StmtResult, RuntimeError> {
9 self.run_in_local_env(|rt| rt.exec_def_algo_stmt_verify_process(def_algo_stmt))?;
10 self.store_def_algo(def_algo_stmt)?;
11 Ok(NonFactualStmtSuccess::new_with_stmt(def_algo_stmt.clone().into()).into())
12 }
13
14 fn exec_def_algo_stmt_verify_process(
15 &mut self,
16 def_algo_stmt: &DefAlgoStmt,
17 ) -> Result<StmtResult, RuntimeError> {
18 let function_name_obj: Obj = Identifier::new(def_algo_stmt.name.clone()).into();
19 let fn_set_where_algo_belongs = match self.get_object_in_fn_set(&function_name_obj) {
20 Some(fn_set) => fn_set,
21 None => {
22 return Err(Self::def_algo_verify_exec_error_without_message(
23 def_algo_stmt,
24 ));
25 }
26 };
27
28 let (requirement_facts_for_param, algo_param_defs_with_type) = self
29 .collect_requirement_facts_and_algo_param_defs(
30 def_algo_stmt,
31 &fn_set_where_algo_belongs,
32 )?;
33
34 let fn_call_obj_for_verification = Self::build_algo_verification_fn_call_obj(def_algo_stmt);
35 let requirement_dom_facts = Self::requirement_facts_to_exist_or_and_chain_dom_facts(
36 def_algo_stmt,
37 &requirement_facts_for_param,
38 )?;
39
40 self.verify_each_def_algo_case_implies_return(
41 def_algo_stmt,
42 &algo_param_defs_with_type,
43 &fn_call_obj_for_verification,
44 &requirement_dom_facts,
45 )?;
46
47 self.verify_def_algo_case_coverage_when_no_default_return(
48 def_algo_stmt,
49 &algo_param_defs_with_type,
50 &requirement_dom_facts,
51 )?;
52
53 Ok(NonFactualStmtSuccess::new_with_stmt(def_algo_stmt.clone().into()).into())
54 }
55
56 fn def_algo_verify_exec_error_without_message(def_algo_stmt: &DefAlgoStmt) -> RuntimeError {
57 short_exec_error(def_algo_stmt.clone().into(), "", None, vec![])
58 }
59
60 fn def_algo_verify_exec_error_with_message_and_optional_cause(
61 def_algo_stmt: &DefAlgoStmt,
62 message: String,
63 cause: Option<RuntimeError>,
64 ) -> RuntimeError {
65 short_exec_error(def_algo_stmt.clone().into(), message, cause, vec![])
66 }
67
68 fn collect_requirement_facts_and_algo_param_defs(
69 &self,
70 def_algo_stmt: &DefAlgoStmt,
71 fn_set_where_algo_belongs: &FnSetBody,
72 ) -> Result<(Vec<Fact>, ParamDefWithType), RuntimeError> {
73 self.requirement_facts_and_param_defs_for_fn_set_with_dom(
74 def_algo_stmt,
75 fn_set_where_algo_belongs,
76 )
77 }
78
79 fn requirement_facts_and_param_defs_for_fn_set_with_dom(
80 &self,
81 def_algo_stmt: &DefAlgoStmt,
82 fn_set_with_dom: &FnSetBody,
83 ) -> Result<(Vec<Fact>, ParamDefWithType), RuntimeError> {
84 let mut args_for_algo_params: Vec<Obj> = Vec::with_capacity(def_algo_stmt.params.len());
85 for param_name in def_algo_stmt.params.iter() {
86 args_for_algo_params.push(obj_for_bound_param_in_scope(
87 param_name.clone(),
88 ParamObjType::Forall,
89 ));
90 }
91
92 let param_satisfy_fn_param_set_facts_atomic =
93 ParamGroupWithSet::facts_for_args_satisfy_param_def_with_set_vec(
94 self,
95 &fn_set_with_dom.params_def_with_set,
96 &args_for_algo_params,
97 ParamObjType::Forall,
98 )
99 .map_err(|runtime_error| {
100 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
101 def_algo_stmt,
102 "algo verify: failed to build param in-set facts".to_string(),
103 Some(runtime_error),
104 )
105 })?;
106
107 let fn_set_param_names = fn_set_with_dom.get_params();
108 if fn_set_param_names.len() != def_algo_stmt.params.len() {
109 return Err(
110 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
111 def_algo_stmt,
112 format!(
113 "algo verify: number of params mismatch (algo params: {}, fn set params: {})",
114 def_algo_stmt.params.len(),
115 fn_set_param_names.len()
116 ),
117 None,
118 ),
119 );
120 }
121
122 let mut fn_set_param_name_to_algo_arg_obj: HashMap<String, Obj> = HashMap::new();
123 for (fn_set_param_name, algo_param_name) in
124 fn_set_param_names.iter().zip(def_algo_stmt.params.iter())
125 {
126 fn_set_param_name_to_algo_arg_obj.insert(
127 fn_set_param_name.clone(),
128 obj_for_bound_param_in_scope(algo_param_name.clone(), ParamObjType::Forall),
129 );
130 }
131
132 let mut requirement_facts: Vec<Fact> = Vec::new();
133 let mut algo_param_defs_with_type: Vec<ParamGroupWithParamType> =
134 Vec::with_capacity(fn_set_with_dom.params_def_with_set.len());
135
136 for param_def_with_set in fn_set_with_dom.params_def_with_set.iter() {
137 let mut mapped_param_names: Vec<String> =
138 Vec::with_capacity(param_def_with_set.params.len());
139 for fn_set_param_name in param_def_with_set.params.iter() {
140 match fn_set_param_name_to_algo_arg_obj.get(fn_set_param_name) {
141 Some(Obj::Atom(AtomObj::Identifier(identifier))) => {
142 mapped_param_names.push(identifier.name.clone());
143 }
144 Some(Obj::Atom(AtomObj::FnSet(p))) => {
145 mapped_param_names.push(p.name.clone());
146 }
147 Some(Obj::Atom(AtomObj::Forall(p))) => {
148 mapped_param_names.push(p.name.clone());
149 }
150 _ => {
151 return Err(
152 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
153 def_algo_stmt,
154 "algo verify: param map internal error".to_string(),
155 None,
156 ),
157 );
158 }
159 }
160 }
161 let instantiated_param_set = self
162 .inst_obj(
163 ¶m_def_with_set.set,
164 &fn_set_param_name_to_algo_arg_obj,
165 ParamObjType::Forall,
166 )
167 .map_err(|runtime_error| {
168 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
169 def_algo_stmt,
170 "algo verify: failed to instantiate fn set param set".to_string(),
171 Some(runtime_error),
172 )
173 })?;
174 algo_param_defs_with_type.push(ParamGroupWithParamType::new(
175 mapped_param_names,
176 ParamType::Obj(instantiated_param_set),
177 ));
178 }
179
180 for in_fact_atomic in param_satisfy_fn_param_set_facts_atomic.iter() {
181 requirement_facts.push(in_fact_atomic.clone().into());
182 }
183 for dom_fact in fn_set_with_dom.dom_facts.iter() {
184 let instantiated_dom_fact = self
185 .inst_or_and_chain_atomic_fact(
186 dom_fact,
187 &fn_set_param_name_to_algo_arg_obj,
188 ParamObjType::Forall,
189 None,
190 )
191 .map_err(|runtime_error| {
192 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
193 def_algo_stmt,
194 "algo verify: failed to instantiate fn set dom fact".to_string(),
195 Some(runtime_error),
196 )
197 })?;
198 requirement_facts.push(instantiated_dom_fact.into());
199 }
200
201 Ok((
202 requirement_facts,
203 ParamDefWithType::new(algo_param_defs_with_type),
204 ))
205 }
206
207 fn build_algo_verification_fn_call_obj(def_algo_stmt: &DefAlgoStmt) -> Obj {
208 let mut fn_call_arg_boxes: Vec<Box<Obj>> = Vec::with_capacity(def_algo_stmt.params.len());
209 for algo_param_name in def_algo_stmt.params.iter() {
210 fn_call_arg_boxes.push(Box::new(obj_for_bound_param_in_scope(
211 algo_param_name.clone(),
212 ParamObjType::Forall,
213 )));
214 }
215 FnObj::new(
216 FnObjHead::Identifier(Identifier::new(def_algo_stmt.name.clone())),
217 vec![fn_call_arg_boxes],
218 )
219 .into()
220 }
221
222 fn requirement_facts_to_exist_or_and_chain_dom_facts(
223 def_algo_stmt: &DefAlgoStmt,
224 requirement_facts: &[Fact],
225 ) -> Result<Vec<ExistOrAndChainAtomicFact>, RuntimeError> {
226 let mut requirement_dom_facts: Vec<ExistOrAndChainAtomicFact> =
227 Vec::with_capacity(requirement_facts.len());
228 for requirement_fact in requirement_facts.iter() {
229 let requirement_dom_fact = match requirement_fact {
230 Fact::AtomicFact(atomic_fact) => atomic_fact.clone().into(),
231 Fact::AndFact(and_fact) => and_fact.clone().into(),
232 Fact::ChainFact(chain_fact) => chain_fact.clone().into(),
233 Fact::OrFact(or_fact) => or_fact.clone().into(),
234 Fact::ExistFact(exist_fact) => exist_fact.clone().into(),
235 Fact::ForallFact(_) | Fact::ForallFactWithIff(_) | Fact::NotForall(_) => {
236 return Err(
237 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
238 def_algo_stmt,
239 "algo verify: requirement fact cannot be forall or not forall"
240 .to_string(),
241 None,
242 ),
243 );
244 }
245 };
246 requirement_dom_facts.push(requirement_dom_fact);
247 }
248 Ok(requirement_dom_facts)
249 }
250
251 fn def_algo_verification_forall_param_map(algo_param_names: &[String]) -> HashMap<String, Obj> {
252 let mut param_to_arg_map = HashMap::with_capacity(algo_param_names.len());
253 for name in algo_param_names.iter() {
254 param_to_arg_map.insert(
255 name.clone(),
256 obj_for_bound_param_in_scope(name.clone(), ParamObjType::Forall),
257 );
258 }
259 param_to_arg_map
260 }
261
262 fn forall_fact_for_def_algo_case(
263 &self,
264 algo_param_defs_with_type: &ParamDefWithType,
265 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
266 algo_case: &AlgoCase,
267 fn_call_obj: &Obj,
268 algo_param_names: &[String],
269 ) -> Result<Fact, RuntimeError> {
270 let param_to_arg_map = Self::def_algo_verification_forall_param_map(algo_param_names);
271 let inst_condition = self.inst_atomic_fact(
272 &algo_case.condition,
273 ¶m_to_arg_map,
274 ParamObjType::Forall,
275 None,
276 )?;
277 let inst_return_value = self.inst_obj(
278 &algo_case.return_stmt.value,
279 ¶m_to_arg_map,
280 ParamObjType::Forall,
281 )?;
282
283 let mut case_dom_facts: Vec<Fact> = Vec::with_capacity(requirement_dom_facts.len() + 1);
284 for requirement_dom_fact in requirement_dom_facts.iter() {
285 case_dom_facts.push(requirement_dom_fact.clone().to_fact());
286 }
287 case_dom_facts.push(inst_condition.into());
288
289 let case_then_facts = vec![EqualFact::new(
290 fn_call_obj.clone(),
291 inst_return_value,
292 algo_case.line_file.clone(),
293 )
294 .into()];
295
296 Ok(ForallFact::new(
297 algo_param_defs_with_type.clone(),
298 case_dom_facts,
299 case_then_facts,
300 algo_case.line_file.clone(),
301 )?
302 .into())
303 }
304
305 fn verify_each_def_algo_case_implies_return(
306 &mut self,
307 def_algo_stmt: &DefAlgoStmt,
308 algo_param_defs_with_type: &ParamDefWithType,
309 fn_call_obj: &Obj,
310 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
311 ) -> Result<(), RuntimeError> {
312 let verify_state = VerifyState::new(0, false);
313 for algo_case in def_algo_stmt.cases.iter() {
314 let case_forall_fact = self.forall_fact_for_def_algo_case(
315 algo_param_defs_with_type,
316 requirement_dom_facts,
317 algo_case,
318 fn_call_obj,
319 &def_algo_stmt.params,
320 )?;
321 self.verify_fact_return_err_if_not_true(&case_forall_fact, &verify_state)
322 .map_err(|runtime_error| {
323 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
324 def_algo_stmt,
325 format!(
326 "algo verify: case `{}` does not imply expected return",
327 algo_case
328 ),
329 Some(runtime_error),
330 )
331 })?;
332 }
333 Ok(())
334 }
335
336 fn verify_def_algo_case_coverage_when_no_default_return(
337 &mut self,
338 def_algo_stmt: &DefAlgoStmt,
339 algo_param_defs_with_type: &ParamDefWithType,
340 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
341 ) -> Result<(), RuntimeError> {
342 if def_algo_stmt.default_return.is_some() {
343 return Ok(());
344 }
345
346 if def_algo_stmt.cases.is_empty() {
347 return Err(
348 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
349 def_algo_stmt,
350 "algo verify: no case and no default return".to_string(),
351 None,
352 ),
353 );
354 }
355
356 let param_to_arg_map = Self::def_algo_verification_forall_param_map(&def_algo_stmt.params);
357 let mut case_conditions: Vec<AndChainAtomicFact> =
358 Vec::with_capacity(def_algo_stmt.cases.len());
359 for algo_case in def_algo_stmt.cases.iter() {
360 let inst_condition = self.inst_atomic_fact(
361 &algo_case.condition,
362 ¶m_to_arg_map,
363 ParamObjType::Forall,
364 None,
365 )?;
366 case_conditions.push(inst_condition.into());
367 }
368 let coverage_or_fact = OrFact::new(case_conditions, def_algo_stmt.line_file.clone());
369 let coverage_forall_fact = ForallFact::new(
370 algo_param_defs_with_type.clone(),
371 requirement_dom_facts
372 .iter()
373 .cloned()
374 .map(ExistOrAndChainAtomicFact::to_fact)
375 .collect(),
376 vec![ExistOrAndChainAtomicFact::OrFact(coverage_or_fact)],
377 def_algo_stmt.line_file.clone(),
378 )?
379 .into();
380
381 let verify_state = VerifyState::new(0, false);
382 self.verify_fact_return_err_if_not_true(&coverage_forall_fact, &verify_state)
383 .map_err(|runtime_error| {
384 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
385 def_algo_stmt,
386 "algo verify: cases do not cover all situations".to_string(),
387 Some(runtime_error),
388 )
389 })?;
390
391 Ok(())
392 }
393}