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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

use crate::prelude::*;

impl Runtime {
    pub fn verify_exist_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: &ExistOrAndChainAtomicFact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeErrorStruct> {
        let stmt_for_fact_errors: Stmt = fact.clone().to_fact().into();
        self.verify_exist_or_and_chain_atomic_fact_well_defined(fact, verify_state)
            .map_err(|well_defined_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    stmt_for_fact_errors.clone(),
                    "".to_string(),
                    Some(well_defined_error.into()),
                    vec![],
                )
            })?;
        self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
            fact.clone(),
        )
        .map_err(|store_fact_error| {
            RuntimeErrorStruct::exec_stmt_new_with_stmt(
                stmt_for_fact_errors,
                "".to_string(),
                Some(store_fact_error.into()),
                vec![],
            )
        })
    }

    pub fn verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: &OrAndChainAtomicFact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeErrorStruct> {
        let stmt_for_fact_errors: Stmt = fact.clone().to_fact().into();
        self.verify_or_and_chain_atomic_fact_well_defined(fact, verify_state)
            .map_err(|well_defined_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    stmt_for_fact_errors.clone(),
                    "".to_string(),
                    Some(well_defined_error.into()),
                    vec![],
                )
            })?;
        self.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(fact.clone())
            .map_err(|store_fact_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    stmt_for_fact_errors,
                    "".to_string(),
                    Some(store_fact_error.into()),
                    vec![],
                )
            })
    }

    pub fn verify_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: Fact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeErrorStruct> {
        let stmt_for_fact_errors: Stmt = fact.clone().into();
        self.verify_fact_well_defined(&fact, verify_state)
            .map_err(|well_defined_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    stmt_for_fact_errors.clone(),
                    "".to_string(),
                    Some(well_defined_error.into()),
                    vec![],
                )
            })?;
        self.store_fact_without_well_defined_verified_and_infer(fact)
            .map_err(|store_fact_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    stmt_for_fact_errors,
                    "".to_string(),
                    Some(store_fact_error.into()),
                    vec![],
                )
            })
    }
}