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