litex/parse/
parse_know_stmt.rs1use crate::prelude::*;
2
3impl Runtime {
4 pub fn parse_know_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
5 tb.skip_token(KNOW)?;
6 if tb.current_token_is_equal_to(COLON) {
7 tb.skip_token(COLON)?;
8 let facts = self.parse_facts_in_body(tb)?;
9 return Ok(KnowStmt::new(facts, tb.line_file.clone()).into());
10 } else if tb.current_token_is_equal_to(FORALL) {
11 let fact = self.parse_fact(tb)?;
12 return Ok(KnowStmt::new(vec![fact], tb.line_file.clone()).into());
13 } else if tb.current_token_is_equal_to(NOT) {
14 if tb.token_at_add_index(1) == FORALL {
15 let fact = self.parse_fact(tb)?;
16 return Ok(KnowStmt::new(vec![fact], tb.line_file.clone()).into());
17 }
18 }
19
20 let mut facts: Vec<Fact> = vec![];
21 loop {
22 let o = self.parse_exist_or_and_chain_atomic_fact(tb)?;
23 facts.push(o.to_fact());
24
25 if tb.exceed_end_of_head() {
26 break;
27 }
28 tb.skip_token(COMMA)?;
29 }
30 Ok(KnowStmt::new(facts, tb.line_file.clone()).into())
31 }
32}