1use crate::prelude::*;
2
3impl Runtime {
4 pub fn parse_fact(&mut self, tb: &mut TokenBlock) -> Result<Fact, RuntimeError> {
5 if tb.current()? == NOT
6 && tb.token_at_add_index(1) == FORALL
7 && tb.token_at_add_index(2) == "!"
8 {
9 tb.skip_token(NOT)?;
10 let fact = self.parse_inline_forall_fact(tb, false)?;
11 match fact {
12 Fact::ForallFact(forall_fact) => Ok(NotForallFact::new(forall_fact).into()),
13 _ => unreachable!("parse_inline_forall_fact only returns ForallFact"),
14 }
15 } else if tb.current()? == NOT && tb.token_at_add_index(1) == FORALL {
16 tb.skip_token(NOT)?;
17 let fact = self.parse_forall_or_forall_with_iff(tb)?;
18 match fact {
19 Fact::ForallFact(forall_fact) => Ok(NotForallFact::new(forall_fact).into()),
20 Fact::ForallFactWithIff(_) => Err(RuntimeError::from(ParseRuntimeError(
21 RuntimeErrorStruct::new_with_msg_and_line_file(
22 "not forall with <=> is not supported".to_string(),
23 tb.line_file.clone(),
24 ),
25 ))),
26 _ => unreachable!("parse_forall_or_forall_with_iff only returns forall facts"),
27 }
28 } else if tb.current()? == FORALL && tb.token_at_add_index(1) == "!" {
29 self.parse_inline_forall_fact(tb, false)
30 } else if tb.current()? == FORALL {
31 self.parse_forall_or_forall_with_iff(tb)
32 } else {
33 let or_and_spec_fact = self.parse_exist_or_and_chain_atomic_fact(tb)?;
34 Ok(or_and_spec_fact.to_fact())
35 }
36 }
37
38 pub(crate) fn parse_inline_forall_fact(
39 &mut self,
40 tb: &mut TokenBlock,
41 nested: bool,
42 ) -> Result<Fact, RuntimeError> {
43 if !tb.body.is_empty() {
44 return Err(RuntimeError::from(ParseRuntimeError(
45 RuntimeErrorStruct::new_with_msg_and_line_file(
46 format!(
47 "inline `{}` must fit on one line (no indented block); use `{}` for block syntax",
48 FORALL_BANG, FORALL
49 ),
50 tb.line_file.clone(),
51 ),
52 )));
53 }
54 self.run_in_local_parsing_time_name_scope(|this| {
55 tb.skip_token(FORALL)?;
56 if tb.current()? != "!" {
57 return Err(RuntimeError::from(ParseRuntimeError(
58 RuntimeErrorStruct::new_with_msg_and_line_file(
59 format!(
60 "expected `!` after `{}` for inline quantifier (`{}`)",
61 FORALL, FORALL_BANG
62 ),
63 tb.line_file.clone(),
64 ),
65 )));
66 }
67 tb.skip_token("!")?;
68 let mut groups: Vec<ParamGroupWithParamType> = vec![];
69 loop {
70 let cur = tb.current()?;
71 if cur == COLON || cur == RIGHT_ARROW || cur == LEFT_CURLY_BRACE {
72 break;
73 }
74 groups.push(
75 this.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Forall)?,
76 );
77 }
78 if groups.is_empty() {
79 return Err(RuntimeError::from(ParseRuntimeError(
80 RuntimeErrorStruct::new_with_msg_and_line_file(
81 format!(
82 "expected at least one parameter group after `{}`",
83 FORALL_BANG
84 ),
85 tb.line_file.clone(),
86 ),
87 )));
88 }
89 let param_def = ParamDefWithType::new(groups);
90 let forall_param_names = param_def.collect_param_names();
91 this.register_collected_param_names_for_def_parse(
92 &forall_param_names,
93 tb.line_file.clone(),
94 )?;
95 if tb.current()? == COLON {
96 tb.skip_token(COLON)?;
97 } else if tb.current()? != RIGHT_ARROW && tb.current()? != LEFT_CURLY_BRACE {
98 return Err(RuntimeError::from(ParseRuntimeError(
99 RuntimeErrorStruct::new_with_msg_and_line_file(
100 format!(
101 "after binding variables in `{}`, expected `{}`, `{}`, or `{}`",
102 FORALL_BANG, COLON, RIGHT_ARROW, LEFT_CURLY_BRACE
103 ),
104 tb.line_file.clone(),
105 ),
106 )));
107 }
108
109 let (dom_facts, then_facts) = this.parse_inline_forall_after_colon(tb)?;
110
111 this.parsing_free_param_collection
112 .end_scope(ParamObjType::Forall, &forall_param_names);
113
114 if !nested && !tb.exceed_end_of_head() {
115 return Err(RuntimeError::from(ParseRuntimeError(
116 RuntimeErrorStruct::new_with_msg_and_line_file(
117 format!("unexpected token after `{}`", FORALL_BANG),
118 tb.line_file.clone(),
119 ),
120 )));
121 }
122
123 Ok(ForallFact::new(param_def, dom_facts, then_facts, tb.line_file.clone())?.into())
124 })
125 }
126
127 fn parse_inline_forall_after_colon(
128 &mut self,
129 tb: &mut TokenBlock,
130 ) -> Result<(Vec<Fact>, Vec<ExistOrAndChainAtomicFact>), RuntimeError> {
131 if tb.exceed_end_of_head() {
132 return Err(RuntimeError::from(ParseRuntimeError(
133 RuntimeErrorStruct::new_with_msg_and_line_file(
134 format!(
135 "expected `{}`, `{{`, or body after `{}` header",
136 RIGHT_ARROW, FORALL_BANG
137 ),
138 tb.line_file.clone(),
139 ),
140 )));
141 }
142 if tb.current()? == RIGHT_ARROW {
143 tb.skip_token(RIGHT_ARROW)?;
144 let then_facts = self.parse_inline_forall_then(tb)?;
145 return Ok((vec![], then_facts));
146 }
147 if tb.current()? == LEFT_CURLY_BRACE {
148 let then_facts = self.parse_inline_forall_braced_then_list(tb)?;
149 return Ok((vec![], then_facts));
150 }
151
152 let mut dom_facts: Vec<Fact> = Vec::new();
153 loop {
154 let seg = self.parse_inline_forall_dom_segment(tb)?;
155 if tb.exceed_end_of_head() {
156 if dom_facts.is_empty() {
157 let then0 = Self::fact_as_exist_or_then(seg, tb.line_file.clone())?;
158 return Ok((vec![], vec![then0]));
159 }
160 return Err(RuntimeError::from(ParseRuntimeError(
161 RuntimeErrorStruct::new_with_msg_and_line_file(
162 format!(
163 "expected `{}` after `{}` domain facts",
164 RIGHT_ARROW, FORALL_BANG
165 ),
166 tb.line_file.clone(),
167 ),
168 )));
169 }
170 match tb.current()? {
171 COMMA => {
172 dom_facts.push(seg);
173 tb.skip_token(COMMA)?;
174 }
175 RIGHT_ARROW => {
176 dom_facts.push(seg);
177 tb.skip_token(RIGHT_ARROW)?;
178 let then_facts = self.parse_inline_forall_then(tb)?;
179 return Ok((dom_facts, then_facts));
180 }
181 _ => {
182 return Err(RuntimeError::from(ParseRuntimeError(
183 RuntimeErrorStruct::new_with_msg_and_line_file(
184 format!(
185 "expected `,`, `{}`, or end of line after `{}` domain fact",
186 RIGHT_ARROW, FORALL_BANG
187 ),
188 tb.line_file.clone(),
189 ),
190 )));
191 }
192 }
193 }
194 }
195
196 fn parse_inline_forall_dom_segment(
197 &mut self,
198 tb: &mut TokenBlock,
199 ) -> Result<Fact, RuntimeError> {
200 if tb.current()? == NOT
201 && tb.token_at_add_index(1) == FORALL
202 && tb.token_at_add_index(2) == "!"
203 {
204 tb.skip_token(NOT)?;
205 let fact = self.parse_inline_forall_fact(tb, true)?;
206 match fact {
207 Fact::ForallFact(ff) => Ok(NotForallFact::new(ff).into()),
208 _ => unreachable!("parse_inline_forall_fact only returns ForallFact"),
209 }
210 } else if tb.current()? == FORALL && tb.token_at_add_index(1) == "!" {
211 self.parse_inline_forall_fact(tb, true)
212 } else if tb.current()? == NOT && tb.token_at_add_index(1) == FORALL {
213 Err(RuntimeError::from(ParseRuntimeError(
214 RuntimeErrorStruct::new_with_msg_and_line_file(
215 format!(
216 "`not {}` in `{}` domain is not supported (requires a block); use `not {}` or a separate line",
217 FORALL, FORALL_BANG, FORALL_BANG
218 ),
219 tb.line_file.clone(),
220 ),
221 )))
222 } else if tb.current()? == FORALL {
223 Err(RuntimeError::from(ParseRuntimeError(
224 RuntimeErrorStruct::new_with_msg_and_line_file(
225 format!(
226 "block `{}` is not allowed inside `{}` domain; use `{}` or move to a multi-line `{}` block",
227 FORALL, FORALL_BANG, FORALL_BANG, FORALL
228 ),
229 tb.line_file.clone(),
230 ),
231 )))
232 } else {
233 let e = self.parse_exist_or_and_chain_atomic_fact(tb)?;
234 Ok(e.to_fact())
235 }
236 }
237
238 fn parse_inline_forall_then(
239 &mut self,
240 tb: &mut TokenBlock,
241 ) -> Result<Vec<ExistOrAndChainAtomicFact>, RuntimeError> {
242 Self::reject_inline_forall_in_then(tb)?;
243 if tb.current()? == LEFT_CURLY_BRACE {
244 return self.parse_inline_forall_braced_then_list(tb);
245 }
246 Ok(vec![self.parse_exist_or_and_chain_atomic_fact(tb)?])
247 }
248
249 fn parse_inline_forall_braced_then_list(
250 &mut self,
251 tb: &mut TokenBlock,
252 ) -> Result<Vec<ExistOrAndChainAtomicFact>, RuntimeError> {
253 tb.skip_token(LEFT_CURLY_BRACE)?;
254 let mut facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
255 loop {
256 Self::reject_inline_forall_in_then(tb)?;
257 facts.push(self.parse_exist_or_and_chain_atomic_fact(tb)?);
258 if tb.current()? != RIGHT_CURLY_BRACE {
259 tb.skip_token(COMMA)?;
260 } else {
261 break;
262 }
263 }
264 tb.skip_token(RIGHT_CURLY_BRACE)?;
265 Ok(facts)
266 }
267
268 fn reject_inline_forall_in_then(tb: &TokenBlock) -> Result<(), RuntimeError> {
269 if tb.exceed_end_of_head() {
270 return Err(RuntimeError::from(ParseRuntimeError(
271 RuntimeErrorStruct::new_with_msg_and_line_file(
272 format!("unexpected end of tokens in `{}` `then`", FORALL_BANG),
273 tb.line_file.clone(),
274 ),
275 )));
276 }
277 if (tb.current()? == FORALL && tb.token_at_add_index(1) == "!")
278 || (tb.current()? == NOT
279 && tb.token_at_add_index(1) == FORALL
280 && tb.token_at_add_index(2) == "!")
281 {
282 return Err(RuntimeError::from(ParseRuntimeError(
283 RuntimeErrorStruct::new_with_msg_and_line_file(
284 format!(
285 "`{}` is not allowed in the `then` part of another `{}`",
286 FORALL_BANG, FORALL_BANG
287 ),
288 tb.line_file.clone(),
289 ),
290 )));
291 }
292 Ok(())
293 }
294
295 fn fact_as_exist_or_then(
296 f: Fact,
297 line_file: LineFile,
298 ) -> Result<ExistOrAndChainAtomicFact, RuntimeError> {
299 match f {
300 Fact::AtomicFact(a) => Ok(ExistOrAndChainAtomicFact::AtomicFact(a)),
301 Fact::ExistFact(e) => Ok(ExistOrAndChainAtomicFact::ExistFact(e)),
302 Fact::OrFact(o) => Ok(ExistOrAndChainAtomicFact::OrFact(o)),
303 Fact::AndFact(a) => Ok(ExistOrAndChainAtomicFact::AndFact(a)),
304 Fact::ChainFact(c) => Ok(ExistOrAndChainAtomicFact::ChainFact(c)),
305 Fact::ForallFact(_) | Fact::ForallFactWithIff(_) | Fact::NotForall(_) => {
306 Err(RuntimeError::from(ParseRuntimeError(
307 RuntimeErrorStruct::new_with_msg_and_line_file(
308 format!(
309 "`{}` without `{}` must end with one chain/atomic-style fact",
310 FORALL_BANG, RIGHT_ARROW
311 ),
312 line_file,
313 ),
314 )))
315 }
316 }
317 }
318
319 fn parse_forall_or_forall_with_iff(
321 &mut self,
322 tb: &mut TokenBlock,
323 ) -> Result<Fact, RuntimeError> {
324 self.run_in_local_parsing_time_name_scope(|this| {
325 tb.skip_token(FORALL)?;
326 let mut groups: Vec<ParamGroupWithParamType> = vec![];
327 while tb.current()? != COLON {
328 groups.push(
329 this.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Forall)?,
330 );
331 }
332 let param_def = ParamDefWithType::new(groups);
333 let forall_param_names = param_def.collect_param_names();
334 this.register_collected_param_names_for_def_parse(
335 &forall_param_names,
336 tb.line_file.clone(),
337 )?;
338 tb.skip_token(COLON)?;
339
340 let last_is_equiv = {
341 let last_body = tb.body.last().ok_or_else(|| {
342 RuntimeError::from(ParseRuntimeError(
343 RuntimeErrorStruct::new_with_msg_and_line_file(
344 "Expected body".to_string(),
345 tb.line_file.clone(),
346 ),
347 ))
348 })?;
349 last_body.current()? == EQUIVALENT_SIGN
350 };
351 let fact_result = if last_is_equiv {
352 this.parse_forall_with_iff(tb, param_def)
353 } else {
354 this.parse_forall(tb, param_def)
355 };
356 this.parsing_free_param_collection
357 .end_scope(ParamObjType::Forall, &forall_param_names);
358 fact_result
359 })
360 }
361
362 fn parse_forall_with_iff(
363 &mut self,
364 tb: &mut TokenBlock,
365 param_def: ParamDefWithType,
366 ) -> Result<Fact, RuntimeError> {
367 if tb.body.len() < 2 {
368 return Err(RuntimeError::from(ParseRuntimeError(
369 RuntimeErrorStruct::new_with_msg_and_line_file(
370 "Expected at least 2 body blocks".to_string(),
371 tb.line_file.clone(),
372 ),
373 )));
374 }
375
376 let mut dom_facts: Vec<Fact> = Vec::new();
377 let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
378 let mut iff_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
379
380 let body_len = tb.body.len();
381
382 let iff_block = tb.body.get_mut(body_len - 1).ok_or_else(|| {
383 RuntimeError::from(ParseRuntimeError(
384 RuntimeErrorStruct::new_with_msg_and_line_file(
385 "Expected <=>: block in forall body".to_string(),
386 tb.line_file.clone(),
387 ),
388 ))
389 })?;
390 iff_block.skip_token_and_colon_and_exceed_end_of_head(EQUIVALENT_SIGN)?;
391 for block in iff_block.body.iter_mut() {
392 iff_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
393 }
394
395 let then_block = tb.body.get_mut(body_len - 2).ok_or_else(|| {
396 RuntimeError::from(ParseRuntimeError(
397 RuntimeErrorStruct::new_with_msg_and_line_file(
398 "Expected =>: block in forall body".to_string(),
399 tb.line_file.clone(),
400 ),
401 ))
402 })?;
403 then_block.skip_token_and_colon_and_exceed_end_of_head(RIGHT_ARROW)?;
404 for block in then_block.body.iter_mut() {
405 then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
406 }
407
408 for block in tb.body.iter_mut().take(body_len - 2) {
409 dom_facts.push(self.parse_fact(block)?);
410 }
411
412 let forall_fact = ForallFact::new(param_def, dom_facts, then_facts, tb.line_file.clone())?;
413
414 Ok(ForallFactWithIff::new(forall_fact, iff_facts, tb.line_file.clone())?.into())
415 }
416
417 fn parse_forall(
418 &mut self,
419 tb: &mut TokenBlock,
420 param_def: ParamDefWithType,
421 ) -> Result<Fact, RuntimeError> {
422 let last_body = tb.body.last().ok_or_else(|| {
423 RuntimeError::from(ParseRuntimeError(
424 RuntimeErrorStruct::new_with_msg_and_line_file(
425 "Expected body".to_string(),
426 tb.line_file.clone(),
427 ),
428 ))
429 })?;
430 if last_body.current()? == RIGHT_ARROW {
431 let mut dom_facts: Vec<Fact> = vec![];
432 let n = tb.body.len();
433 for block in tb.body.iter_mut().take(n - 1) {
434 dom_facts.push(self.parse_fact(block)?);
435 }
436 let last = tb.body.last_mut().ok_or_else(|| {
437 RuntimeError::from(ParseRuntimeError(
438 RuntimeErrorStruct::new_with_msg_and_line_file(
439 "Expected body".to_string(),
440 tb.line_file.clone(),
441 ),
442 ))
443 })?;
444 last.skip_token_and_colon_and_exceed_end_of_head(RIGHT_ARROW)?;
445 let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
446 for block in last.body.iter_mut() {
447 then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
448 }
449 Ok(ForallFact::new(param_def, dom_facts, then_facts, tb.line_file.clone())?.into())
450 } else {
451 let mut then_facts: Vec<ExistOrAndChainAtomicFact> = Vec::new();
452 for block in tb.body.iter_mut() {
453 then_facts.push(self.parse_exist_or_and_chain_atomic_fact(block)?);
454 }
455 Ok(ForallFact::new(param_def, vec![], then_facts, tb.line_file.clone())?.into())
456 }
457 }
458
459 pub fn parse_and_chain_atomic_fact(
461 &mut self,
462 tb: &mut TokenBlock,
463 ) -> Result<AndChainAtomicFact, RuntimeError> {
464 let first = self.parse_chain_atomic(tb, true)?;
465
466 match first {
468 ChainAtomicFact::ChainFact(c) => return Ok(AndChainAtomicFact::ChainFact(c)),
469 ChainAtomicFact::AtomicFact(a) => {
470 let mut collected: Vec<AtomicFact> = vec![a];
471 while !tb.exceed_end_of_head() && tb.current()? == AND {
472 tb.skip_token(AND)?;
473 let next = self.parse_atomic_fact(tb, true)?;
474 collected.push(next);
475 }
476 if collected.len() == 1 {
477 return Ok(AndChainAtomicFact::AtomicFact(collected.remove(0)));
478 }
479 Ok(AndChainAtomicFact::AndFact(AndFact::new(
480 collected,
481 tb.line_file.clone(),
482 )))
483 }
484 }
485 }
486
487 pub fn parse_exist_fact(&mut self, tb: &mut TokenBlock) -> Result<ExistFactEnum, RuntimeError> {
488 self.run_in_local_parsing_time_name_scope(|this| {
489 let is_exist_unique = if tb.current()? == EXIST {
490 tb.skip_token(EXIST)?;
491 if tb.current()? == "!" {
492 tb.skip_token("!")?;
493 true
494 } else {
495 false
496 }
497 } else {
498 return Err(RuntimeError::from(ParseRuntimeError(
499 RuntimeErrorStruct::new_with_msg_and_line_file(
500 format!(
501 "expected `{}` or `{}` at start of exist fact",
502 EXIST, EXIST_BANG
503 ),
504 tb.line_file.clone(),
505 ),
506 )));
507 };
508 let mut groups: Vec<ParamGroupWithParamType> = vec![];
509 while tb.current()? != ST {
510 groups.push(
511 this.parse_param_def_with_param_type_and_skip_comma(tb, ParamObjType::Exist)?,
512 );
513 }
514 let param_def = ParamDefWithType::new(groups);
515 let exist_param_names = param_def.collect_param_names();
516 this.run_in_local_parsing_time_name_scope(move |inner| {
517 inner.register_collected_param_names_for_def_parse(
518 &exist_param_names,
519 tb.line_file.clone(),
520 )?;
521 let fact_result = (|| {
522 tb.skip_token(ST)?;
523
524 tb.skip_token(LEFT_CURLY_BRACE)?;
525
526 let mut facts: Vec<ExistBodyFact> = vec![];
527 loop {
528 facts.push(inner.parse_exist_body_fact(tb)?);
529 if tb.current()? != RIGHT_CURLY_BRACE {
530 tb.skip_token(COMMA)?;
531 } else {
532 break;
533 }
534 }
535 tb.skip_token(RIGHT_CURLY_BRACE)?;
536
537 let line_file = tb.line_file.clone();
538 let body = ExistFactBody::new(param_def, facts, line_file)?;
539 Ok(if is_exist_unique {
540 ExistFactEnum::ExistUniqueFact(body)
541 } else {
542 ExistFactEnum::ExistFact(body)
543 })
544 })();
545 inner
546 .parsing_free_param_collection
547 .end_scope(ParamObjType::Exist, &exist_param_names);
548 fact_result
549 })
550 })
551 }
552
553 fn parse_exist_body_fact(
554 &mut self,
555 tb: &mut TokenBlock,
556 ) -> Result<ExistBodyFact, RuntimeError> {
557 if tb.current()? == FORALL && tb.token_at_add_index(1) == "!" {
558 let fact = self.parse_inline_forall_fact(tb, true)?;
559 match fact {
560 Fact::ForallFact(forall_fact) => Ok(ExistBodyFact::InlineForall(forall_fact)),
561 _ => unreachable!("parse_inline_forall_fact only returns ForallFact"),
562 }
563 } else {
564 Ok(self.parse_or_and_chain_atomic_fact(tb)?.into())
565 }
566 }
567
568 pub fn parse_facts_in_body(&mut self, tb: &mut TokenBlock) -> Result<Vec<Fact>, RuntimeError> {
569 let mut facts: Vec<Fact> = vec![];
570 for block in tb.body.iter_mut() {
571 facts.push(self.parse_fact(block)?);
572 }
573 Ok(facts)
574 }
575
576 pub fn parse_exist_or_and_chain_atomic_fact(
577 &mut self,
578 tb: &mut TokenBlock,
579 ) -> Result<ExistOrAndChainAtomicFact, RuntimeError> {
580 match tb.current()? {
581 EXIST => {
582 let exist_fact = self.parse_exist_fact(tb)?;
583 Ok(ExistOrAndChainAtomicFact::ExistFact(exist_fact))
584 }
585 NOT => {
586 if tb.token_at_add_index(1) == EXIST {
587 if tb.token_at_add_index(2) == "!" {
588 return Err(RuntimeError::from(ParseRuntimeError(
589 RuntimeErrorStruct::new_with_msg_and_line_file(
590 format!("`{} {}` is not supported", NOT, EXIST_BANG),
591 tb.line_file.clone(),
592 ),
593 )));
594 }
595 tb.skip_token(NOT)?;
596 let exist_fact = self.parse_exist_fact(tb)?;
597 return Ok(ExistOrAndChainAtomicFact::ExistFact(match exist_fact {
598 ExistFactEnum::ExistFact(body) => ExistFactEnum::NotExistFact(body),
599 ExistFactEnum::ExistUniqueFact(_) | ExistFactEnum::NotExistFact(_) => {
600 unreachable!("`not exist` parse should only produce plain exist body")
601 }
602 }));
603 }
604 let first = self.parse_and_chain_atomic_fact_allow_leading_not(tb)?;
605 let mut list: Vec<AndChainAtomicFact> = vec![first];
606 while !tb.exceed_end_of_head() && tb.current()? == OR {
607 tb.skip_token(OR)?;
608 list.push(self.parse_and_chain_atomic_fact_allow_leading_not(tb)?);
609 }
610 if list.len() == 1 {
611 return Ok(match list.remove(0) {
612 AndChainAtomicFact::AtomicFact(a) => {
613 ExistOrAndChainAtomicFact::AtomicFact(a)
614 }
615 AndChainAtomicFact::AndFact(a) => ExistOrAndChainAtomicFact::AndFact(a),
616 AndChainAtomicFact::ChainFact(c) => ExistOrAndChainAtomicFact::ChainFact(c),
617 });
618 }
619 Ok(ExistOrAndChainAtomicFact::OrFact(OrFact::new(
620 list,
621 tb.line_file.clone(),
622 )))
623 }
624 FORALL => {
625 return Err(RuntimeError::from(ParseRuntimeError(
626 RuntimeErrorStruct::new_with_msg_and_line_file(
627 "Expected exist or and chain atomic fact".to_string(),
628 tb.line_file.clone(),
629 ),
630 )));
631 }
632 _ => Ok(self.parse_or_and_chain_atomic_fact(tb)?.into()),
633 }
634 }
635
636 pub fn parse_atomic_fact(
638 &mut self,
639 tb: &mut TokenBlock,
640 is_true: bool,
641 ) -> Result<AtomicFact, RuntimeError> {
642 if tb.current()? == NOT {
643 tb.skip_token(NOT)?;
644 return Ok(self.parse_atomic_fact(tb, !is_true)?);
645 }
646
647 let line_file = tb.line_file.clone();
648 if tb.current()? == FACT_PREFIX {
649 tb.skip_token(FACT_PREFIX)?;
650 let prop = self.parse_predicate(tb)?;
651 let args = self.parse_braced_objs(tb)?;
652 let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
653 |e: RuntimeError| {
654 let msg = match &e {
655 RuntimeError::NewFactError(s) => s.msg.clone(),
656 _ => "parse atomic fact".to_string(),
657 };
658 RuntimeError::from(ParseRuntimeError(
659 RuntimeErrorStruct::new_with_msg_and_line_file(msg, tb.line_file.clone()),
660 ))
661 },
662 )?;
663 return Ok(atomic);
664 }
665 let first_obj = self.parse_obj(tb)?;
666 if tb.exceed_end_of_head() {
667 return Err(RuntimeError::from(ParseRuntimeError(
668 RuntimeErrorStruct::new_with_msg_and_line_file(
669 "Expected operator or $prop in atomic fact".to_string(),
670 tb.line_file.clone(),
671 ),
672 )));
673 }
674 let tok = tb.current()?.to_string();
675 let prop = if is_comparison_str(&tok) {
676 tb.advance()?;
677 AtomicName::WithoutMod(tok.clone())
678 } else if tok == FACT_PREFIX {
679 tb.skip_token(FACT_PREFIX)?;
680 self.parse_predicate(tb)?
681 } else {
682 return Err(RuntimeError::from(ParseRuntimeError(
683 RuntimeErrorStruct::new_with_msg_and_line_file(
684 "Expected operator or $prop in atomic fact".to_string(),
685 tb.line_file.clone(),
686 ),
687 )));
688 };
689 let next_obj = self.parse_obj(tb)?;
690 let args = vec![first_obj, next_obj];
691 let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
692 |e: RuntimeError| {
693 let msg = match &e {
694 RuntimeError::NewFactError(s) => s.msg.clone(),
695 _ => "parse atomic fact".to_string(),
696 };
697 RuntimeError::from(ParseRuntimeError(
698 RuntimeErrorStruct::new_with_msg_and_line_file(msg, tb.line_file.clone()),
699 ))
700 },
701 )?;
702 Ok(atomic)
703 }
704
705 pub fn parse_and_chain_atomic_fact_allow_leading_not(
711 &mut self,
712 tb: &mut TokenBlock,
713 ) -> Result<AndChainAtomicFact, RuntimeError> {
714 if tb.current()? == NOT {
715 tb.skip_token(NOT)?;
716 let a = self.parse_atomic_fact(tb, false)?;
717 return Ok(AndChainAtomicFact::AtomicFact(a));
718 }
719 self.parse_and_chain_atomic_fact(tb)
720 }
721
722 pub fn parse_or_and_chain_atomic_fact(
723 &mut self,
724 tb: &mut TokenBlock,
725 ) -> Result<OrAndChainAtomicFact, RuntimeError> {
726 let first = self.parse_and_chain_atomic_fact_allow_leading_not(tb)?;
727 let mut list: Vec<AndChainAtomicFact> = vec![first];
728 while !tb.exceed_end_of_head() && tb.current()? == OR {
729 tb.skip_token(OR)?;
730 list.push(self.parse_and_chain_atomic_fact_allow_leading_not(tb)?);
731 }
732 if list.len() == 1 {
733 return Ok(match list.remove(0) {
734 AndChainAtomicFact::AtomicFact(a) => OrAndChainAtomicFact::AtomicFact(a),
735 AndChainAtomicFact::AndFact(a) => OrAndChainAtomicFact::AndFact(a),
736 AndChainAtomicFact::ChainFact(c) => OrAndChainAtomicFact::ChainFact(c),
737 });
738 }
739 Ok(OrAndChainAtomicFact::OrFact(OrFact::new(
740 list,
741 tb.line_file.clone(),
742 )))
743 }
744
745 pub fn parse_chain_atomic(
747 &mut self,
748 tb: &mut TokenBlock,
749 is_true: bool,
750 ) -> Result<ChainAtomicFact, RuntimeError> {
751 let line_file = tb.line_file.clone();
752 if tb.current()? == FACT_PREFIX {
753 tb.skip_token(FACT_PREFIX)?;
754 let prop = self.parse_predicate(tb)?;
755 let args = self.parse_braced_objs(tb)?;
756 let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
757 |e: RuntimeError| {
758 let msg = match &e {
759 RuntimeError::NewFactError(s) => s.msg.clone(),
760 _ => "parse atomic fact".to_string(),
761 };
762 RuntimeError::from(ParseRuntimeError(
763 RuntimeErrorStruct::new_with_msg_and_line_file(msg, tb.line_file.clone()),
764 ))
765 },
766 )?;
767 return Ok(ChainAtomicFact::AtomicFact(atomic));
768 }
769 let first_obj = self.parse_obj(tb)?;
770 let mut objs: Vec<Obj> = vec![first_obj];
771 let mut prop_names: Vec<AtomicName> = vec![];
772 while !tb.exceed_end_of_head() {
773 let tok = tb.current()?.to_string();
774 let prop = if is_comparison_str(&tok) {
775 tb.advance()?;
776 AtomicName::WithoutMod(tok.clone())
777 } else if tok == FACT_PREFIX {
778 tb.skip_token(FACT_PREFIX)?;
779 self.parse_predicate(tb)?
780 } else {
781 break;
782 };
783 let next_obj = self.parse_obj(tb)?;
784 prop_names.push(prop);
785 objs.push(next_obj);
786 }
787 if prop_names.is_empty() {
788 return Err(RuntimeError::from(ParseRuntimeError(
789 RuntimeErrorStruct::new_with_msg_and_line_file(
790 "Expected operator or $prop in fact".to_string(),
791 tb.line_file.clone(),
792 ),
793 )));
794 }
795 if !is_true && (objs.len() > 2 || prop_names.len() > 1) {
796 return Err(RuntimeError::from(ParseRuntimeError(
797 RuntimeErrorStruct::new_with_msg_and_line_file(
798 "Negated fact must be single atomic (one operator)".to_string(),
799 tb.line_file.clone(),
800 ),
801 )));
802 }
803 if objs.len() == 2 && prop_names.len() == 1 {
804 let prop = prop_names.remove(0);
805 let args = objs;
806 let atomic = AtomicFact::to_atomic_fact(prop, is_true, args, line_file).map_err(
807 |e: RuntimeError| {
808 let msg = match &e {
809 RuntimeError::NewFactError(s) => s.msg.clone(),
810 _ => "parse atomic fact".to_string(),
811 };
812 RuntimeError::from(ParseRuntimeError(
813 RuntimeErrorStruct::new_with_msg_and_line_file(msg, tb.line_file.clone()),
814 ))
815 },
816 )?;
817 return Ok(ChainAtomicFact::AtomicFact(atomic));
818 }
819 Ok(ChainAtomicFact::ChainFact(ChainFact::new(
820 objs, prop_names, line_file,
821 )))
822 }
823}
824
825#[cfg(test)]
826mod inline_forall_parse_tests {
827 use crate::parse::TokenBlock;
828 use crate::prelude::*;
829 use std::rc::Rc;
830
831 fn parse_one_fact_line(line: &str) -> Result<Fact, RuntimeError> {
832 let mut rt = Runtime::new();
833 let mut blocks = TokenBlock::parse_blocks(line, Rc::from("test.lit"))?;
834 assert_eq!(blocks.len(), 1, "{line:?}");
835 rt.parse_fact(&mut blocks[0])
836 }
837
838 #[test]
839 fn inline_forall_single_then_without_arrow() {
840 let f = parse_one_fact_line("forall! x R: x > 0").unwrap();
841 let Fact::ForallFact(ff) = f else {
842 panic!("expected ForallFact");
843 };
844 assert!(ff.dom_facts.is_empty());
845 assert_eq!(ff.then_facts.len(), 1);
846 }
847
848 #[test]
849 fn inline_forall_no_colon_before_arrow_when_no_dom() {
850 let f = parse_one_fact_line("forall! x R => { x > 0 }").unwrap();
851 let Fact::ForallFact(ff) = f else {
852 panic!("expected ForallFact");
853 };
854 assert!(ff.dom_facts.is_empty());
855 assert_eq!(ff.then_facts.len(), 1);
856 }
857
858 #[test]
859 fn inline_forall_no_colon_braced_then_when_no_dom() {
860 let f = parse_one_fact_line("forall! x R { x > 0, x + 1 > 1 }").unwrap();
861 let Fact::ForallFact(ff) = f else {
862 panic!("expected ForallFact");
863 };
864 assert!(ff.dom_facts.is_empty());
865 assert_eq!(ff.then_facts.len(), 2);
866 }
867
868 #[test]
869 fn inline_forall_dom_arrow_then() {
870 let f = parse_one_fact_line("forall! x R: x > 0 => { x >= 0 }").unwrap();
871 let Fact::ForallFact(ff) = f else {
872 panic!("expected ForallFact");
873 };
874 assert_eq!(ff.dom_facts.len(), 1);
875 assert_eq!(ff.then_facts.len(), 1);
876 }
877
878 #[test]
879 fn inline_forall_empty_dom_arrow() {
880 let f = parse_one_fact_line("forall! x R: => { x > 0 }").unwrap();
881 let Fact::ForallFact(ff) = f else {
882 panic!("expected ForallFact");
883 };
884 assert!(ff.dom_facts.is_empty());
885 assert_eq!(ff.then_facts.len(), 1);
886 }
887
888 #[test]
889 fn inline_forall_nested_in_dom() {
890 let f = parse_one_fact_line("forall! x R: forall! y R: y > 0 => { x > y } => { x > 0 }")
891 .unwrap();
892 let Fact::ForallFact(ff) = f else {
893 panic!("expected ForallFact");
894 };
895 assert_eq!(ff.dom_facts.len(), 1);
896 assert!(matches!(&ff.dom_facts[0], Fact::ForallFact(_)));
897 assert_eq!(ff.then_facts.len(), 1);
898 }
899
900 #[test]
901 fn inline_forall_braced_then() {
902 let f = parse_one_fact_line("forall! x R: x > 0 => { x >= 0, x + 1 > 0 }").unwrap();
903 let Fact::ForallFact(ff) = f else {
904 panic!("expected ForallFact");
905 };
906 assert_eq!(ff.dom_facts.len(), 1);
907 assert_eq!(ff.then_facts.len(), 2);
908 }
909
910 #[test]
911 fn inline_forall_no_dom_braced_then() {
912 let f = parse_one_fact_line("forall! x R: { x > 0, x + 1 > 1 }").unwrap();
913 let Fact::ForallFact(ff) = f else {
914 panic!("expected ForallFact");
915 };
916 assert!(ff.dom_facts.is_empty());
917 assert_eq!(ff.then_facts.len(), 2);
918 }
919
920 #[test]
921 fn not_inline_forall_parses_as_not_forall() {
922 let f = parse_one_fact_line("not forall! x R: x > 0 => { x + 1 > 1 }").unwrap();
923 assert!(matches!(f, Fact::NotForall(_)));
924 }
925
926 #[test]
927 fn inline_forall_then_may_not_contain_inline_forall() {
928 let err = parse_one_fact_line("forall! x R: x > 0 => { forall! y R: y > 0 => { y > x } }")
929 .unwrap_err();
930 let RuntimeError::ParseError(s) = err else {
931 panic!("expected parse error, got {err:?}");
932 };
933 assert!(s.msg.contains("then"), "{}", s.msg);
934 }
935}