litex/parse/by_stmt/
for_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn parse_by_for_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
5        tb.skip_token(FOR)?;
6        if tb.current()? != COLON {
7            let fact = self.parse_header_fact_before_trailing_colon(
8                tb,
9                "by for",
10                "by for => <forall fact>:",
11                "by for <forall fact>:",
12            )?;
13            let forall_fact = match fact {
14                Fact::ForallFact(ff) => ff,
15                Fact::ForallFactWithIff(_) => {
16                    return Err(RuntimeError::from(ParseRuntimeError(
17                        RuntimeErrorStruct::new_with_msg_and_line_file(
18                            "by for: forall with `<=>` is not allowed here".to_string(),
19                            tb.line_file.clone(),
20                        ),
21                    )));
22                }
23                _ => {
24                    return Err(RuntimeError::from(ParseRuntimeError(
25                        RuntimeErrorStruct::new_with_msg_and_line_file(
26                            "by for: header shorthand must be a single `forall` fact".to_string(),
27                            tb.line_file.clone(),
28                        ),
29                    )));
30                }
31            };
32
33            for g in forall_fact.params_def_with_type.groups.iter() {
34                match &g.param_type {
35                    ParamType::Obj(Obj::Range(_)) | ParamType::Obj(Obj::ClosedRange(_)) => {}
36                    _ => {
37                        return Err(RuntimeError::from(ParseRuntimeError(
38                            RuntimeErrorStruct::new_with_msg_and_line_file(
39                                "by for: each forall parameter type must be range or closed_range"
40                                    .to_string(),
41                                forall_fact.line_file.clone(),
42                            ),
43                        )));
44                    }
45                }
46            }
47
48            let names = forall_fact.params_def_with_type.collect_param_names();
49            let lf = tb.line_file.clone();
50            let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
51                ParamObjType::Forall,
52                &names,
53                lf,
54                |this| {
55                    tb.body
56                        .iter_mut()
57                        .map(|b| this.parse_stmt(b))
58                        .collect::<Result<_, _>>()
59                },
60            )?;
61
62            return Ok(ByForStmt::new(forall_fact, proof, tb.line_file.clone()).into());
63        }
64        tb.skip_token(COLON)?;
65        if !tb.exceed_end_of_head() {
66            return Err(RuntimeError::from(ParseRuntimeError(
67                RuntimeErrorStruct::new_with_msg_and_line_file(
68                    "by for: expected `:` immediately after `for`".to_string(),
69                    tb.line_file.clone(),
70                ),
71            )));
72        }
73        if tb.body.is_empty() {
74            return Err(RuntimeError::from(ParseRuntimeError(
75                RuntimeErrorStruct::new_with_msg_and_line_file(
76                    "by for: expects a body".to_string(),
77                    tb.line_file.clone(),
78                ),
79            )));
80        }
81
82        let prove_block = tb.body.get_mut(0).ok_or_else(|| {
83            RuntimeError::from(ParseRuntimeError(
84                RuntimeErrorStruct::new_with_msg_and_line_file(
85                    "by for: expected prove block".to_string(),
86                    tb.line_file.clone(),
87                ),
88            ))
89        })?;
90        if prove_block.header.get(0).map(|s| s.as_str()) != Some(PROVE) {
91            return Err(RuntimeError::from(ParseRuntimeError(
92                RuntimeErrorStruct::new_with_msg_and_line_file(
93                    "by for: first block must be `prove:`".to_string(),
94                    prove_block.line_file.clone(),
95                ),
96            )));
97        }
98        prove_block.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
99        if prove_block.body.len() != 1 {
100            return Err(RuntimeError::from(ParseRuntimeError(
101                RuntimeErrorStruct::new_with_msg_and_line_file(
102                    "by for: `prove:` must contain exactly one forall fact".to_string(),
103                    prove_block.line_file.clone(),
104                ),
105            )));
106        }
107
108        let forall_block = prove_block.body.get_mut(0).ok_or_else(|| {
109            RuntimeError::from(ParseRuntimeError(
110                RuntimeErrorStruct::new_with_msg_and_line_file(
111                    "by for: missing forall block".to_string(),
112                    tb.line_file.clone(),
113                ),
114            ))
115        })?;
116        let fact = self.parse_fact(forall_block)?;
117        let forall_fact = match fact {
118            Fact::ForallFact(ff) => ff,
119            Fact::ForallFactWithIff(_) => {
120                return Err(RuntimeError::from(ParseRuntimeError(
121                    RuntimeErrorStruct::new_with_msg_and_line_file(
122                        "by for: forall with `<=>` is not allowed here".to_string(),
123                        forall_block.line_file.clone(),
124                    ),
125                )));
126            }
127            _ => {
128                return Err(RuntimeError::from(ParseRuntimeError(
129                    RuntimeErrorStruct::new_with_msg_and_line_file(
130                        "by for: `prove:` must be a single `forall` fact".to_string(),
131                        forall_block.line_file.clone(),
132                    ),
133                )));
134            }
135        };
136
137        for g in forall_fact.params_def_with_type.groups.iter() {
138            match &g.param_type {
139                ParamType::Obj(Obj::Range(_)) | ParamType::Obj(Obj::ClosedRange(_)) => {}
140                _ => {
141                    return Err(RuntimeError::from(ParseRuntimeError(
142                        RuntimeErrorStruct::new_with_msg_and_line_file(
143                            "by for: each forall parameter type must be range or closed_range"
144                                .to_string(),
145                            forall_fact.line_file.clone(),
146                        ),
147                    )));
148                }
149            }
150        }
151
152        let names = forall_fact.params_def_with_type.collect_param_names();
153        let lf = tb.line_file.clone();
154        let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
155            ParamObjType::Forall,
156            &names,
157            lf,
158            |this| {
159                tb.body
160                    .iter_mut()
161                    .skip(1)
162                    .map(|b| this.parse_stmt(b))
163                    .collect::<Result<_, _>>()
164            },
165        )?;
166
167        Ok(ByForStmt::new(forall_fact, proof, tb.line_file.clone()).into())
168    }
169}
litex/parse/by_stmt/for_by_stmt.rs

litex/parse/by_stmt/
for_by_stmt.rs
