litex/parse/by_stmt/
cases_by_stmt.rs

1use crate::parse::parse_helpers::collect_forall_param_names_from_facts;
2use crate::prelude::*;
3
4impl Runtime {
5    pub fn parse_by_cases_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
6        tb.skip_token(CASES)?;
7        // `by cases goal:` puts the goal on the header line; body starts with `case` arms.
8        let (then_facts, case_body_skip): (Vec<Fact>, usize) = if tb.current()? == COLON {
9            tb.skip_token(COLON)?;
10            if tb.body.is_empty() {
11                return Err(RuntimeError::from(ParseRuntimeError(
12                    RuntimeErrorStruct::new_with_msg_and_line_file(
13                        "cases: expects at least one body block".to_string(),
14                        tb.line_file.clone(),
15                    ),
16                )));
17            }
18            let then_facts: Vec<Fact> = {
19                let first = tb.body.get_mut(0).ok_or_else(|| {
20                    RuntimeError::from(ParseRuntimeError(
21                        RuntimeErrorStruct::new_with_msg_and_line_file(
22                            "Expected body".to_string(),
23                            tb.line_file.clone(),
24                        ),
25                    ))
26                })?;
27                first.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
28                first
29                    .body
30                    .iter_mut()
31                    .map(|b| self.parse_fact(b))
32                    .collect::<Result<_, _>>()?
33            };
34            (then_facts, 1)
35        } else {
36            let fact = self.parse_header_fact_before_trailing_colon(
37                tb,
38                "by cases",
39                "by cases => <fact>:",
40                "by cases <fact>:",
41            )?;
42            (vec![fact], 0)
43        };
44
45        let min_body = case_body_skip + 1;
46        if tb.body.len() < min_body {
47            return Err(RuntimeError::from(ParseRuntimeError(
48                RuntimeErrorStruct::new_with_msg_and_line_file(
49                    "cases: expects at least one `case` arm".to_string(),
50                    tb.line_file.clone(),
51                ),
52            )));
53        }
54        let forall_param_names = collect_forall_param_names_from_facts(&then_facts);
55        let line_file = tb.line_file.clone();
56        let (cases, proofs, impossible_facts) = if forall_param_names.is_empty() {
57            self.parse_by_cases_case_and_proof_blocks(tb, case_body_skip)?
58        } else {
59            self.parse_in_local_free_param_scope(
60                ParamObjType::Forall,
61                &forall_param_names,
62                line_file,
63                |rt| rt.parse_by_cases_case_and_proof_blocks(tb, case_body_skip),
64            )?
65        };
66        Ok(ByCasesStmt::new(
67            cases,
68            then_facts,
69            proofs,
70            impossible_facts,
71            tb.line_file.clone(),
72        )
73        .into())
74    }
75
76    /// Parses all `case ...:` arms (conditions, proof bodies, optional `impossible` facts).
77    fn parse_by_cases_case_and_proof_blocks(
78        &mut self,
79        tb: &mut TokenBlock,
80        case_body_skip: usize,
81    ) -> Result<
82        (
83            Vec<AndChainAtomicFact>,
84            Vec<Vec<Stmt>>,
85            Vec<Option<AtomicFact>>,
86        ),
87        RuntimeError,
88    > {
89        let case_block_count = tb.body.len().saturating_sub(case_body_skip);
90        let mut cases: Vec<AndChainAtomicFact> = Vec::with_capacity(case_block_count);
91        let mut proofs: Vec<Vec<Stmt>> = Vec::with_capacity(case_block_count);
92        let mut impossible_facts: Vec<Option<AtomicFact>> = Vec::with_capacity(case_block_count);
93        for block in tb.body.iter_mut().skip(case_body_skip) {
94            block.skip_token(CASE)?;
95            let case = self.parse_and_chain_atomic_fact_allow_leading_not(block)?;
96            block.skip_token(COLON)?;
97            if !block.exceed_end_of_head() {
98                return Err(RuntimeError::from(ParseRuntimeError(
99                    RuntimeErrorStruct::new_with_msg_and_line_file(
100                        "case: expected end of head after condition".to_string(),
101                        block.line_file.clone(),
102                    ),
103                )));
104            }
105            cases.push(case);
106            let n = block.body.len();
107            if block.body.is_empty() {
108                proofs.push(vec![]);
109                impossible_facts.push(None);
110                continue;
111            }
112            let (proof_stmts, impossible) =
113                if block.body[n - 1].header.get(0).map(|s| s.as_str()) == Some(IMPOSSIBLE) {
114                    let proof: Vec<Stmt> = block.body[0..n - 1]
115                        .iter_mut()
116                        .map(|b| self.parse_stmt(b))
117                        .collect::<Result<_, _>>()?;
118                    let last_block = block.body.get_mut(n - 1).ok_or_else(|| {
119                        RuntimeError::from(ParseRuntimeError(
120                            RuntimeErrorStruct::new_with_msg_and_line_file(
121                                "Expected body".to_string(),
122                                tb.line_file.clone(),
123                            ),
124                        ))
125                    })?;
126                    last_block.skip_token(IMPOSSIBLE)?;
127                    let imp = self.parse_atomic_fact(last_block, true)?;
128                    (proof, Some(imp))
129                } else {
130                    let proof: Vec<Stmt> = block
131                        .body
132                        .iter_mut()
133                        .map(|b| self.parse_stmt(b))
134                        .collect::<Result<_, _>>()?;
135                    (proof, None)
136                };
137            proofs.push(proof_stmts);
138            impossible_facts.push(impossible);
139        }
140        Ok((cases, proofs, impossible_facts))
141    }
142}
litex/parse/by_stmt/cases_by_stmt.rs

litex/parse/by_stmt/
cases_by_stmt.rs
