litex/parse/by_stmt/
extension_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn parse_by_extension_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
5        tb.skip_token_and_colon_and_exceed_end_of_head(EXTENSION)?;
6
7        if tb.body.is_empty() {
8            return Err(RuntimeError::from(ParseRuntimeError(
9                RuntimeErrorStruct::new_with_msg_and_line_file(
10                    "by extension: expects at least one body block".to_string(),
11                    tb.line_file.clone(),
12                ),
13            )));
14        }
15
16        tb.body[0].skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
17
18        if tb.body[0].body.len() != 1 {
19            return Err(RuntimeError::from(ParseRuntimeError(
20                RuntimeErrorStruct::new_with_msg_and_line_file(
21                    "by extension: prove: expects exactly one atomic fact block".to_string(),
22                    tb.body[0].line_file.clone(),
23                ),
24            )));
25        }
26
27        let to_prove_equal_fact = self.parse_atomic_fact(
28            tb.body[0].body.get_mut(0).ok_or_else(|| {
29                RuntimeError::from(ParseRuntimeError(
30                    RuntimeErrorStruct::new_with_msg_and_line_file(
31                        "Expected body".to_string(),
32                        tb.line_file.clone(),
33                    ),
34                ))
35            })?,
36            true,
37        )?;
38
39        let (left, right) = match to_prove_equal_fact {
40            AtomicFact::EqualFact(equal_fact) => (equal_fact.left, equal_fact.right),
41            _ => {
42                return Err(RuntimeError::from(ParseRuntimeError(
43                    RuntimeErrorStruct::new_with_msg_and_line_file(
44                        "by extension: prove: expects equal fact".to_string(),
45                        tb.line_file.clone(),
46                    ),
47                )));
48            }
49        };
50
51        let mut proof: Vec<Stmt> = vec![];
52        for block in tb.body[1..].iter_mut() {
53            proof.push(self.parse_stmt(block)?);
54        }
55
56        Ok(ByExtensionStmt::new(left, right, proof, tb.line_file.clone()).into())
57    }
58}
litex/parse/by_stmt/extension_by_stmt.rs

litex/parse/by_stmt/
extension_by_stmt.rs
