Skip to main content

litex/parse/
parse_def_stmt.rs

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(&params, 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    // return HaveObjInNonemptySetOrParamTypeStmt or HaveObjEqualStmt
129    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    /// `have fn by` 已消费;解析 `induc from <Obj>: <name> ( <param> Z: <param> >= <induc_from> ) <ret_set> : case ...`。
238    /// 前若干条特例为 `case <k>: obj`,其中 `<k>` 为 **0 起下标占位符**,须与该行顺序一致(第 1 条为 0,第 2 条为 1,…);
239    /// 最后一条须为 `case >= n:`,其中 **n 为特例个数**(数字字面量);且要么行末 `: obj`,要么 `:` 后换行跟子块 `case when: obj`。
240    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            &param,
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(&param)?;
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(&param)?;
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    /// 特例行 `case <k>:`:`<k>` 须为自然数字面量,且等于该行在特例中的 **0-based 顺序**(第 1 条为 0,第 2 条为 1,…)。
520    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    /// Parses `{ params [: dom_facts] }` for `family`. Leaves a **Def** free-param scope open for the
565    /// caller to parse `= obj` and then call `end_scope`.
566    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(&params, tb.line_file.clone())?;
653            tb.skip_token(COLON)?;
654            this.parsing_free_param_collection.begin_scope(
655                ParamObjType::DefAlgo,
656                &params,
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, &params_for_end);
686            Ok(algo_result?.into())
687        })
688    }
689
690    /// head 里是 if and_spec_fact :,body 有且只有一个块,即 return obj。
691    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    /// head 里是 return,后跟 obj。
705    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    /// `prop name` / similar: consumes `{` … `}` of typed param groups and registers names.
730    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    /// After `{` is consumed: param-type groups until `:` or `}` (family header); registers names.
749    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(&param_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}