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