litex/parse/by_stmt/
induc_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn parse_by_induc_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
5        tb.skip_token(INDUC)?;
6        self.parse_induc_stmt_after_keyword(tb, false)
7    }
8
9    pub fn parse_strong_induc_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
10        tb.skip_token(STRONG_INDUC)?;
11        self.parse_induc_stmt_after_keyword(tb, true)
12    }
13
14    fn parse_induc_stmt_after_keyword(
15        &mut self,
16        tb: &mut TokenBlock,
17        strong: bool,
18    ) -> Result<Stmt, RuntimeError> {
19        let param = tb.advance()?;
20
21        tb.skip_token(FROM)?;
22        let induc_from = self.parse_obj(tb)?;
23        tb.skip_token(COLON)?;
24        if !tb.exceed_end_of_head() {
25            return Err(RuntimeError::from(ParseRuntimeError(
26                RuntimeErrorStruct::new_with_msg_and_line_file(
27                    "induc: expected end of head".to_string(),
28                    tb.line_file.clone(),
29                ),
30            )));
31        }
32
33        if tb.body.is_empty() {
34            return Err(RuntimeError::from(ParseRuntimeError(
35                RuntimeErrorStruct::new_with_msg_and_line_file(
36                    "induc: expects prove: block".to_string(),
37                    tb.line_file.clone(),
38                ),
39            )));
40        }
41
42        tb.body[0].skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
43
44        if tb.body[0].body.is_empty() {
45            return Err(RuntimeError::from(ParseRuntimeError(
46                RuntimeErrorStruct::new_with_msg_and_line_file(
47                    "induc prove: expects at least one fact to prove".to_string(),
48                    tb.body[0].line_file.clone(),
49                ),
50            )));
51        }
52
53        let prove_line = tb.body[0].line_file.clone();
54        let induc_param = [param.clone()];
55        let mut to_prove: Vec<ExistOrAndChainAtomicFact> = Vec::new();
56        self.parse_in_local_free_param_scope(
57            ParamObjType::Induc,
58            &induc_param,
59            prove_line,
60            |this| {
61                for block in tb.body[0].body.iter_mut() {
62                    to_prove.push(this.parse_exist_or_and_chain_atomic_fact(block)?);
63                }
64                Ok(())
65            },
66        )?;
67
68        let proof_line = tb.line_file.clone();
69        let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
70            ParamObjType::Induc,
71            &induc_param,
72            proof_line,
73            |this| {
74                tb.body
75                    .iter_mut()
76                    .skip(1)
77                    .map(|b| this.parse_stmt(b))
78                    .collect::<Result<_, _>>()
79            },
80        )?;
81
82        Ok(ByInducStmt::new(
83            to_prove,
84            param,
85            induc_from,
86            proof,
87            tb.line_file.clone(),
88            strong,
89        )
90        .into())
91    }
92}
litex/parse/by_stmt/induc_by_stmt.rs

litex/parse/by_stmt/
induc_by_stmt.rs
