litex-lang 0.9.6-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

use crate::prelude::*;

impl Runtime {
    pub fn parse_know_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
        tb.skip_token(KNOW)?;
        if tb.current_token_is_equal_to(COLON) {
            tb.skip_token(COLON)?;
            let facts = self.parse_facts_in_body(tb)?;
            Ok(KnowStmt::new(facts, tb.line_file.clone()).into())
        } else if tb.current_token_is_equal_to(FORALL) {
            let fact = self.parse_fact(tb)?;
            Ok(KnowStmt::new(vec![fact], tb.line_file.clone()).into())
        } else {
            let mut facts: Vec<Fact> = vec![];
            loop {
                let o = self.parse_exist_or_and_chain_atomic_fact(tb)?;
                facts.push(o.to_fact());

                if tb.exceed_end_of_head() {
                    break;
                }
                tb.skip_token(COMMA)?;
            }
            Ok(KnowStmt::new(facts, tb.line_file.clone()).into())
        }
    }
}