Skip to main content

litex/parse/
parse_know_stmt.rs

1use 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}