litex/parse/by_stmt/
commutative_prop_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn parse_by_commutative_prop_stmt(
5        &mut self,
6        tb: &mut TokenBlock,
7    ) -> Result<Stmt, RuntimeError> {
8        tb.skip_token(COMMUTATIVE_PROP)?;
9        tb.skip_token(COLON)?;
10        if !tb.exceed_end_of_head() {
11            return Err(RuntimeError::from(ParseRuntimeError(
12                RuntimeErrorStruct::new_with_msg_and_line_file(
13                    "by commutative_prop: expected end of head after `:`".to_string(),
14                    tb.line_file.clone(),
15                ),
16            )));
17        }
18        if tb.body.is_empty() {
19            return Err(RuntimeError::from(ParseRuntimeError(
20                RuntimeErrorStruct::new_with_msg_and_line_file(
21                    "by commutative_prop: expects a body".to_string(),
22                    tb.line_file.clone(),
23                ),
24            )));
25        }
26
27        let prove_block = tb.body.get_mut(0).ok_or_else(|| {
28            RuntimeError::from(ParseRuntimeError(
29                RuntimeErrorStruct::new_with_msg_and_line_file(
30                    "by commutative_prop: expected prove block".to_string(),
31                    tb.line_file.clone(),
32                ),
33            ))
34        })?;
35        if prove_block.header.get(0).map(|s| s.as_str()) != Some(PROVE) {
36            return Err(RuntimeError::from(ParseRuntimeError(
37                RuntimeErrorStruct::new_with_msg_and_line_file(
38                    "by commutative_prop: first block must be `prove:`".to_string(),
39                    prove_block.line_file.clone(),
40                ),
41            )));
42        }
43        prove_block.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
44        if prove_block.body.len() != 1 {
45            return Err(RuntimeError::from(ParseRuntimeError(
46                RuntimeErrorStruct::new_with_msg_and_line_file(
47                    "by commutative_prop: `prove:` must contain exactly one forall fact"
48                        .to_string(),
49                    prove_block.line_file.clone(),
50                ),
51            )));
52        }
53
54        let forall_block = prove_block.body.get_mut(0).ok_or_else(|| {
55            RuntimeError::from(ParseRuntimeError(
56                RuntimeErrorStruct::new_with_msg_and_line_file(
57                    "by commutative_prop: missing forall block".to_string(),
58                    tb.line_file.clone(),
59                ),
60            ))
61        })?;
62        let fact = self.parse_fact(forall_block)?;
63        let forall_fact = match fact {
64            Fact::ForallFact(ff) => ff,
65            Fact::ForallFactWithIff(_) => {
66                return Err(RuntimeError::from(ParseRuntimeError(
67                    RuntimeErrorStruct::new_with_msg_and_line_file(
68                        "by commutative_prop: forall with `<=>` is not allowed here".to_string(),
69                        forall_block.line_file.clone(),
70                    ),
71                )));
72            }
73            _ => {
74                return Err(RuntimeError::from(ParseRuntimeError(
75                    RuntimeErrorStruct::new_with_msg_and_line_file(
76                        "by commutative_prop: `prove:` must be a single `forall` fact".to_string(),
77                        forall_block.line_file.clone(),
78                    ),
79                )));
80            }
81        };
82
83        let shape_check =
84            ByCommutativePropStmt::new(forall_fact.clone(), Vec::new(), tb.line_file.clone())
85                .commutative_prop_registration();
86        if let Err(msg) = shape_check {
87            return Err(RuntimeError::from(ParseRuntimeError(
88                RuntimeErrorStruct::new_with_msg_and_line_file(msg, forall_fact.line_file.clone()),
89            )));
90        }
91
92        let names = forall_fact.params_def_with_type.collect_param_names();
93        let lf = tb.line_file.clone();
94        let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
95            ParamObjType::Forall,
96            &names,
97            lf,
98            |this| {
99                tb.body
100                    .iter_mut()
101                    .skip(1)
102                    .map(|b| this.parse_stmt(b))
103                    .collect::<Result<_, _>>()
104            },
105        )?;
106
107        Ok(ByCommutativePropStmt::new(forall_fact, proof, tb.line_file.clone()).into())
108    }
109}
litex/parse/by_stmt/commutative_prop_by_stmt.rs

litex/parse/by_stmt/
commutative_prop_by_stmt.rs
