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 if tb.current_token_is_equal_to(COLON) {
68 return Err(RuntimeError::from(ParseRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file("by enumerate: expected `finite_set` before `:` (use `by enumerate finite_set:`)"
69 .to_string(), tb.line_file.clone()))));
70 }
71 self.parse_by_enumerate_closed_range_stmt(tb)
72 }
73
74 fn parse_by_enumerate_finite_set_stmt_forall_in_prove(
76 &mut self,
77 tb: &mut TokenBlock,
78 ) -> Result<Stmt, RuntimeError> {
79 if !tb.exceed_end_of_head() {
80 return Err(RuntimeError::from(ParseRuntimeError(
81 RuntimeErrorStruct::new_with_msg_and_line_file(
82 "by enumerate finite_set: expected end of head after `:`".to_string(),
83 tb.line_file.clone(),
84 ),
85 )));
86 }
87 if tb.body.is_empty() {
88 return Err(RuntimeError::from(ParseRuntimeError(
89 RuntimeErrorStruct::new_with_msg_and_line_file(
90 "by enumerate finite_set: expects a body".to_string(),
91 tb.line_file.clone(),
92 ),
93 )));
94 }
95
96 let prove_block = tb.body.get_mut(0).ok_or_else(|| {
97 RuntimeError::from(ParseRuntimeError(
98 RuntimeErrorStruct::new_with_msg_and_line_file(
99 "by enumerate finite_set: expected prove block".to_string(),
100 tb.line_file.clone(),
101 ),
102 ))
103 })?;
104 if prove_block.header.get(0).map(|s| s.as_str()) != Some(PROVE) {
105 return Err(RuntimeError::from(ParseRuntimeError(
106 RuntimeErrorStruct::new_with_msg_and_line_file(
107 "by enumerate finite_set: first block must be `prove:`".to_string(),
108 prove_block.line_file.clone(),
109 ),
110 )));
111 }
112 prove_block.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
113 if prove_block.body.len() != 1 {
114 return Err(RuntimeError::from(ParseRuntimeError(
115 RuntimeErrorStruct::new_with_msg_and_line_file(
116 "by enumerate finite_set: `prove:` must contain exactly one forall fact"
117 .to_string(),
118 prove_block.line_file.clone(),
119 ),
120 )));
121 }
122
123 let forall_block = prove_block.body.get_mut(0).ok_or_else(|| {
124 RuntimeError::from(ParseRuntimeError(
125 RuntimeErrorStruct::new_with_msg_and_line_file(
126 "by enumerate finite_set: missing forall block".to_string(),
127 tb.line_file.clone(),
128 ),
129 ))
130 })?;
131 let fact = self.parse_fact(forall_block)?;
132 let forall_fact = match fact {
133 Fact::ForallFact(ff) => ff,
134 Fact::ForallFactWithIff(_) => {
135 return Err(RuntimeError::from(ParseRuntimeError(
136 RuntimeErrorStruct::new_with_msg_and_line_file(
137 "by enumerate finite_set: forall with `<=>` is not allowed here"
138 .to_string(),
139 forall_block.line_file.clone(),
140 ),
141 )));
142 }
143 _ => {
144 return Err(RuntimeError::from(ParseRuntimeError(
145 RuntimeErrorStruct::new_with_msg_and_line_file(
146 "by enumerate finite_set: `prove:` must be a single `forall` fact"
147 .to_string(),
148 forall_block.line_file.clone(),
149 ),
150 )));
151 }
152 };
153
154 for g in forall_fact.params_def_with_type.groups.iter() {
155 match &g.param_type {
156 ParamType::Obj(Obj::ListSet(_)) => {}
157 _ => {
158 return Err(RuntimeError::from(ParseRuntimeError(
159 RuntimeErrorStruct::new_with_msg_and_line_file("by enumerate finite_set: each forall parameter type must be a list set `{ ... }`"
160 .to_string(), forall_fact.line_file.clone()),
161 )));
162 }
163 }
164 }
165
166 let names = forall_fact.params_def_with_type.collect_param_names();
167 let lf = tb.line_file.clone();
168 let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
169 ParamObjType::Forall,
170 &names,
171 lf,
172 |this| {
173 tb.body
174 .iter_mut()
175 .skip(1)
176 .map(|b| this.parse_stmt(b))
177 .collect::<Result<_, _>>()
178 },
179 )?;
180
181 Ok(ByEnumerateFiniteSetStmt::new(forall_fact, proof, tb.line_file.clone()).into())
182 }
183}