1use crate::prelude::*;
2use crate::verify::number_is_in_z;
3
4impl Runtime {
5 pub fn parse_def_struct_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
6 tb.skip_token(STRUCT)?;
7 let name = tb.advance()?;
8 is_valid_litex_name(&name).map_err(|msg| {
9 RuntimeError::from(ParseRuntimeError(
10 RuntimeErrorStruct::new_with_msg_and_line_file(msg, tb.line_file.clone()),
11 ))
12 })?;
13
14 let stmt_result = self.run_in_local_parsing_time_name_scope(|this| {
15 let param_def_with_dom = if tb.current_token_is_equal_to(LEFT_BRACE) {
16 let param_def = this.parse_def_braced_param_groups_with_param_type(tb)?;
17 Some((param_def, Vec::new()))
18 } else {
19 None
20 };
21 let struct_param_names = param_def_with_dom
22 .as_ref()
23 .map(|(param_def, _)| param_def.collect_param_names())
24 .unwrap_or_else(Vec::new);
25
26 let parse_result = (|| -> Result<DefStructStmt, RuntimeError> {
27 tb.skip_token(COLON)?;
28 if tb.body.is_empty() {
29 return Err(RuntimeError::from(ParseRuntimeError(
30 RuntimeErrorStruct::new_with_msg_and_line_file(
31 "struct definition expects at least two fields".to_string(),
32 tb.line_file.clone(),
33 ),
34 )));
35 }
36
37 let mut fields: Vec<(String, Obj)> = Vec::new();
38 let mut equivalent_facts: Vec<Fact> = Vec::new();
39 let mut seen_equivalent = false;
40
41 for block in tb.body.iter_mut() {
42 if block.current()? == EQUIVALENT_SIGN {
43 if seen_equivalent {
44 return Err(RuntimeError::from(ParseRuntimeError(
45 RuntimeErrorStruct::new_with_msg_and_line_file(
46 "struct definition can only have one `<=>:` block".to_string(),
47 block.line_file.clone(),
48 ),
49 )));
50 }
51 seen_equivalent = true;
52 equivalent_facts = this.parse_struct_equivalent_facts(block, &fields)?;
53 } else {
54 if seen_equivalent {
55 return Err(RuntimeError::from(ParseRuntimeError(
56 RuntimeErrorStruct::new_with_msg_and_line_file(
57 "struct fields must appear before `<=>:`".to_string(),
58 block.line_file.clone(),
59 ),
60 )));
61 }
62 let field = this.parse_struct_field(block)?;
63 if fields.iter().any(|(name, _)| name == &field.0) {
64 return Err(RuntimeError::from(ParseRuntimeError(
65 RuntimeErrorStruct::new_with_msg_and_line_file(
66 format!("duplicate struct field `{}`", field.0),
67 block.line_file.clone(),
68 ),
69 )));
70 }
71 fields.push(field);
72 }
73 }
74
75 if fields.len() < 2 {
76 return Err(RuntimeError::from(ParseRuntimeError(
77 RuntimeErrorStruct::new_with_msg_and_line_file(
78 "struct definition expects at least two fields".to_string(),
79 tb.line_file.clone(),
80 ),
81 )));
82 }
83
84 Ok(DefStructStmt::new(
85 name.clone(),
86 param_def_with_dom,
87 fields,
88 equivalent_facts,
89 tb.line_file.clone(),
90 ))
91 })();
92
93 if !struct_param_names.is_empty() {
94 this.parsing_free_param_collection
95 .end_scope(ParamObjType::DefHeader, &struct_param_names);
96 }
97 parse_result
98 });
99
100 let stmt = stmt_result?;
101 self.insert_parsed_name_into_top_parsing_time_name_scope(&stmt.name, tb.line_file.clone())?;
102 Ok(stmt.into())
103 }
104
105 fn parse_struct_field(
106 &mut self,
107 block: &mut TokenBlock,
108 ) -> Result<(String, Obj), RuntimeError> {
109 if !block.body.is_empty() {
110 return Err(RuntimeError::from(ParseRuntimeError(
111 RuntimeErrorStruct::new_with_msg_and_line_file(
112 "struct field must fit on one line".to_string(),
113 block.line_file.clone(),
114 ),
115 )));
116 }
117
118 let field_name = block.advance()?;
119 is_valid_litex_name(&field_name).map_err(|msg| {
120 RuntimeError::from(ParseRuntimeError(
121 RuntimeErrorStruct::new_with_msg_and_line_file(msg, block.line_file.clone()),
122 ))
123 })?;
124
125 let field_type = self.parse_obj(block)?;
126 if !block.exceed_end_of_head() {
127 return Err(RuntimeError::from(ParseRuntimeError(
128 RuntimeErrorStruct::new_with_msg_and_line_file(
129 "unexpected token after struct field type".to_string(),
130 block.line_file.clone(),
131 ),
132 )));
133 }
134 Ok((field_name, field_type))
135 }
136
137 fn parse_struct_equivalent_facts(
138 &mut self,
139 block: &mut TokenBlock,
140 fields: &Vec<(String, Obj)>,
141 ) -> Result<Vec<Fact>, RuntimeError> {
142 block.skip_token(EQUIVALENT_SIGN)?;
143 block.skip_token(COLON)?;
144 if !block.exceed_end_of_head() {
145 return Err(RuntimeError::from(ParseRuntimeError(
146 RuntimeErrorStruct::new_with_msg_and_line_file(
147 "`<=>:` in struct definition must not have inline facts".to_string(),
148 block.line_file.clone(),
149 ),
150 )));
151 }
152 let field_names = fields
153 .iter()
154 .map(|(name, _)| name.clone())
155 .collect::<Vec<_>>();
156 self.parsing_free_param_collection.begin_scope(
157 ParamObjType::DefStructField,
158 &field_names,
159 block.line_file.clone(),
160 )?;
161 let facts_result = self.parse_facts_in_body(block);
162 self.parsing_free_param_collection
163 .end_scope(ParamObjType::DefStructField, &field_names);
164 facts_result
165 }
166
167 pub fn parse_def_prop_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
168 let stmt = self.run_in_local_parsing_time_name_scope(|this| {
169 tb.skip_token(PROP)?;
170 let name = this.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
171 let param_defs = this.parse_def_braced_param_groups_with_param_type(tb)?;
172 let def_param_names = param_defs.collect_param_names();
173
174 if tb.current_token_is_equal_to(COLON) {
175 tb.skip_token(COLON)?;
176 } else {
177 if !tb.exceed_end_of_head() {
178 return Err(RuntimeError::from(ParseRuntimeError(
179 RuntimeErrorStruct::new_with_msg_and_line_file(
180 "expect `:` or end of line after `)` in prop statement".to_string(),
181 tb.line_file.clone(),
182 ),
183 )));
184 } else {
185 this.parsing_free_param_collection
186 .end_scope(ParamObjType::DefHeader, &def_param_names);
187 return Ok(DefPropStmt::new(
188 name,
189 param_defs,
190 vec![],
191 tb.line_file.clone(),
192 ));
193 }
194 }
195
196 let facts_result = this.parse_facts_in_body(tb);
197 this.parsing_free_param_collection
198 .end_scope(ParamObjType::DefHeader, &def_param_names);
199 let facts = facts_result?;
200 Ok(DefPropStmt::new(
201 name,
202 param_defs,
203 facts,
204 tb.line_file.clone(),
205 ))
206 });
207
208 let stmt_ok = stmt?;
209 self.insert_parsed_name_into_top_parsing_time_name_scope(
210 &stmt_ok.name,
211 tb.line_file.clone(),
212 )?;
213
214 Ok(stmt_ok.into())
215 }
216
217 pub fn parse_def_abstract_prop_stmt(
218 &mut self,
219 tb: &mut TokenBlock,
220 ) -> Result<Stmt, RuntimeError> {
221 let stmt: Result<DefAbstractPropStmt, RuntimeError> = self
222 .run_in_local_parsing_time_name_scope(|this| {
223 tb.skip_token(ABSTRACT_PROP)?;
224 let name = this.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
225 tb.skip_token(LEFT_BRACE)?;
226 let mut params = vec![];
227 while tb.current()? != RIGHT_BRACE {
228 params.push(tb.advance()?);
229 if !tb.current_token_is_equal_to(RIGHT_BRACE) {
230 tb.skip_token(COMMA)?;
231 }
232 }
233 tb.skip_token(RIGHT_BRACE)?;
234
235 this.register_collected_param_names_for_def_parse(¶ms, tb.line_file.clone())?;
236
237 Ok(DefAbstractPropStmt::new(name, params, tb.line_file.clone()))
238 });
239
240 let stmt_ok = stmt?;
241 self.insert_parsed_name_into_top_parsing_time_name_scope(
242 &stmt_ok.name,
243 tb.line_file.clone(),
244 )?;
245 Ok(stmt_ok.into())
246 }
247
248 pub fn parse_def_let_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
249 tb.skip_token(LET)?;
250 let mut param_def: Vec<ParamGroupWithParamType> = vec![];
251 loop {
252 match tb.current() {
253 Ok(t) if t == COLON => break,
254 Err(_) => break,
255 Ok(_) => {}
256 }
257 param_def.push(
258 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Identifier)?,
259 );
260 }
261 let param_def = ParamDefWithType::new(param_def);
262 let all_param_names = param_def.collect_param_names();
263 self.register_collected_param_names_for_def_parse(&all_param_names, tb.line_file.clone())?;
264
265 let facts = if tb.current_token_is_equal_to(COLON) {
266 tb.skip_token(COLON)?;
267
268 let facts_result: Result<Vec<Fact>, RuntimeError> = if tb.exceed_end_of_head() {
269 self.parse_facts_in_body(tb)
270 } else {
271 let mut facts = Vec::new();
272 let parse_result = (|| {
273 loop {
274 facts.push(self.parse_fact(tb)?);
275 if tb.exceed_end_of_head() {
276 break;
277 }
278 tb.skip_token(COMMA)?;
279 if tb.exceed_end_of_head() {
280 return Err(RuntimeError::from(ParseRuntimeError(
281 RuntimeErrorStruct::new_with_msg_and_line_file(
282 "expected fact after comma in inline let statement".to_string(),
283 tb.line_file.clone(),
284 ),
285 )));
286 }
287 }
288 if !tb.body.is_empty() {
289 return Err(RuntimeError::from(ParseRuntimeError(
290 RuntimeErrorStruct::new_with_msg_and_line_file(
291 "inline let statement cannot also have an indented body"
292 .to_string(),
293 tb.line_file.clone(),
294 ),
295 )));
296 }
297 Ok(())
298 })();
299 parse_result.map(|_| facts)
300 };
301 if facts_result.is_err() && !all_param_names.is_empty() {
302 self.parsing_free_param_collection
303 .end_scope(ParamObjType::Identifier, &all_param_names);
304 }
305 let facts = facts_result?;
306 self.parsing_free_param_collection
307 .end_scope(ParamObjType::Identifier, &all_param_names);
308 facts
309 } else {
310 if !all_param_names.is_empty() {
311 self.parsing_free_param_collection
312 .end_scope(ParamObjType::Identifier, &all_param_names);
313 }
314 vec![]
315 };
316 Ok(DefLetStmt::new(param_def, facts, tb.line_file.clone()).into())
317 }
318
319 pub fn parse_have_obj_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
321 tb.skip_token(HAVE)?;
322 let mut param_defs: Vec<ParamGroupWithParamType> = vec![];
323 loop {
324 param_defs.push(
325 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Identifier)?,
326 );
327 match tb.current() {
328 Ok(t) if t == EQUAL => break,
329 Err(_) => break,
330 Ok(_) => {}
331 }
332 }
333 if param_defs.is_empty() {
334 return Err(RuntimeError::from(ParseRuntimeError(
335 RuntimeErrorStruct::new_with_msg_and_line_file(
336 "have expects at least one param type pair".to_string(),
337 tb.line_file.clone(),
338 ),
339 )));
340 }
341 let param_defs = ParamDefWithType::new(param_defs);
342 let have_param_names = param_defs.collect_param_names();
343 self.register_collected_param_names_for_def_parse(&have_param_names, tb.line_file.clone())?;
344
345 if tb.current().map(|t| t != EQUAL).unwrap_or(true) {
346 if !have_param_names.is_empty() {
347 self.parsing_free_param_collection
348 .end_scope(ParamObjType::Identifier, &have_param_names);
349 }
350 Ok(HaveObjInNonemptySetOrParamTypeStmt::new(param_defs, tb.line_file.clone()).into())
351 } else {
352 tb.skip_token(EQUAL)?;
353 let objs_result = (|| -> Result<Vec<Obj>, RuntimeError> {
354 let mut objs_equal_to = vec![self.parse_obj(tb)?];
355 while matches!(tb.current(), Ok(t) if t == COMMA) {
356 tb.skip_token(COMMA)?;
357 objs_equal_to.push(self.parse_obj(tb)?);
358 }
359 Ok(objs_equal_to)
360 })();
361 self.parsing_free_param_collection
362 .end_scope(ParamObjType::Identifier, &have_param_names);
363 let objs_equal_to = objs_result?;
364 Ok(HaveObjEqualStmt::new(param_defs, objs_equal_to, tb.line_file.clone()).into())
365 }
366 }
367
368 pub fn parse_have_fn_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
369 tb.skip_token(HAVE)?;
370 tb.skip_token(FN_LOWER_CASE)?;
371 if tb.current_token_is_equal_to(BY) {
372 tb.skip_token(BY)?;
373 self.parse_have_fn_by_induc_stmt(tb)
374 } else {
375 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
376 if tb.current_token_is_equal_to(BY) {
377 tb.skip_token(BY)?;
378 let lf = tb.line_file.clone();
379 let fact = self.parse_fact(tb)?;
380 let forall = match fact {
381 Fact::ForallFact(ff) => ff,
382 _ => {
383 return Err(RuntimeError::from(ParseRuntimeError(
384 RuntimeErrorStruct::new_with_msg_and_line_file(
385 "have fn <name> by ... expects a `forall` fact".to_string(),
386 lf,
387 ),
388 )));
389 }
390 };
391 if !tb.exceed_end_of_head() {
392 return Err(RuntimeError::from(ParseRuntimeError(
393 RuntimeErrorStruct::new_with_msg_and_line_file(
394 "unexpected token after `have fn` `by` `forall` fact".to_string(),
395 tb.line_file.clone(),
396 ),
397 )));
398 }
399 return Ok(HaveFnByForallExistUniqueStmt::new(name, forall, lf).into());
400 }
401
402 let fs = self.parse_fn_set_clause(tb)?;
403 let fn_param_names = fs.collect_all_param_names_including_nested_ret_fn_sets();
404
405 if tb.current_token_is_equal_to(COLON) {
406 tb.skip_token(COLON)?;
407 let case_block_count = tb.body.len();
408 let mut cases: Vec<AndChainAtomicFact> = Vec::with_capacity(case_block_count);
409 let mut equal_tos: Vec<Obj> = Vec::with_capacity(case_block_count);
410 for block in tb.body.iter_mut() {
411 block.skip_token(CASE)?;
412 let case_lf = block.line_file.clone();
413 cases.push(self.with_optional_free_param_scope(
414 ParamObjType::FnSet,
415 &fn_param_names,
416 case_lf,
417 |this| this.parse_and_chain_atomic_fact(block),
418 )?);
419 block.skip_token(COLON)?;
420 let rhs_lf = block.line_file.clone();
421 equal_tos.push(self.with_optional_free_param_scope(
422 ParamObjType::FnSet,
423 &fn_param_names,
424 rhs_lf,
425 |this| this.parse_obj(block),
426 )?);
427 }
428 Ok(
429 HaveFnEqualCaseByCaseStmt::new(
430 name,
431 fs,
432 cases,
433 equal_tos,
434 tb.line_file.clone(),
435 )
436 .into(),
437 )
438 } else {
439 tb.skip_token(EQUAL)?;
440
441 let lf = tb.line_file.clone();
442 let equal_to = self.with_optional_free_param_scope(
443 ParamObjType::FnSet,
444 &fn_param_names,
445 lf,
446 |this| this.parse_obj(tb),
447 )?;
448 let equal_to_anonymous_fn = AnonymousFn::new(
449 fs.params_def_with_set.clone(),
450 fs.dom_facts.clone(),
451 fs.ret_set.clone(),
452 equal_to,
453 )?;
454 Ok(HaveFnEqualStmt::new(name, equal_to_anonymous_fn, tb.line_file.clone()).into())
455 }
456 }
457 }
458
459 fn parse_have_fn_by_induc_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
463 tb.skip_token(INDUC)?;
464 tb.skip_token(FROM)?;
465 let induc_from = self.parse_obj(tb)?;
466 tb.skip_token(COLON)?;
467 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
468
469 tb.skip_token(LEFT_BRACE)?;
470 let param = tb.advance()?;
471 if !tb.current_token_is_equal_to(Z) {
472 return Err(RuntimeError::from(ParseRuntimeError(
473 RuntimeErrorStruct::new_with_msg_and_line_file(
474 "have fn by induc from: expected `Z` after parameter name".to_string(),
475 tb.line_file.clone(),
476 ),
477 )));
478 }
479 tb.skip_token(Z)?;
480 tb.skip_token(COLON)?;
481
482 self.run_in_local_parsing_time_name_scope(|this| {
483 this.parse_have_fn_by_induc_stmt_after_param_scope(tb, name, param, induc_from)
484 })
485 }
486
487 fn parse_have_fn_by_induc_stmt_after_param_scope(
488 &mut self,
489 tb: &mut TokenBlock,
490 name: String,
491 param: String,
492 induc_from: Obj,
493 ) -> Result<Stmt, RuntimeError> {
494 self.validate_user_fn_param_names_for_parse(&[param.clone()], tb.line_file.clone())?;
495 let dom_and_chain = self.parse_and_chain_atomic_fact(tb)?;
496 Self::verify_have_fn_by_induc_dom_matches_induc_from(
497 &dom_and_chain,
498 ¶m,
499 &induc_from,
500 tb.line_file.clone(),
501 )?;
502 tb.skip_token(RIGHT_BRACE)?;
503 let ret_set = self.parse_obj(tb)?;
504
505 if !tb.current_token_is_equal_to(COLON) {
506 return Err(RuntimeError::from(ParseRuntimeError(
507 RuntimeErrorStruct::new_with_msg_and_line_file(
508 "have fn by induc from: expected `:` before case blocks".to_string(),
509 tb.line_file.clone(),
510 ),
511 )));
512 }
513 tb.skip_token(COLON)?;
514
515 let num_blocks = tb.body.len();
516 if num_blocks <= 1 {
517 return Err(RuntimeError::from(ParseRuntimeError(
518 RuntimeErrorStruct::new_with_msg_and_line_file(
519 "have fn by induc from: expected at least two case blocks".to_string(),
520 tb.line_file.clone(),
521 ),
522 )));
523 }
524
525 let num_special = num_blocks - 1;
526 let mut special_cases_equal_tos: Vec<Obj> = Vec::with_capacity(num_special);
527
528 let induc_from_is_number_obj = matches!(induc_from, Obj::Number(_));
529 if induc_from_is_number_obj {
530 if let Obj::Number(n) = &induc_from {
531 if !number_is_in_z(n) {
532 return Err(
533 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
534 "have fn by induc from: when `from` is a number literal, it must be an integer, got {}",
535 induc_from.to_string()
536 ), tb.line_file.clone()))));
537 }
538 }
539 }
540
541 for i in 0..num_special {
542 let block = &mut tb.body[i];
543 block.skip_token(CASE)?;
544
545 block.skip_token(¶m)?;
546
547 block.skip_token(EQUAL)?;
548
549 let slot_label = self.parse_obj(block)?;
550 Self::verify_have_fn_by_induc_special_case_slot_label(
551 &slot_label,
552 i,
553 block.line_file.clone(),
554 )?;
555
556 if induc_from_is_number_obj {
557 let induc_from_add_i: Obj = Add::new(
558 induc_from.clone(),
559 Into::<Obj>::into(Number::new(i.to_string())),
560 )
561 .into();
562
563 if !induc_from_add_i
564 .two_objs_can_be_calculated_and_equal_by_calculation(&slot_label)
565 {
566 return Err(
567 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
568 "have fn by induc from: when `from` is a number literal, special case must be `case {} = {}:` (`from` + {}), got {}",
569 param, induc_from_add_i.to_string(), i, slot_label.to_string()
570 ), block.line_file.clone()))));
571 }
572 } else {
573 let induc_from_add_i: Obj = Add::new(
574 induc_from.clone(),
575 Into::<Obj>::into(Number::new(i.to_string())),
576 )
577 .into();
578
579 if induc_from_add_i.to_string() != slot_label.to_string() {
580 return Err(
581 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
582 "have fn by induc from: when `from` is not a number literal, special case must be `case {} = {}:`, got {}",
583 param, induc_from_add_i.to_string(), slot_label.to_string()
584 ), block.line_file.clone()))));
585 }
586 }
587
588 block.skip_token(COLON)?;
589 if !block.exceed_end_of_head() {
590 special_cases_equal_tos.push(self.parse_obj(block)?);
591 } else {
592 return Err(
593 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"
594 .to_string(), block.line_file.clone()))));
595 }
596 }
597
598 let induc_names_last = [param.clone()];
599 let last_case_line = tb.body[num_blocks - 1].line_file.clone();
600 let last_case = self.parse_in_local_free_param_scope(
601 ParamObjType::Induc,
602 &induc_names_last,
603 last_case_line,
604 |this| {
605 let last_block = &mut tb.body[num_blocks - 1];
606 last_block.skip_token(CASE)?;
607 last_block.skip_token(¶m)?;
608 last_block.skip_token(GREATER_EQUAL)?;
609 let last_bound = this.parse_obj(last_block)?;
610
611 if induc_from_is_number_obj {
612 let induc_from_add_n: Obj = Add::new(
613 induc_from.clone(),
614 Into::<Obj>::into(Number::new(num_special.to_string())),
615 )
616 .into();
617 if !induc_from_add_n
618 .two_objs_can_be_calculated_and_equal_by_calculation(&last_bound)
619 {
620 return Err(
621 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
622 "have fn by induc from: when `from` is a number literal, last case must be `case >= {}:` (`from` + {}), got {}",
623 induc_from_add_n.to_string(), num_special, last_bound.to_string()
624 ), last_block.line_file.clone()))));
625 }
626 } else {
627 let induc_from_add_n: Obj = Add::new(
628 induc_from.clone(),
629 Into::<Obj>::into(Number::new(num_special.to_string())),
630 )
631 .into();
632 if induc_from_add_n.to_string() != last_bound.to_string() {
633 return Err(
634 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
635 "have fn by induc from: when `from` is not a number literal, last case must be `case >= {}:`, got {}",
636 induc_from_add_n.to_string(), last_bound.to_string()
637 ), last_block.line_file.clone()))));
638 }
639 }
640
641 last_block.skip_token(COLON)?;
642
643 if !last_block.exceed_end_of_head() {
644 let last_obj = this.parse_obj(last_block)?;
645 if !last_block.exceed_end_of_head() {
646 return Err(
647 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: unexpected tokens after `obj` in last case"
648 .to_string(), last_block.line_file.clone()))));
649 }
650 if !last_block.body.is_empty() {
651 return Err(
652 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"
653 .to_string(), last_block.line_file.clone()))));
654 }
655 Ok(HaveFnByInducLastCase::EqualTo(last_obj))
656 } else if !last_block.body.is_empty() {
657 let mut nested: Vec<HaveFnByInducNestedCase> =
658 Vec::with_capacity(last_block.body.len());
659 for sub in last_block.body.iter_mut() {
660 sub.skip_token(CASE)?;
661 let w = this.parse_and_chain_atomic_fact(sub)?;
662 sub.skip_token(COLON)?;
663 if sub.exceed_end_of_head() {
664 return Err(
665 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must be `case <when>: <obj>`"
666 .to_string(), sub.line_file.clone()))));
667 }
668 let o = this.parse_obj(sub)?;
669 if !sub.body.is_empty() {
670 return Err(
671 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must not have further indentation"
672 .to_string(), sub.line_file.clone()))));
673 }
674 nested.push(HaveFnByInducNestedCase {
675 case_fact: w,
676 equal_to: o,
677 });
678 }
679 Ok(HaveFnByInducLastCase::NestedCases(nested))
680 } else {
681 Err(RuntimeError::from(ParseRuntimeError(
682 RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: last case must end with `: <obj>` or `:` with nested `case` blocks"
683 .to_string(), last_block.line_file.clone()),
684 )))
685 }
686 },
687 )?;
688
689 Ok(HaveFnByInducStmt::new(
690 name,
691 param,
692 ret_set,
693 induc_from,
694 special_cases_equal_tos,
695 last_case,
696 tb.line_file.clone(),
697 )
698 .into())
699 }
700
701 fn verify_have_fn_by_induc_dom_matches_induc_from(
702 when: &AndChainAtomicFact,
703 param_name: &str,
704 induc_from: &Obj,
705 line_file: LineFile,
706 ) -> Result<(), RuntimeError> {
707 let ge = match when {
708 AndChainAtomicFact::AtomicFact(AtomicFact::GreaterEqualFact(ge)) => ge,
709 _ => {
710 return Err(RuntimeError::from(ParseRuntimeError(
711 RuntimeErrorStruct::new_with_msg_and_line_file(
712 "have fn by induc from: dom fact must be a single `>=` fact".to_string(),
713 line_file,
714 ),
715 )));
716 }
717 };
718 match &ge.left {
719 Obj::Atom(AtomObj::Identifier(id)) if id.name == param_name => {}
720 _ => {
721 return Err(RuntimeError::from(ParseRuntimeError(
722 RuntimeErrorStruct::new_with_msg_and_line_file(
723 "have fn by induc from: `>=` left must be the parameter name".to_string(),
724 line_file,
725 ),
726 )));
727 }
728 }
729 if ge.right.to_string() != induc_from.to_string() {
730 return Err(RuntimeError::from(ParseRuntimeError(
731 RuntimeErrorStruct::new_with_msg_and_line_file(
732 "have fn by induc from: `>=` right must match the object after `from`"
733 .to_string(),
734 line_file,
735 ),
736 )));
737 }
738 Ok(())
739 }
740
741 fn verify_have_fn_by_induc_special_case_slot_label(
743 slot: &Obj,
744 expected_index: usize,
745 line_file: LineFile,
746 ) -> Result<(), RuntimeError> {
747 match slot {
748 Obj::Number(n) => {
749 if n.normalized_value == expected_index.to_string() {
750 Ok(())
751 } else {
752 Err(
753 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
754 "have fn by induc from: special case label must be `{}` (0-based index for this row), got {}",
755 expected_index, n.normalized_value
756 ), line_file))))
757 }
758 }
759 _ => Err(
760 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, …)"
761 .to_string(), line_file)))),
762 }
763 }
764
765 pub fn parse_have_exist(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
766 tb.skip_token(HAVE)?;
767 tb.skip_token(BY)?;
768
769 let true_fact = self.parse_exist_fact(tb)?;
770
771 tb.skip_token(COLON)?;
772
773 let mut equal_tos = vec![];
774 while !tb.exceed_end_of_head() {
775 equal_tos.push(tb.advance()?);
776 if tb.current_token_is_equal_to(COMMA) {
777 tb.skip_token(COMMA)?;
778 }
779 }
780
781 self.register_collected_param_names_for_def_parse(&equal_tos, tb.line_file.clone())?;
782
783 Ok(HaveByExistStmt::new(equal_tos, true_fact, tb.line_file.clone()).into())
784 }
785
786 fn parse_braced_params_and_optional_dom_facts(
789 &mut self,
790 tb: &mut TokenBlock,
791 ) -> Result<(ParamDefWithType, Vec<OrAndChainAtomicFact>), RuntimeError> {
792 tb.skip_token(LEFT_BRACE)?;
793 let params_def_with_type =
794 self.parse_def_param_type_groups_until_colon_or_right_brace(tb)?;
795 let scope_names = params_def_with_type.collect_param_names();
796 let dom_facts = if tb.current_token_is_equal_to(COLON) {
797 tb.skip_token(COLON)?;
798 let mut facts = vec![];
799 let dom_result = loop {
800 if tb.current()? == RIGHT_BRACE {
801 break Ok(facts);
802 }
803 match self.parse_or_and_chain_atomic_fact(tb) {
804 Ok(f) => facts.push(f),
805 Err(e) => {
806 self.parsing_free_param_collection
807 .end_scope(ParamObjType::DefHeader, &scope_names);
808 break Err(e);
809 }
810 }
811 if tb.current_token_is_equal_to(COMMA) {
812 tb.skip_token(COMMA)?;
813 }
814 };
815 dom_result?
816 } else {
817 vec![]
818 };
819 if let Err(e) = tb.skip_token(RIGHT_BRACE) {
820 self.parsing_free_param_collection
821 .end_scope(ParamObjType::DefHeader, &scope_names);
822 return Err(e);
823 }
824 Ok((params_def_with_type, dom_facts))
825 }
826
827 pub fn parse_def_family_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
828 tb.skip_token(FAMILY)?;
829 let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
830
831 self.run_in_local_parsing_time_name_scope(move |this| {
832 let (params_def_with_type, dom_facts) =
833 this.parse_braced_params_and_optional_dom_facts(tb)?;
834 let family_def_scope_names = params_def_with_type.collect_param_names();
835 let stmt_result = (|| -> Result<Stmt, RuntimeError> {
836 if !tb.current_token_is_equal_to(EQUAL) {
837 return Err(RuntimeError::from(ParseRuntimeError(
838 RuntimeErrorStruct::new_with_msg_and_line_file(
839 "family definition expects `=` after `}`".to_string(),
840 tb.line_file.clone(),
841 ),
842 )));
843 }
844 tb.skip_token(EQUAL)?;
845 let equal_to = this.parse_obj(tb)?;
846 Ok(DefFamilyStmt::new(
847 name,
848 params_def_with_type,
849 dom_facts,
850 equal_to,
851 tb.line_file.clone(),
852 )
853 .into())
854 })();
855 this.parsing_free_param_collection
856 .end_scope(ParamObjType::DefHeader, &family_def_scope_names);
857 stmt_result
858 })
859 }
860
861 pub fn parse_def_algorithm_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
862 tb.skip_token(ALGO)?;
863 let name = tb.advance()?;
864 self.run_in_local_parsing_time_name_scope(move |this| {
865 tb.skip_token(LEFT_BRACE)?;
866 let mut params: Vec<String> = vec![];
867 while tb.current()? != RIGHT_BRACE {
868 params.push(tb.advance()?);
869 if tb.current_token_is_equal_to(COMMA) {
870 tb.skip_token(COMMA)?;
871 }
872 }
873 tb.skip_token(RIGHT_BRACE)?;
874 this.register_collected_param_names_for_def_parse(¶ms, tb.line_file.clone())?;
875 tb.skip_token(COLON)?;
876 this.parsing_free_param_collection.begin_scope(
877 ParamObjType::DefAlgo,
878 ¶ms,
879 tb.line_file.clone(),
880 )?;
881 let params_for_end = params.clone();
882 let algo_result = (|| -> Result<DefAlgoStmt, RuntimeError> {
883 let mut algo_cases: Vec<AlgoCase> = vec![];
884 let mut default_return: Option<AlgoReturn> = None;
885 match tb.body.split_last_mut() {
886 None => {}
887 Some((last_block, leading_blocks)) => {
888 for block in leading_blocks.iter_mut() {
889 algo_cases.push(this.parse_algo_case(block)?);
890 }
891 if last_block.current_token_empty_if_exceed_end_of_head() == CASE {
892 algo_cases.push(this.parse_algo_case(last_block)?);
893 } else {
894 default_return = Some(this.parse_algo_return(last_block)?);
895 }
896 }
897 }
898 Ok(DefAlgoStmt::new(
899 name,
900 params,
901 algo_cases,
902 default_return,
903 tb.line_file.clone(),
904 ))
905 })();
906 this.parsing_free_param_collection
907 .end_scope(ParamObjType::DefAlgo, ¶ms_for_end);
908 Ok(algo_result?.into())
909 })
910 }
911
912 fn parse_algo_case(&mut self, block: &mut TokenBlock) -> Result<AlgoCase, RuntimeError> {
914 block.skip_token(CASE)?;
915 let condition = self.parse_atomic_fact(block, true)?;
916 block.skip_token(COLON)?;
917
918 let return_stmt = self.parse_algo_return(block)?;
919 Ok(AlgoCase::new(
920 condition,
921 return_stmt,
922 block.line_file.clone(),
923 ))
924 }
925
926 fn parse_algo_return(&mut self, block: &mut TokenBlock) -> Result<AlgoReturn, RuntimeError> {
928 let value = self.parse_obj(block)?;
929 Ok(AlgoReturn::new(value, block.line_file.clone()))
930 }
931}
932
933impl Runtime {
934 pub fn register_collected_param_names_for_def_parse(
935 &mut self,
936 names: &Vec<String>,
937 line_file: LineFile,
938 ) -> Result<(), RuntimeError> {
939 self.validate_names_and_insert_into_top_parsing_time_name_scope(names, line_file.clone())
940 .map_err(|e| {
941 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
942 None,
943 String::new(),
944 line_file,
945 Some(e),
946 vec![],
947 )))
948 })
949 }
950
951 fn parse_def_braced_param_groups_with_param_type(
953 &mut self,
954 tb: &mut TokenBlock,
955 ) -> Result<ParamDefWithType, RuntimeError> {
956 tb.skip_token(LEFT_BRACE)?;
957 let mut groups = Vec::new();
958 while tb.current()? != RIGHT_BRACE {
959 groups.push(
960 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
961 );
962 }
963 tb.skip_token(RIGHT_BRACE)?;
964 let param_defs = ParamDefWithType::new(groups);
965 let names = param_defs.collect_param_names();
966 self.register_collected_param_names_for_def_parse(&names, tb.line_file.clone())?;
967 Ok(param_defs)
968 }
969
970 fn parse_def_param_type_groups_until_colon_or_right_brace(
972 &mut self,
973 tb: &mut TokenBlock,
974 ) -> Result<ParamDefWithType, RuntimeError> {
975 let mut groups = vec![];
976 while tb.current()? != COLON && tb.current()? != RIGHT_BRACE {
977 groups.push(
978 self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
979 );
980 }
981 let params_def_with_type = ParamDefWithType::new(groups);
982 let param_names = params_def_with_type.collect_param_names();
983 self.register_collected_param_names_for_def_parse(¶m_names, tb.line_file.clone())?;
984 Ok(params_def_with_type)
985 }
986
987 pub fn insert_parsed_name_into_top_parsing_time_name_scope(
988 &mut self,
989 name: &str,
990 line_file: LineFile,
991 ) -> Result<(), RuntimeError> {
992 self.validate_name_and_insert_into_top_parsing_time_name_scope(name, line_file.clone())
993 .map_err(|e| {
994 RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
995 None,
996 String::new(),
997 line_file,
998 Some(e),
999 vec![],
1000 )))
1001 })
1002 }
1003
1004 pub fn parse_name_and_insert_into_top_parsing_time_name_scope(
1005 &mut self,
1006 tb: &mut TokenBlock,
1007 ) -> Result<String, RuntimeError> {
1008 let name = tb.advance()?;
1009 self.insert_parsed_name_into_top_parsing_time_name_scope(&name, tb.line_file.clone())?;
1010 Ok(name)
1011 }
1012}