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            let facts_result: Result<Vec<Fact>, RuntimeError> = if tb.exceed_end_of_head() {
107                self.parse_facts_in_body(tb)
108            } else {
109                let mut facts = Vec::new();
110                let parse_result = (|| {
111                    loop {
112                        facts.push(self.parse_fact(tb)?);
113                        if tb.exceed_end_of_head() {
114                            break;
115                        }
116                        tb.skip_token(COMMA)?;
117                        if tb.exceed_end_of_head() {
118                            return Err(RuntimeError::from(ParseRuntimeError(
119                                RuntimeErrorStruct::new_with_msg_and_line_file(
120                                    "expected fact after comma in inline let statement".to_string(),
121                                    tb.line_file.clone(),
122                                ),
123                            )));
124                        }
125                    }
126                    if !tb.body.is_empty() {
127                        return Err(RuntimeError::from(ParseRuntimeError(
128                            RuntimeErrorStruct::new_with_msg_and_line_file(
129                                "inline let statement cannot also have an indented body"
130                                    .to_string(),
131                                tb.line_file.clone(),
132                            ),
133                        )));
134                    }
135                    Ok(())
136                })();
137                parse_result.map(|_| facts)
138            };
139            if facts_result.is_err() && !all_param_names.is_empty() {
140                self.parsing_free_param_collection
141                    .end_scope(ParamObjType::Identifier, &all_param_names);
142            }
143            let facts = facts_result?;
144            self.parsing_free_param_collection
145                .end_scope(ParamObjType::Identifier, &all_param_names);
146            facts
147        } else {
148            if !all_param_names.is_empty() {
149                self.parsing_free_param_collection
150                    .end_scope(ParamObjType::Identifier, &all_param_names);
151            }
152            vec![]
153        };
154        Ok(DefLetStmt::new(param_def, facts, tb.line_file.clone()).into())
155    }
156
157    // return HaveObjInNonemptySetOrParamTypeStmt or HaveObjEqualStmt
158    pub fn parse_have_obj_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
159        tb.skip_token(HAVE)?;
160        let mut param_defs: Vec<ParamGroupWithParamType> = vec![];
161        loop {
162            param_defs.push(
163                self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Identifier)?,
164            );
165            match tb.current() {
166                Ok(t) if t == EQUAL => break,
167                Err(_) => break,
168                Ok(_) => {}
169            }
170        }
171        if param_defs.is_empty() {
172            return Err(RuntimeError::from(ParseRuntimeError(
173                RuntimeErrorStruct::new_with_msg_and_line_file(
174                    "have expects at least one param type pair".to_string(),
175                    tb.line_file.clone(),
176                ),
177            )));
178        }
179        let param_defs = ParamDefWithType::new(param_defs);
180        let have_param_names = param_defs.collect_param_names();
181        self.register_collected_param_names_for_def_parse(&have_param_names, tb.line_file.clone())?;
182
183        if tb.current().map(|t| t != EQUAL).unwrap_or(true) {
184            if !have_param_names.is_empty() {
185                self.parsing_free_param_collection
186                    .end_scope(ParamObjType::Identifier, &have_param_names);
187            }
188            Ok(HaveObjInNonemptySetOrParamTypeStmt::new(param_defs, tb.line_file.clone()).into())
189        } else {
190            tb.skip_token(EQUAL)?;
191            let objs_result = (|| -> Result<Vec<Obj>, RuntimeError> {
192                let mut objs_equal_to = vec![self.parse_obj(tb)?];
193                while matches!(tb.current(), Ok(t) if t == COMMA) {
194                    tb.skip_token(COMMA)?;
195                    objs_equal_to.push(self.parse_obj(tb)?);
196                }
197                Ok(objs_equal_to)
198            })();
199            self.parsing_free_param_collection
200                .end_scope(ParamObjType::Identifier, &have_param_names);
201            let objs_equal_to = objs_result?;
202            Ok(HaveObjEqualStmt::new(param_defs, objs_equal_to, tb.line_file.clone()).into())
203        }
204    }
205
206    pub fn parse_have_fn_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
207        tb.skip_token(HAVE)?;
208        tb.skip_token(FN_LOWER_CASE)?;
209        if tb.current_token_is_equal_to(BY) {
210            tb.skip_token(BY)?;
211            self.parse_have_fn_by_induc_stmt(tb)
212        } else {
213            let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
214            if tb.current_token_is_equal_to(BY) {
215                tb.skip_token(BY)?;
216                let lf = tb.line_file.clone();
217                let fact = self.parse_fact(tb)?;
218                let forall = match fact {
219                    Fact::ForallFact(ff) => ff,
220                    _ => {
221                        return Err(RuntimeError::from(ParseRuntimeError(
222                            RuntimeErrorStruct::new_with_msg_and_line_file(
223                                "have fn <name> by ... expects a `forall` fact".to_string(),
224                                lf,
225                            ),
226                        )));
227                    }
228                };
229                if !tb.exceed_end_of_head() {
230                    return Err(RuntimeError::from(ParseRuntimeError(
231                        RuntimeErrorStruct::new_with_msg_and_line_file(
232                            "unexpected token after `have fn` `by` `forall` fact".to_string(),
233                            tb.line_file.clone(),
234                        ),
235                    )));
236                }
237                return Ok(HaveFnByForallExistUniqueStmt::new(name, forall, lf).into());
238            }
239
240            let fs = self.parse_fn_set_clause(tb)?;
241            let fn_param_names = fs.collect_all_param_names_including_nested_ret_fn_sets();
242
243            if tb.current_token_is_equal_to(COLON) {
244                tb.skip_token(COLON)?;
245                let case_block_count = tb.body.len();
246                let mut cases: Vec<AndChainAtomicFact> = Vec::with_capacity(case_block_count);
247                let mut equal_tos: Vec<Obj> = Vec::with_capacity(case_block_count);
248                for block in tb.body.iter_mut() {
249                    block.skip_token(CASE)?;
250                    let case_lf = block.line_file.clone();
251                    cases.push(self.with_optional_free_param_scope(
252                        ParamObjType::FnSet,
253                        &fn_param_names,
254                        case_lf,
255                        |this| this.parse_and_chain_atomic_fact(block),
256                    )?);
257                    block.skip_token(COLON)?;
258                    let rhs_lf = block.line_file.clone();
259                    equal_tos.push(self.with_optional_free_param_scope(
260                        ParamObjType::FnSet,
261                        &fn_param_names,
262                        rhs_lf,
263                        |this| this.parse_obj(block),
264                    )?);
265                }
266                Ok(
267                    HaveFnEqualCaseByCaseStmt::new(
268                        name,
269                        fs,
270                        cases,
271                        equal_tos,
272                        tb.line_file.clone(),
273                    )
274                    .into(),
275                )
276            } else {
277                tb.skip_token(EQUAL)?;
278
279                let lf = tb.line_file.clone();
280                let equal_to = self.with_optional_free_param_scope(
281                    ParamObjType::FnSet,
282                    &fn_param_names,
283                    lf,
284                    |this| this.parse_obj(tb),
285                )?;
286                let equal_to_anonymous_fn = AnonymousFn::new(
287                    fs.params_def_with_set.clone(),
288                    fs.dom_facts.clone(),
289                    fs.ret_set.clone(),
290                    equal_to,
291                )?;
292                Ok(HaveFnEqualStmt::new(name, equal_to_anonymous_fn, tb.line_file.clone()).into())
293            }
294        }
295    }
296
297    /// `have fn by` 已消费；解析 `induc from <Obj>: <name> ( <param> Z: <param> >= <induc_from> ) <ret_set> : case ...`。
298    /// 前若干条特例为 `case <k>: obj`，其中 `<k>` 为 **0 起下标占位符**，须与该行顺序一致（第 1 条为 0，第 2 条为 1，…）；
299    /// 最后一条须为 `case >= n:`，其中 **n 为特例个数**（数字字面量）；且要么行末 `: obj`，要么 `:` 后换行跟子块 `case when: obj`。
300    fn parse_have_fn_by_induc_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
301        tb.skip_token(INDUC)?;
302        tb.skip_token(FROM)?;
303        let induc_from = self.parse_obj(tb)?;
304        tb.skip_token(COLON)?;
305        let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
306
307        tb.skip_token(LEFT_BRACE)?;
308        let param = tb.advance()?;
309        if !tb.current_token_is_equal_to(Z) {
310            return Err(RuntimeError::from(ParseRuntimeError(
311                RuntimeErrorStruct::new_with_msg_and_line_file(
312                    "have fn by induc from: expected `Z` after parameter name".to_string(),
313                    tb.line_file.clone(),
314                ),
315            )));
316        }
317        tb.skip_token(Z)?;
318        tb.skip_token(COLON)?;
319
320        self.run_in_local_parsing_time_name_scope(|this| {
321            this.parse_have_fn_by_induc_stmt_after_param_scope(tb, name, param, induc_from)
322        })
323    }
324
325    fn parse_have_fn_by_induc_stmt_after_param_scope(
326        &mut self,
327        tb: &mut TokenBlock,
328        name: String,
329        param: String,
330        induc_from: Obj,
331    ) -> Result<Stmt, RuntimeError> {
332        self.validate_user_fn_param_names_for_parse(&[param.clone()], tb.line_file.clone())?;
333        let dom_and_chain = self.parse_and_chain_atomic_fact(tb)?;
334        Self::verify_have_fn_by_induc_dom_matches_induc_from(
335            &dom_and_chain,
336            &param,
337            &induc_from,
338            tb.line_file.clone(),
339        )?;
340        tb.skip_token(RIGHT_BRACE)?;
341        let ret_set = self.parse_obj(tb)?;
342
343        if !tb.current_token_is_equal_to(COLON) {
344            return Err(RuntimeError::from(ParseRuntimeError(
345                RuntimeErrorStruct::new_with_msg_and_line_file(
346                    "have fn by induc from: expected `:` before case blocks".to_string(),
347                    tb.line_file.clone(),
348                ),
349            )));
350        }
351        tb.skip_token(COLON)?;
352
353        let num_blocks = tb.body.len();
354        if num_blocks <= 1 {
355            return Err(RuntimeError::from(ParseRuntimeError(
356                RuntimeErrorStruct::new_with_msg_and_line_file(
357                    "have fn by induc from: expected at least two case blocks".to_string(),
358                    tb.line_file.clone(),
359                ),
360            )));
361        }
362
363        let num_special = num_blocks - 1;
364        let mut special_cases_equal_tos: Vec<Obj> = Vec::with_capacity(num_special);
365
366        let induc_from_is_number_obj = matches!(induc_from, Obj::Number(_));
367        if induc_from_is_number_obj {
368            if let Obj::Number(n) = &induc_from {
369                if !number_is_in_z(n) {
370                    return Err(
371                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
372                                "have fn by induc from: when `from` is a number literal, it must be an integer, got {}",
373                                induc_from.to_string()
374                            ), tb.line_file.clone()))));
375                }
376            }
377        }
378
379        for i in 0..num_special {
380            let block = &mut tb.body[i];
381            block.skip_token(CASE)?;
382
383            block.skip_token(&param)?;
384
385            block.skip_token(EQUAL)?;
386
387            let slot_label = self.parse_obj(block)?;
388            Self::verify_have_fn_by_induc_special_case_slot_label(
389                &slot_label,
390                i,
391                block.line_file.clone(),
392            )?;
393
394            if induc_from_is_number_obj {
395                let induc_from_add_i: Obj = Add::new(
396                    induc_from.clone(),
397                    Into::<Obj>::into(Number::new(i.to_string())),
398                )
399                .into();
400
401                if !induc_from_add_i
402                    .two_objs_can_be_calculated_and_equal_by_calculation(&slot_label)
403                {
404                    return Err(
405                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
406                                "have fn by induc from: when `from` is a number literal, special case must be `case {} = {}:` (`from` + {}), got {}",
407                                param, induc_from_add_i.to_string(), i, slot_label.to_string()
408                            ), block.line_file.clone()))));
409                }
410            } else {
411                let induc_from_add_i: Obj = Add::new(
412                    induc_from.clone(),
413                    Into::<Obj>::into(Number::new(i.to_string())),
414                )
415                .into();
416
417                if induc_from_add_i.to_string() != slot_label.to_string() {
418                    return Err(
419                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
420                                "have fn by induc from: when `from` is not a number literal, special case must be `case {} = {}:`, got {}",
421                                param, induc_from_add_i.to_string(), slot_label.to_string()
422                            ), block.line_file.clone()))));
423                }
424            }
425
426            block.skip_token(COLON)?;
427            if !block.exceed_end_of_head() {
428                special_cases_equal_tos.push(self.parse_obj(block)?);
429            } else {
430                return Err(
431                    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"
432                            .to_string(), block.line_file.clone()))));
433            }
434        }
435
436        let induc_names_last = [param.clone()];
437        let last_case_line = tb.body[num_blocks - 1].line_file.clone();
438        let last_case = self.parse_in_local_free_param_scope(
439            ParamObjType::Induc,
440            &induc_names_last,
441            last_case_line,
442            |this| {
443                let last_block = &mut tb.body[num_blocks - 1];
444                last_block.skip_token(CASE)?;
445                last_block.skip_token(&param)?;
446                last_block.skip_token(GREATER_EQUAL)?;
447                let last_bound = this.parse_obj(last_block)?;
448
449                if induc_from_is_number_obj {
450                    let induc_from_add_n: Obj = Add::new(
451                        induc_from.clone(),
452                        Into::<Obj>::into(Number::new(num_special.to_string())),
453                    )
454                    .into();
455                    if !induc_from_add_n
456                        .two_objs_can_be_calculated_and_equal_by_calculation(&last_bound)
457                    {
458                        return Err(
459                            RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
460                            "have fn by induc from: when `from` is a number literal, last case must be `case >= {}:` (`from` + {}), got {}",
461                            induc_from_add_n.to_string(), num_special, last_bound.to_string()
462                        ), last_block.line_file.clone()))));
463                    }
464                } else {
465                    let induc_from_add_n: Obj = Add::new(
466                        induc_from.clone(),
467                        Into::<Obj>::into(Number::new(num_special.to_string())),
468                    )
469                    .into();
470                    if induc_from_add_n.to_string() != last_bound.to_string() {
471                        return Err(
472                            RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
473                            "have fn by induc from: when `from` is not a number literal, last case must be `case >= {}:`, got {}",
474                            induc_from_add_n.to_string(), last_bound.to_string()
475                        ), last_block.line_file.clone()))));
476                    }
477                }
478
479                last_block.skip_token(COLON)?;
480
481                if !last_block.exceed_end_of_head() {
482                    let last_obj = this.parse_obj(last_block)?;
483                    if !last_block.exceed_end_of_head() {
484                        return Err(
485                            RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: unexpected tokens after `obj` in last case"
486                            .to_string(), last_block.line_file.clone()))));
487                    }
488                    if !last_block.body.is_empty() {
489                        return Err(
490                        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"
491                                .to_string(), last_block.line_file.clone()))));
492                    }
493                    Ok(HaveFnByInducLastCase::EqualTo(last_obj))
494                } else if !last_block.body.is_empty() {
495                    let mut nested: Vec<HaveFnByInducNestedCase> =
496                        Vec::with_capacity(last_block.body.len());
497                    for sub in last_block.body.iter_mut() {
498                        sub.skip_token(CASE)?;
499                        let w = this.parse_and_chain_atomic_fact(sub)?;
500                        sub.skip_token(COLON)?;
501                        if sub.exceed_end_of_head() {
502                            return Err(
503                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must be `case <when>: <obj>`"
504                                .to_string(), sub.line_file.clone()))));
505                        }
506                        let o = this.parse_obj(sub)?;
507                        if !sub.body.is_empty() {
508                            return Err(
509                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: nested case must not have further indentation"
510                                .to_string(), sub.line_file.clone()))));
511                        }
512                        nested.push(HaveFnByInducNestedCase {
513                            case_fact: w,
514                            equal_to: o,
515                        });
516                    }
517                    Ok(HaveFnByInducLastCase::NestedCases(nested))
518                } else {
519                    Err(RuntimeError::from(ParseRuntimeError(
520                        RuntimeErrorStruct::new_with_msg_and_line_file("have fn by induc from: last case must end with `: <obj>` or `:` with nested `case` blocks"
521                                .to_string(), last_block.line_file.clone()),
522                    )))
523                }
524            },
525        )?;
526
527        Ok(HaveFnByInducStmt::new(
528            name,
529            param,
530            ret_set,
531            induc_from,
532            special_cases_equal_tos,
533            last_case,
534            tb.line_file.clone(),
535        )
536        .into())
537    }
538
539    fn verify_have_fn_by_induc_dom_matches_induc_from(
540        when: &AndChainAtomicFact,
541        param_name: &str,
542        induc_from: &Obj,
543        line_file: LineFile,
544    ) -> Result<(), RuntimeError> {
545        let ge = match when {
546            AndChainAtomicFact::AtomicFact(AtomicFact::GreaterEqualFact(ge)) => ge,
547            _ => {
548                return Err(RuntimeError::from(ParseRuntimeError(
549                    RuntimeErrorStruct::new_with_msg_and_line_file(
550                        "have fn by induc from: dom fact must be a single `>=` fact".to_string(),
551                        line_file,
552                    ),
553                )));
554            }
555        };
556        match &ge.left {
557            Obj::Atom(AtomObj::Identifier(id)) if id.name == param_name => {}
558            _ => {
559                return Err(RuntimeError::from(ParseRuntimeError(
560                    RuntimeErrorStruct::new_with_msg_and_line_file(
561                        "have fn by induc from: `>=` left must be the parameter name".to_string(),
562                        line_file,
563                    ),
564                )));
565            }
566        }
567        if ge.right.to_string() != induc_from.to_string() {
568            return Err(RuntimeError::from(ParseRuntimeError(
569                RuntimeErrorStruct::new_with_msg_and_line_file(
570                    "have fn by induc from: `>=` right must match the object after `from`"
571                        .to_string(),
572                    line_file,
573                ),
574            )));
575        }
576        Ok(())
577    }
578
579    /// 特例行 `case <k>:`：`<k>` 须为自然数字面量，且等于该行在特例中的 **0-based 顺序**（第 1 条为 0，第 2 条为 1，…）。
580    fn verify_have_fn_by_induc_special_case_slot_label(
581        slot: &Obj,
582        expected_index: usize,
583        line_file: LineFile,
584    ) -> Result<(), RuntimeError> {
585        match slot {
586            Obj::Number(n) => {
587                if n.normalized_value == expected_index.to_string() {
588                    Ok(())
589                } else {
590                    Err(
591                        RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(format!(
592                                "have fn by induc from: special case label must be `{}` (0-based index for this row), got {}",
593                                expected_index, n.normalized_value
594                            ), line_file))))
595                }
596            }
597            _ => Err(
598                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, …)"
599                        .to_string(), line_file)))),
600        }
601    }
602
603    pub fn parse_have_exist(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
604        tb.skip_token(HAVE)?;
605        tb.skip_token(BY)?;
606
607        let true_fact = self.parse_exist_fact(tb)?;
608
609        tb.skip_token(COLON)?;
610
611        let mut equal_tos = vec![];
612        while !tb.exceed_end_of_head() {
613            equal_tos.push(tb.advance()?);
614            if tb.current_token_is_equal_to(COMMA) {
615                tb.skip_token(COMMA)?;
616            }
617        }
618
619        self.register_collected_param_names_for_def_parse(&equal_tos, tb.line_file.clone())?;
620
621        Ok(HaveByExistStmt::new(equal_tos, true_fact, tb.line_file.clone()).into())
622    }
623
624    /// Parses `{ params [: dom_facts] }` for `family`. Leaves a **Def** free-param scope open for the
625    /// caller to parse `= obj` and then call `end_scope`.
626    fn parse_braced_params_and_optional_dom_facts(
627        &mut self,
628        tb: &mut TokenBlock,
629    ) -> Result<(ParamDefWithType, Vec<OrAndChainAtomicFact>), RuntimeError> {
630        tb.skip_token(LEFT_BRACE)?;
631        let params_def_with_type =
632            self.parse_def_param_type_groups_until_colon_or_right_brace(tb)?;
633        let scope_names = params_def_with_type.collect_param_names();
634        let dom_facts = if tb.current_token_is_equal_to(COLON) {
635            tb.skip_token(COLON)?;
636            let mut facts = vec![];
637            let dom_result = loop {
638                if tb.current()? == RIGHT_BRACE {
639                    break Ok(facts);
640                }
641                match self.parse_or_and_chain_atomic_fact(tb) {
642                    Ok(f) => facts.push(f),
643                    Err(e) => {
644                        self.parsing_free_param_collection
645                            .end_scope(ParamObjType::DefHeader, &scope_names);
646                        break Err(e);
647                    }
648                }
649                if tb.current_token_is_equal_to(COMMA) {
650                    tb.skip_token(COMMA)?;
651                }
652            };
653            dom_result?
654        } else {
655            vec![]
656        };
657        if let Err(e) = tb.skip_token(RIGHT_BRACE) {
658            self.parsing_free_param_collection
659                .end_scope(ParamObjType::DefHeader, &scope_names);
660            return Err(e);
661        }
662        Ok((params_def_with_type, dom_facts))
663    }
664
665    pub fn parse_def_family_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
666        tb.skip_token(FAMILY)?;
667        let name = self.parse_name_and_insert_into_top_parsing_time_name_scope(tb)?;
668
669        self.run_in_local_parsing_time_name_scope(move |this| {
670            let (params_def_with_type, dom_facts) =
671                this.parse_braced_params_and_optional_dom_facts(tb)?;
672            let family_def_scope_names = params_def_with_type.collect_param_names();
673            let stmt_result = (|| -> Result<Stmt, RuntimeError> {
674                if !tb.current_token_is_equal_to(EQUAL) {
675                    return Err(RuntimeError::from(ParseRuntimeError(
676                        RuntimeErrorStruct::new_with_msg_and_line_file(
677                            "family definition expects `=` after `}`".to_string(),
678                            tb.line_file.clone(),
679                        ),
680                    )));
681                }
682                tb.skip_token(EQUAL)?;
683                let equal_to = this.parse_obj(tb)?;
684                Ok(DefFamilyStmt::new(
685                    name,
686                    params_def_with_type,
687                    dom_facts,
688                    equal_to,
689                    tb.line_file.clone(),
690                )
691                .into())
692            })();
693            this.parsing_free_param_collection
694                .end_scope(ParamObjType::DefHeader, &family_def_scope_names);
695            stmt_result
696        })
697    }
698
699    pub fn parse_def_algorithm_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
700        tb.skip_token(ALGO)?;
701        let name = tb.advance()?;
702        self.run_in_local_parsing_time_name_scope(move |this| {
703            tb.skip_token(LEFT_BRACE)?;
704            let mut params: Vec<String> = vec![];
705            while tb.current()? != RIGHT_BRACE {
706                params.push(tb.advance()?);
707                if tb.current_token_is_equal_to(COMMA) {
708                    tb.skip_token(COMMA)?;
709                }
710            }
711            tb.skip_token(RIGHT_BRACE)?;
712            this.register_collected_param_names_for_def_parse(&params, tb.line_file.clone())?;
713            tb.skip_token(COLON)?;
714            this.parsing_free_param_collection.begin_scope(
715                ParamObjType::DefAlgo,
716                &params,
717                tb.line_file.clone(),
718            )?;
719            let params_for_end = params.clone();
720            let algo_result = (|| -> Result<DefAlgoStmt, RuntimeError> {
721                let mut algo_cases: Vec<AlgoCase> = vec![];
722                let mut default_return: Option<AlgoReturn> = None;
723                match tb.body.split_last_mut() {
724                    None => {}
725                    Some((last_block, leading_blocks)) => {
726                        for block in leading_blocks.iter_mut() {
727                            algo_cases.push(this.parse_algo_case(block)?);
728                        }
729                        if last_block.current_token_empty_if_exceed_end_of_head() == CASE {
730                            algo_cases.push(this.parse_algo_case(last_block)?);
731                        } else {
732                            default_return = Some(this.parse_algo_return(last_block)?);
733                        }
734                    }
735                }
736                Ok(DefAlgoStmt::new(
737                    name,
738                    params,
739                    algo_cases,
740                    default_return,
741                    tb.line_file.clone(),
742                ))
743            })();
744            this.parsing_free_param_collection
745                .end_scope(ParamObjType::DefAlgo, &params_for_end);
746            Ok(algo_result?.into())
747        })
748    }
749
750    /// head 里是 if and_spec_fact :，body 有且只有一个块，即 return obj。
751    fn parse_algo_case(&mut self, block: &mut TokenBlock) -> Result<AlgoCase, RuntimeError> {
752        block.skip_token(CASE)?;
753        let condition = self.parse_atomic_fact(block, true)?;
754        block.skip_token(COLON)?;
755
756        let return_stmt = self.parse_algo_return(block)?;
757        Ok(AlgoCase::new(
758            condition,
759            return_stmt,
760            block.line_file.clone(),
761        ))
762    }
763
764    /// head 里是 return，后跟 obj。
765    fn parse_algo_return(&mut self, block: &mut TokenBlock) -> Result<AlgoReturn, RuntimeError> {
766        let value = self.parse_obj(block)?;
767        Ok(AlgoReturn::new(value, block.line_file.clone()))
768    }
769}
770
771impl Runtime {
772    pub fn register_collected_param_names_for_def_parse(
773        &mut self,
774        names: &Vec<String>,
775        line_file: LineFile,
776    ) -> Result<(), RuntimeError> {
777        self.validate_names_and_insert_into_top_parsing_time_name_scope(names, line_file.clone())
778            .map_err(|e| {
779                RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
780                    None,
781                    String::new(),
782                    line_file,
783                    Some(e),
784                    vec![],
785                )))
786            })
787    }
788
789    /// `prop name` / similar: consumes `{` … `}` of typed param groups and registers names.
790    fn parse_def_braced_param_groups_with_param_type(
791        &mut self,
792        tb: &mut TokenBlock,
793    ) -> Result<ParamDefWithType, RuntimeError> {
794        tb.skip_token(LEFT_BRACE)?;
795        let mut groups = Vec::new();
796        while tb.current()? != RIGHT_BRACE {
797            groups.push(
798                self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
799            );
800        }
801        tb.skip_token(RIGHT_BRACE)?;
802        let param_defs = ParamDefWithType::new(groups);
803        let names = param_defs.collect_param_names();
804        self.register_collected_param_names_for_def_parse(&names, tb.line_file.clone())?;
805        Ok(param_defs)
806    }
807
808    /// After `{` is consumed: param-type groups until `:` or `}` (family header); registers names.
809    fn parse_def_param_type_groups_until_colon_or_right_brace(
810        &mut self,
811        tb: &mut TokenBlock,
812    ) -> Result<ParamDefWithType, RuntimeError> {
813        let mut groups = vec![];
814        while tb.current()? != COLON && tb.current()? != RIGHT_BRACE {
815            groups.push(
816                self.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::DefHeader)?,
817            );
818        }
819        let params_def_with_type = ParamDefWithType::new(groups);
820        let param_names = params_def_with_type.collect_param_names();
821        self.register_collected_param_names_for_def_parse(&param_names, tb.line_file.clone())?;
822        Ok(params_def_with_type)
823    }
824
825    pub fn insert_parsed_name_into_top_parsing_time_name_scope(
826        &mut self,
827        name: &str,
828        line_file: LineFile,
829    ) -> Result<(), RuntimeError> {
830        self.validate_name_and_insert_into_top_parsing_time_name_scope(name, line_file.clone())
831            .map_err(|e| {
832                RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new(
833                    None,
834                    String::new(),
835                    line_file,
836                    Some(e),
837                    vec![],
838                )))
839            })
840    }
841
842    pub fn parse_name_and_insert_into_top_parsing_time_name_scope(
843        &mut self,
844        tb: &mut TokenBlock,
845    ) -> Result<String, RuntimeError> {
846        let name = tb.advance()?;
847        self.insert_parsed_name_into_top_parsing_time_name_scope(&name, tb.line_file.clone())?;
848        Ok(name)
849    }
850}
litex/parse/parse_def_stmt.rs

litex/parse/
parse_def_stmt.rs
