1use crate::prelude::*;
2use crate::verify::number_is_in_z;
3
4impl Runtime {
5 pub fn parse_def_prop_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
6 let stmt = self.run_in_local_parsing_time_name_scope(|this| {
7 tb.skip_token(PROP)?;
8 let name = this.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
9 let param_defs = this.parse_def_braced_param_groups_with_param_type(tb)?;
10 let def_param_names = param_defs.collect_param_names();
11
12 if tb.current_token_is_equal_to(COLON) {
13 tb.skip_token(COLON)?;
14 } else {
15 if !tb.exceed_end_of_head() {
16 return Err(RuntimeError::from(ParseRuntimeError(
17 RuntimeErrorStruct::new_with_msg_and_line_file(
18 "expect `:` or end of line after `)` in prop statement".to_string(),
19 tb.line_file.clone(),
20 ),
21 )));
22 } else {
23 this.parsing_free_param_collection
24 .end_scope(ParamObjType::DefHeader, &def_param_names);
25 return Ok(DefPropStmt::new(
26 name,
27 param_defs,
28 vec![],
29 tb.line_file.clone(),
30 ));
31 }
32 }
33
34 let facts_result = this.parse_facts_in_body(tb);
35 this.parsing_free_param_collection
36 .end_scope(ParamObjType::DefHeader, &def_param_names);
37 let facts = facts_result?;
38 Ok(DefPropStmt::new(
39 name,
40 param_defs,
41 facts,
42 tb.line_file.clone(),
43 ))
44 });
45
46 let stmt_ok = stmt?;
47 self.insert_parsed_name_into_top_parsing_time_name_scope(
48 &stmt_ok.name,
49 tb.line_file.clone(),
50 )?;
51
52 Ok(stmt_ok.into())
53 }
54
55 pub fn parse_def_abstract_prop_stmt(
56 &mut self,
57 tb: &mut TokenBlock,
58 ) -> Result<Stmt, RuntimeError> {
59 let stmt: Result<DefAbstractPropStmt, RuntimeError> = self
60 .run_in_local_parsing_time_name_scope(|this| {
61 tb.skip_token(ABSTRACT_PROP)?;
62 let name = this.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
63 tb.skip_token(LEFT_BRACE)?;
64 let mut params = vec![];
65 while tb.current()? != RIGHT_BRACE {
66 params.push(tb.advance()?);
67 if !tb.current_token_is_equal_to(RIGHT_BRACE) {
68 tb.skip_token(COMMA)?;
69 }
70 }
71 tb.skip_token(RIGHT_BRACE)?;
72
73 this.register_collected_param_names_for_def_parse(¶ms, tb.line_file.clone())?;
74
75 Ok(DefAbstractPropStmt::new(name, params, tb.line_file.clone()))
76 });
77
78 let stmt_ok = stmt?;
79 self.insert_parsed_name_into_top_parsing_time_name_scope(
80 &stmt_ok.name,
81 tb.line_file.clone(),
82 )?;
83 Ok(stmt_ok.into())
84 }
85
86 pub fn parse_def_let_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
87 tb.skip_token(LET)?;
88 let mut param_def: Vec<ParamGroupWithParamType> = vec![];
89 loop {
90 match tb.current() {
91 Ok(t) if t == COLON => break,
92 Err(_) => break,
93 Ok(_) => {}
94 }
95 param_def.push(
96 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Identifier)?,
97 );
98 }
99 let param_def = ParamDefWithType::new(param_def);
100 let all_param_names = param_def.collect_param_names();
101 self.register_collected_param_names_for_def_parse(&all_param_names, tb.line_file.clone())?;
102
103 let facts = if tb.current_token_is_equal_to(COLON) {
104 tb.skip_token(COLON)?;
105
106 if !tb.exceed_end_of_head() {
107 return Err(RuntimeError::from(ParseRuntimeError(
108 RuntimeErrorStruct::new_with_msg_and_line_file(
109 "expect end of line after `:` in let statement".to_string(),
110 tb.line_file.clone(),
111 ),
112 )));
113 }
114 let facts_result = self.parse_facts_in_body(tb);
115 self.parsing_free_param_collection
116 .end_scope(ParamObjType::Identifier, &all_param_names);
117 facts_result?
118 } else {
119 if !all_param_names.is_empty() {
120 self.parsing_free_param_collection
121 .end_scope(ParamObjType::Identifier, &all_param_names);
122 }
123 vec![]
124 };
125 Ok(DefLetStmt::new(param_def, facts, tb.line_file.clone()).into())
126 }
127
128 pub fn parse_have_obj_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
130 tb.skip_token(HAVE)?;
131 let mut param_defs: Vec<ParamGroupWithParamType> = vec![];
132 loop {
133 param_defs.push(
134 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Identifier)?,
135 );
136 match tb.current() {
137 Ok(t) if t == EQUAL => break,
138 Err(_) => break,
139 Ok(_) => {}
140 }
141 }
142 if param_defs.is_empty() {
143 return Err(RuntimeError::from(ParseRuntimeError(
144 RuntimeErrorStruct::new_with_msg_and_line_file(
145 "have expects at least one param type pair".to_string(),
146 tb.line_file.clone(),
147 ),
148 )));
149 }
150 let param_defs = ParamDefWithType::new(param_defs);
151 let have_param_names = param_defs.collect_param_names();
152 self.register_collected_param_names_for_def_parse(&have_param_names, tb.line_file.clone())?;
153
154 if tb.current().map(|t| t != EQUAL).unwrap_or(true) {
155 if !have_param_names.is_empty() {
156 self.parsing_free_param_collection
157 .end_scope(ParamObjType::Identifier, &have_param_names);
158 }
159 Ok(HaveObjInNonemptySetOrParamTypeStmt::new(param_defs, tb.line_file.clone()).into())
160 } else {
161 tb.skip_token(EQUAL)?;
162 let objs_result = (|| -> Result<Vec<Obj>, RuntimeError> {
163 let mut objs_equal_to = vec![self.parse_obj(tb)?];
164 while matches!(tb.current(), Ok(t) if t == COMMA) {
165 tb.skip_token(COMMA)?;
166 objs_equal_to.push(self.parse_obj(tb)?);
167 }
168 Ok(objs_equal_to)
169 })();
170 self.parsing_free_param_collection
171 .end_scope(ParamObjType::Identifier, &have_param_names);
172 let objs_equal_to = objs_result?;
173 Ok(HaveObjEqualStmt::new(param_defs, objs_equal_to, tb.line_file.clone()).into())
174 }
175 }
176
177 pub fn parse_have_fn_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
178 tb.skip_token(HAVE)?;
179 tb.skip_token(FN_LOWER_CASE)?;
180 if tb.current_token_is_equal_to(BY) {
181 tb.skip_token(BY)?;
182 self.parse_have_fn_by_induc_stmt(tb)
183 } else {
184 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
185
186 let fs = self.parse_fn_set_clause(tb)?;
187 let fn_param_names = fs.collect_all_param_names_including_nested_ret_fn_sets();
188
189 if tb.current_token_is_equal_to(COLON) {
190 tb.skip_token(COLON)?;
191 let case_block_count = tb.body.len();
192 let mut cases: Vec<AndChainAtomicFact> = Vec::with_capacity(case_block_count);
193 let mut equal_tos: Vec<Obj> = Vec::with_capacity(case_block_count);
194 for block in tb.body.iter_mut() {
195 block.skip_token(CASE)?;
196 let case_lf = block.line_file.clone();
197 cases.push(self.with_optional_free_param_scope(
198 ParamObjType::FnSet,
199 &fn_param_names,
200 case_lf,
201 |this| this.parse_and_chain_atomic_fact(block),
202 )?);
203 block.skip_token(COLON)?;
204 let rhs_lf = block.line_file.clone();
205 equal_tos.push(self.with_optional_free_param_scope(
206 ParamObjType::FnSet,
207 &fn_param_names,
208 rhs_lf,
209 |this| this.parse_obj(block),
210 )?);
211 }
212 Ok(
213 HaveFnEqualCaseByCaseStmt::new(
214 name,
215 fs,
216 cases,
217 equal_tos,
218 tb.line_file.clone(),
219 )
220 .into(),
221 )
222 } else {
223 tb.skip_token(EQUAL)?;
224
225 let lf = tb.line_file.clone();
226 let equal_to = self.with_optional_free_param_scope(
227 ParamObjType::FnSet,
228 &fn_param_names,
229 lf,
230 |this| this.parse_obj(tb),
231 )?;
232 Ok(HaveFnEqualStmt::new(name, fs, equal_to, tb.line_file.clone()).into())
233 }
234 }
235 }
236
237 fn parse_have_fn_by_induc_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
241 tb.skip_token(INDUC)?;
242 tb.skip_token(FROM)?;
243 let induc_from = self.parse_obj(tb)?;
244 tb.skip_token(COLON)?;
245 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
246
247 tb.skip_token(LEFT_BRACE)?;
248 let param = tb.advance()?;
249 if !tb.current_token_is_equal_to(Z) {
250 return Err(RuntimeError::from(ParseRuntimeError(
251 RuntimeErrorStruct::new_with_msg_and_line_file(
252 "have fn by induc from: expected `Z` after parameter name".to_string(),
253 tb.line_file.clone(),
254 ),
255 )));
256 }
257 tb.skip_token(Z)?;
258 tb.skip_token(COLON)?;
259
260 self.run_in_local_parsing_time_name_scope(|this| {
261 this.parse_have_fn_by_induc_stmt_after_param_scope(tb, name, param, induc_from)
262 })
263 }
264
265 fn parse_have_fn_by_induc_stmt_after_param_scope(
266 &mut self,
267 tb: &mut TokenBlock,
268 name: String,
269 param: String,
270 induc_from: Obj,
271 ) -> Result<Stmt, RuntimeError> {
272 self.validate_user_fn_param_names_for_parse(&[param.clone()], tb.line_file.clone())?;
273 let dom_and_chain = self.parse_and_chain_atomic_fact(tb)?;
274 Self::verify_have_fn_by_induc_dom_matches_induc_from(
275 &dom_and_chain,
276 ¶m,
277 &induc_from,
278 tb.line_file.clone(),
279 )?;
280 tb.skip_token(RIGHT_BRACE)?;
281 let ret_set = self.parse_obj(tb)?;
282
283 if !tb.current_token_is_equal_to(COLON) {
284 return Err(RuntimeError::from(ParseRuntimeError(
285 RuntimeErrorStruct::new_with_msg_and_line_file(
286 "have fn by induc from: expected `:` before case blocks".to_string(),
287 tb.line_file.clone(),
288 ),
289 )));
290 }
291 tb.skip_token(COLON)?;
292
293 let num_blocks = tb.body.len();
294 if num_blocks <= 1 {
295 return Err(RuntimeError::from(ParseRuntimeError(
296 RuntimeErrorStruct::new_with_msg_and_line_file(
297 "have fn by induc from: expected at least two case blocks".to_string(),
298 tb.line_file.clone(),
299 ),
300 )));
301 }
302
303 let num_special = num_blocks - 1;
304 let mut special_cases_equal_tos: Vec<Obj> = Vec::with_capacity(num_special);
305
306 let induc_from_is_number_obj = matches!(induc_from, Obj::Number(_));
307 if induc_from_is_number_obj {
308 if let Obj::Number(n) = &induc_from {
309 if !number_is_in_z(n) {
310 return Err(
311 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
312 "have fn by induc from: when `from` is a number literal, it must be an integer, got {}",
313 induc_from.to_string()
314 ), tb.line_file.clone()))));
315 }
316 }
317 }
318
319 for i in 0..num_special {
320 let block = &mut tb.body[i];
321 block.skip_token(CASE)?;
322
323 block.skip_token(¶m)?;
324
325 block.skip_token(EQUAL)?;
326
327 let slot_label = self.parse_obj(block)?;
328 Self::verify_have_fn_by_induc_special_case_slot_label(
329 &slot_label,
330 i,
331 block.line_file.clone(),
332 )?;
333
334 if induc_from_is_number_obj {
335 let induc_from_add_i: Obj = Add::new(
336 induc_from.clone(),
337 Into::<Obj>::into(Number::new(i.to_string())),
338 )
339 .into();
340
341 if !induc_from_add_i
342 .two_objs_can_be_calculated_and_equal_by_calculation(&slot_label)
343 {
344 return Err(
345 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
346 "have fn by induc from: when `from` is a number literal, special case must be `case {} = {}:` (`from` + {}), got {}",
347 param, induc_from_add_i.to_string(), i, slot_label.to_string()
348 ), block.line_file.clone()))));
349 }
350 } else {
351 let induc_from_add_i: Obj = Add::new(
352 induc_from.clone(),
353 Into::<Obj>::into(Number::new(i.to_string())),
354 )
355 .into();
356
357 if induc_from_add_i.to_string() != slot_label.to_string() {
358 return Err(
359 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
360 "have fn by induc from: when `from` is not a number literal, special case must be `case {} = {}:`, got {}",
361 param, induc_from_add_i.to_string(), slot_label.to_string()
362 ), block.line_file.clone()))));
363 }
364 }
365
366 block.skip_token(COLON)?;
367 if !block.exceed_end_of_head() {
368 special_cases_equal_tos.push(self.parse_obj(block)?);
369 } else {
370 return Err(
371 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: special case must be `case <index>: <obj>` on one line"
372 .to_string(), block.line_file.clone()))));
373 }
374 }
375
376 let induc_names_last = [param.clone()];
377 let last_case_line = tb.body[num_blocks - 1].line_file.clone();
378 let last_case = self.parse_in_local_free_param_scope(
379 ParamObjType::Induc,
380 &induc_names_last,
381 last_case_line,
382 |this| {
383 let last_block = &mut tb.body[num_blocks - 1];
384 last_block.skip_token(CASE)?;
385 last_block.skip_token(¶m)?;
386 last_block.skip_token(GREATER_EQUAL)?;
387 let last_bound = this.parse_obj(last_block)?;
388
389 if induc_from_is_number_obj {
390 let induc_from_add_n: Obj = Add::new(
391 induc_from.clone(),
392 Into::<Obj>::into(Number::new(num_special.to_string())),
393 )
394 .into();
395 if !induc_from_add_n
396 .two_objs_can_be_calculated_and_equal_by_calculation(&last_bound)
397 {
398 return Err(
399 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
400 "have fn by induc from: when `from` is a number literal, last case must be `case >= {}:` (`from` + {}), got {}",
401 induc_from_add_n.to_string(), num_special, last_bound.to_string()
402 ), last_block.line_file.clone()))));
403 }
404 } else {
405 let induc_from_add_n: Obj = Add::new(
406 induc_from.clone(),
407 Into::<Obj>::into(Number::new(num_special.to_string())),
408 )
409 .into();
410 if induc_from_add_n.to_string() != last_bound.to_string() {
411 return Err(
412 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
413 "have fn by induc from: when `from` is not a number literal, last case must be `case >= {}:`, got {}",
414 induc_from_add_n.to_string(), last_bound.to_string()
415 ), last_block.line_file.clone()))));
416 }
417 }
418
419 last_block.skip_token(COLON)?;
420
421 if !last_block.exceed_end_of_head() {
422 let last_obj = this.parse_obj(last_block)?;
423 if !last_block.exceed_end_of_head() {
424 return Err(
425 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: unexpected tokens after `obj` in last case"
426 .to_string(), last_block.line_file.clone()))));
427 }
428 if !last_block.body.is_empty() {
429 return Err(
430 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: if last case has `:` and an object on the same line, it must not have a nested body"
431 .to_string(), last_block.line_file.clone()))));
432 }
433 Ok(HaveFnByInducLastCase::EqualTo(last_obj))
434 } else if !last_block.body.is_empty() {
435 let mut nested: Vec<HaveFnByInducNestedCase> =
436 Vec::with_capacity(last_block.body.len());
437 for sub in last_block.body.iter_mut() {
438 sub.skip_token(CASE)?;
439 let w = this.parse_and_chain_atomic_fact(sub)?;
440 sub.skip_token(COLON)?;
441 if sub.exceed_end_of_head() {
442 return Err(
443 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must be `case <when>: <obj>`"
444 .to_string(), sub.line_file.clone()))));
445 }
446 let o = this.parse_obj(sub)?;
447 if !sub.body.is_empty() {
448 return Err(
449 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must not have further indentation"
450 .to_string(), sub.line_file.clone()))));
451 }
452 nested.push(HaveFnByInducNestedCase {
453 case_fact: w,
454 equal_to: o,
455 });
456 }
457 Ok(HaveFnByInducLastCase::NestedCases(nested))
458 } else {
459 Err(RuntimeError::from(ParseRuntimeError(
460 RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: last case must end with `: <obj>` or `:` with nested `case` blocks"
461 .to_string(), last_block.line_file.clone()),
462 )))
463 }
464 },
465 )?;
466
467 Ok(HaveFnByInducStmt::new(
468 name,
469 param,
470 ret_set,
471 induc_from,
472 special_cases_equal_tos,
473 last_case,
474 tb.line_file.clone(),
475 )
476 .into())
477 }
478
479 fn verify_have_fn_by_induc_dom_matches_induc_from(
480 when: &AndChainAtomicFact,
481 param_name: &str,
482 induc_from: &Obj,
483 line_file: LineFile,
484 ) -> Result<(), RuntimeError> {
485 let ge = match when {
486 AndChainAtomicFact::AtomicFact(AtomicFact::GreaterEqualFact(ge)) => ge,
487 _ => {
488 return Err(RuntimeError::from(ParseRuntimeError(
489 RuntimeErrorStruct::new_with_msg_and_line_file(
490 "have fn by induc from: dom fact must be a single `>=` fact".to_string(),
491 line_file,
492 ),
493 )));
494 }
495 };
496 match &ge.left {
497 Obj::Atom(AtomObj::Identifier(id)) if id.name == param_name => {}
498 _ => {
499 return Err(RuntimeError::from(ParseRuntimeError(
500 RuntimeErrorStruct::new_with_msg_and_line_file(
501 "have fn by induc from: `>=` left must be the parameter name".to_string(),
502 line_file,
503 ),
504 )));
505 }
506 }
507 if ge.right.to_string() != induc_from.to_string() {
508 return Err(RuntimeError::from(ParseRuntimeError(
509 RuntimeErrorStruct::new_with_msg_and_line_file(
510 "have fn by induc from: `>=` right must match the object after `from`"
511 .to_string(),
512 line_file,
513 ),
514 )));
515 }
516 Ok(())
517 }
518
519 fn verify_have_fn_by_induc_special_case_slot_label(
521 slot: &Obj,
522 expected_index: usize,
523 line_file: LineFile,
524 ) -> Result<(), RuntimeError> {
525 match slot {
526 Obj::Number(n) => {
527 if n.normalized_value == expected_index.to_string() {
528 Ok(())
529 } else {
530 Err(
531 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
532 "have fn by induc from: special case label must be `{}` (0-based index for this row), got {}",
533 expected_index, n.normalized_value
534 ), line_file))))
535 }
536 }
537 _ => Err(
538 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: special case must be `case <natural>: <obj>` where <natural> is the 0-based index (0, 1, …)"
539 .to_string(), line_file)))),
540 }
541 }
542
543 pub fn parse_have_exist(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
544 tb.skip_token(HAVE)?;
545 tb.skip_token(BY)?;
546
547 let true_fact = self.parse_exist_fact(tb)?;
548
549 tb.skip_token(COLON)?;
550
551 let mut equal_tos = vec![];
552 while !tb.exceed_end_of_head() {
553 equal_tos.push(tb.advance()?);
554 if tb.current_token_is_equal_to(COMMA) {
555 tb.skip_token(COMMA)?;
556 }
557 }
558
559 self.register_collected_param_names_for_def_parse(&equal_tos, tb.line_file.clone())?;
560
561 Ok(HaveByExistStmt::new(equal_tos, true_fact, tb.line_file.clone()).into())
562 }
563
564 fn parse_braced_params_and_optional_dom_facts(
567 &mut self,
568 tb: &mut TokenBlock,
569 ) -> Result<(ParamDefWithType, Vec<OrAndChainAtomicFact>), RuntimeError> {
570 tb.skip_token(LEFT_BRACE)?;
571 let params_def_with_type =
572 self.parse_def_param_type_groups_until_colon_or_right_brace(tb)?;
573 let scope_names = params_def_with_type.collect_param_names();
574 let dom_facts = if tb.current_token_is_equal_to(COLON) {
575 tb.skip_token(COLON)?;
576 let mut facts = vec![];
577 let dom_result = loop {
578 if tb.current()? == RIGHT_BRACE {
579 break Ok(facts);
580 }
581 match self.parse_or_and_chain_atomic_fact(tb) {
582 Ok(f) => facts.push(f),
583 Err(e) => {
584 self.parsing_free_param_collection
585 .end_scope(ParamObjType::DefHeader, &scope_names);
586 break Err(e);
587 }
588 }
589 if tb.current_token_is_equal_to(COMMA) {
590 tb.skip_token(COMMA)?;
591 }
592 };
593 dom_result?
594 } else {
595 vec![]
596 };
597 if let Err(e) = tb.skip_token(RIGHT_BRACE) {
598 self.parsing_free_param_collection
599 .end_scope(ParamObjType::DefHeader, &scope_names);
600 return Err(e);
601 }
602 Ok((params_def_with_type, dom_facts))
603 }
604
605 pub fn parse_def_family_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
606 tb.skip_token(FAMILY)?;
607 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
608
609 self.run_in_local_parsing_time_name_scope(move |this| {
610 let (params_def_with_type, dom_facts) =
611 this.parse_braced_params_and_optional_dom_facts(tb)?;
612 let family_def_scope_names = params_def_with_type.collect_param_names();
613 let stmt_result = (|| -> Result<Stmt, RuntimeError> {
614 if !tb.current_token_is_equal_to(EQUAL) {
615 return Err(RuntimeError::from(ParseRuntimeError(
616 RuntimeErrorStruct::new_with_msg_and_line_file(
617 "family definition expects `=` after `}`".to_string(),
618 tb.line_file.clone(),
619 ),
620 )));
621 }
622 tb.skip_token(EQUAL)?;
623 let equal_to = this.parse_obj(tb)?;
624 Ok(DefFamilyStmt::new(
625 name,
626 params_def_with_type,
627 dom_facts,
628 equal_to,
629 tb.line_file.clone(),
630 )
631 .into())
632 })();
633 this.parsing_free_param_collection
634 .end_scope(ParamObjType::DefHeader, &family_def_scope_names);
635 stmt_result
636 })
637 }
638
639 pub fn parse_def_algorithm_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
640 tb.skip_token(ALGO)?;
641 let name = tb.advance()?;
642 self.run_in_local_parsing_time_name_scope(move |this| {
643 tb.skip_token(LEFT_BRACE)?;
644 let mut params: Vec<String> = vec![];
645 while tb.current()? != RIGHT_BRACE {
646 params.push(tb.advance()?);
647 if tb.current_token_is_equal_to(COMMA) {
648 tb.skip_token(COMMA)?;
649 }
650 }
651 tb.skip_token(RIGHT_BRACE)?;
652 this.register_collected_param_names_for_def_parse(¶ms, tb.line_file.clone())?;
653 tb.skip_token(COLON)?;
654 this.parsing_free_param_collection.begin_scope(
655 ParamObjType::DefAlgo,
656 ¶ms,
657 tb.line_file.clone(),
658 )?;
659 let params_for_end = params.clone();
660 let algo_result = (|| -> Result<DefAlgoStmt, RuntimeError> {
661 let mut algo_cases: Vec<AlgoCase> = vec![];
662 let mut default_return: Option<AlgoReturn> = None;
663 match tb.body.split_last_mut() {
664 None => {}
665 Some((last_block, leading_blocks)) => {
666 for block in leading_blocks.iter_mut() {
667 algo_cases.push(this.parse_algo_case(block)?);
668 }
669 if last_block.current_token_empty_if_exceed_end_of_head() == CASE {
670 algo_cases.push(this.parse_algo_case(last_block)?);
671 } else {
672 default_return = Some(this.parse_algo_return(last_block)?);
673 }
674 }
675 }
676 Ok(DefAlgoStmt::new(
677 name,
678 params,
679 algo_cases,
680 default_return,
681 tb.line_file.clone(),
682 ))
683 })();
684 this.parsing_free_param_collection
685 .end_scope(ParamObjType::DefAlgo, ¶ms_for_end);
686 Ok(algo_result?.into())
687 })
688 }
689
690 fn parse_algo_case(&mut self, block: &mut TokenBlock) -> Result<AlgoCase, RuntimeError> {
692 block.skip_token(CASE)?;
693 let condition = self.parse_atomic_fact(block, true)?;
694 block.skip_token(COLON)?;
695
696 let return_stmt = self.parse_algo_return(block)?;
697 Ok(AlgoCase::new(
698 condition,
699 return_stmt,
700 block.line_file.clone(),
701 ))
702 }
703
704 fn parse_algo_return(&mut self, block: &mut TokenBlock) -> Result<AlgoReturn, RuntimeError> {
706 let value = self.parse_obj(block)?;
707 Ok(AlgoReturn::new(value, block.line_file.clone()))
708 }
709}
710
711impl Runtime {
712 pub fn register_collected_param_names_for_def_parse(
713 &mut self,
714 names: &Vec<String>,
715 line_file: LineFile,
716 ) -> Result<(), RuntimeError> {
717 self.validate_names_and_insert_into_top_parsing_time_name_scope(names, line_file.clone())
718 .map_err(|e| {
719 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
720 None,
721 String::new(),
722 line_file,
723 Some(e),
724 vec![],
725 )))
726 })
727 }
728
729 fn parse_def_braced_param_groups_with_param_type(
731 &mut self,
732 tb: &mut TokenBlock,
733 ) -> Result<ParamDefWithType, RuntimeError> {
734 tb.skip_token(LEFT_BRACE)?;
735 let mut groups = Vec::new();
736 while tb.current()? != RIGHT_BRACE {
737 groups.push(
738 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
739 );
740 }
741 tb.skip_token(RIGHT_BRACE)?;
742 let param_defs = ParamDefWithType::new(groups);
743 let names = param_defs.collect_param_names();
744 self.register_collected_param_names_for_def_parse(&names, tb.line_file.clone())?;
745 Ok(param_defs)
746 }
747
748 fn parse_def_param_type_groups_until_colon_or_right_brace(
750 &mut self,
751 tb: &mut TokenBlock,
752 ) -> Result<ParamDefWithType, RuntimeError> {
753 let mut groups = vec![];
754 while tb.current()? != COLON && tb.current()? != RIGHT_BRACE {
755 groups.push(
756 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
757 );
758 }
759 let params_def_with_type = ParamDefWithType::new(groups);
760 let param_names = params_def_with_type.collect_param_names();
761 self.register_collected_param_names_for_def_parse(¶m_names, tb.line_file.clone())?;
762 Ok(params_def_with_type)
763 }
764
765 pub fn insert_parsed_name_into_top_parsing_time_name_scope(
766 &mut self,
767 name: &str,
768 line_file: LineFile,
769 ) -> Result<(), RuntimeError> {
770 self.validate_name_and_insert_into_top_parsing_time_name_scope(name, line_file.clone())
771 .map_err(|e| {
772 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
773 None,
774 String::new(),
775 line_file,
776 Some(e),
777 vec![],
778 )))
779 })
780 }
781
782 pub fn parse_name_and_insert_into_top_parsing_time_name_scope(
783 &mut self,
784 tb: &mut TokenBlock,
785 ) -> Result<String, RuntimeError> {
786 let name = tb.advance()?;
787 self.insert_parsed_name_into_top_parsing_time_name_scope(&name, tb.line_file.clone())?;
788 Ok(name)
789 }
790}