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_type = ParamType::Obj(
162 self.inst_obj(
163 param_def_with_set.set_obj(),
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 );
175 algo_param_defs_with_type.push(ParamGroupWithParamType::new(
176 mapped_param_names,
177 instantiated_param_type,
178 ));
179 }
180
181 for in_fact_atomic in param_satisfy_fn_param_set_facts_atomic.iter() {
182 requirement_facts.push(in_fact_atomic.clone().into());
183 }
184 for dom_fact in fn_set_with_dom.dom_facts.iter() {
185 let instantiated_dom_fact = self
186 .inst_or_and_chain_atomic_fact(
187 dom_fact,
188 &fn_set_param_name_to_algo_arg_obj,
189 ParamObjType::Forall,
190 None,
191 )
192 .map_err(|runtime_error| {
193 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
194 def_algo_stmt,
195 "algo verify: failed to instantiate fn set dom fact".to_string(),
196 Some(runtime_error),
197 )
198 })?;
199 requirement_facts.push(instantiated_dom_fact.into());
200 }
201
202 Ok((
203 requirement_facts,
204 ParamDefWithType::new(algo_param_defs_with_type),
205 ))
206 }
207
208 fn build_algo_verification_fn_call_obj(def_algo_stmt: &DefAlgoStmt) -> Obj {
209 let mut fn_call_arg_boxes: Vec<Box<Obj>> = Vec::with_capacity(def_algo_stmt.params.len());
210 for algo_param_name in def_algo_stmt.params.iter() {
211 fn_call_arg_boxes.push(Box::new(obj_for_bound_param_in_scope(
212 algo_param_name.clone(),
213 ParamObjType::Forall,
214 )));
215 }
216 FnObj::new(
217 FnObjHead::Identifier(Identifier::new(def_algo_stmt.name.clone())),
218 vec![fn_call_arg_boxes],
219 )
220 .into()
221 }
222
223 fn requirement_facts_to_exist_or_and_chain_dom_facts(
224 def_algo_stmt: &DefAlgoStmt,
225 requirement_facts: &[Fact],
226 ) -> Result<Vec<ExistOrAndChainAtomicFact>, RuntimeError> {
227 let mut requirement_dom_facts: Vec<ExistOrAndChainAtomicFact> =
228 Vec::with_capacity(requirement_facts.len());
229 for requirement_fact in requirement_facts.iter() {
230 let requirement_dom_fact = match requirement_fact {
231 Fact::AtomicFact(atomic_fact) => atomic_fact.clone().into(),
232 Fact::AndFact(and_fact) => and_fact.clone().into(),
233 Fact::ChainFact(chain_fact) => chain_fact.clone().into(),
234 Fact::OrFact(or_fact) => or_fact.clone().into(),
235 Fact::ExistFact(exist_fact) => exist_fact.clone().into(),
236 Fact::ForallFact(_) | Fact::ForallFactWithIff(_) | Fact::NotForall(_) => {
237 return Err(
238 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
239 def_algo_stmt,
240 "algo verify: requirement fact cannot be forall or not forall"
241 .to_string(),
242 None,
243 ),
244 );
245 }
246 };
247 requirement_dom_facts.push(requirement_dom_fact);
248 }
249 Ok(requirement_dom_facts)
250 }
251
252 fn def_algo_verification_forall_param_map(algo_param_names: &[String]) -> HashMap<String, Obj> {
253 let mut param_to_arg_map = HashMap::with_capacity(algo_param_names.len());
254 for name in algo_param_names.iter() {
255 param_to_arg_map.insert(
256 name.clone(),
257 obj_for_bound_param_in_scope(name.clone(), ParamObjType::Forall),
258 );
259 }
260 param_to_arg_map
261 }
262
263 fn forall_fact_for_def_algo_case(
264 &self,
265 algo_param_defs_with_type: &ParamDefWithType,
266 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
267 algo_case: &AlgoCase,
268 fn_call_obj: &Obj,
269 algo_param_names: &[String],
270 ) -> Result<Fact, RuntimeError> {
271 let param_to_arg_map = Self::def_algo_verification_forall_param_map(algo_param_names);
272 let inst_condition = self.inst_atomic_fact(
273 &algo_case.condition,
274 ¶m_to_arg_map,
275 ParamObjType::Forall,
276 None,
277 )?;
278 let inst_return_value = self.inst_obj(
279 &algo_case.return_stmt.value,
280 ¶m_to_arg_map,
281 ParamObjType::Forall,
282 )?;
283
284 let mut case_dom_facts: Vec<Fact> = Vec::with_capacity(requirement_dom_facts.len() + 1);
285 for requirement_dom_fact in requirement_dom_facts.iter() {
286 case_dom_facts.push(requirement_dom_fact.clone().to_fact());
287 }
288 case_dom_facts.push(inst_condition.into());
289
290 let case_then_facts = vec![EqualFact::new(
291 fn_call_obj.clone(),
292 inst_return_value,
293 algo_case.line_file.clone(),
294 )
295 .into()];
296
297 Ok(ForallFact::new(
298 algo_param_defs_with_type.clone(),
299 case_dom_facts,
300 case_then_facts,
301 algo_case.line_file.clone(),
302 )?
303 .into())
304 }
305
306 fn verify_each_def_algo_case_implies_return(
307 &mut self,
308 def_algo_stmt: &DefAlgoStmt,
309 algo_param_defs_with_type: &ParamDefWithType,
310 fn_call_obj: &Obj,
311 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
312 ) -> Result<(), RuntimeError> {
313 let verify_state = VerifyState::new(0, false);
314 for algo_case in def_algo_stmt.cases.iter() {
315 let case_forall_fact = self.forall_fact_for_def_algo_case(
316 algo_param_defs_with_type,
317 requirement_dom_facts,
318 algo_case,
319 fn_call_obj,
320 &def_algo_stmt.params,
321 )?;
322 self.verify_fact_return_err_if_not_true(&case_forall_fact, &verify_state)
323 .map_err(|runtime_error| {
324 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
325 def_algo_stmt,
326 format!(
327 "algo verify: case `{}` does not imply expected return",
328 algo_case
329 ),
330 Some(runtime_error),
331 )
332 })?;
333 }
334 Ok(())
335 }
336
337 fn verify_def_algo_case_coverage_when_no_default_return(
338 &mut self,
339 def_algo_stmt: &DefAlgoStmt,
340 algo_param_defs_with_type: &ParamDefWithType,
341 requirement_dom_facts: &[ExistOrAndChainAtomicFact],
342 ) -> Result<(), RuntimeError> {
343 if def_algo_stmt.default_return.is_some() {
344 return Ok(());
345 }
346
347 if def_algo_stmt.cases.is_empty() {
348 return Err(
349 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
350 def_algo_stmt,
351 "algo verify: no case and no default return".to_string(),
352 None,
353 ),
354 );
355 }
356
357 let param_to_arg_map = Self::def_algo_verification_forall_param_map(&def_algo_stmt.params);
358 let mut case_conditions: Vec<AndChainAtomicFact> =
359 Vec::with_capacity(def_algo_stmt.cases.len());
360 for algo_case in def_algo_stmt.cases.iter() {
361 let inst_condition = self.inst_atomic_fact(
362 &algo_case.condition,
363 ¶m_to_arg_map,
364 ParamObjType::Forall,
365 None,
366 )?;
367 case_conditions.push(inst_condition.into());
368 }
369 let coverage_or_fact = OrFact::new(case_conditions, def_algo_stmt.line_file.clone());
370 let coverage_forall_fact = ForallFact::new(
371 algo_param_defs_with_type.clone(),
372 requirement_dom_facts
373 .iter()
374 .cloned()
375 .map(ExistOrAndChainAtomicFact::to_fact)
376 .collect(),
377 vec![ExistOrAndChainAtomicFact::OrFact(coverage_or_fact)],
378 def_algo_stmt.line_file.clone(),
379 )?
380 .into();
381
382 let verify_state = VerifyState::new(0, false);
383 self.verify_fact_return_err_if_not_true(&coverage_forall_fact, &verify_state)
384 .map_err(|runtime_error| {
385 Self::def_algo_verify_exec_error_with_message_and_optional_cause(
386 def_algo_stmt,
387 "algo verify: cases do not cover all situations".to_string(),
388 Some(runtime_error),
389 )
390 })?;
391
392 Ok(())
393 }
394}