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 {
    /// Dispatch infer by atomic fact type.
    /// Example: `x $in S` enters membership infer.
    pub(crate) fn infer_atomic_fact(
        &mut self,
        atomic_fact: &AtomicFact,
    ) -> Result<InferResult, RuntimeError> {
        match atomic_fact {
            AtomicFact::EqualFact(equal_fact) => self.infer_equal_fact(equal_fact),
            AtomicFact::InFact(in_fact) => self.infer_in_fact(in_fact),
            AtomicFact::NormalAtomicFact(normal_atomic_fact) => {
                self.infer_normal_atomic_fact(normal_atomic_fact)
            }
            AtomicFact::SubsetFact(subset_fact) => self.infer_subset_fact(subset_fact),
            AtomicFact::SupersetFact(superset_fact) => self.infer_superset_fact(superset_fact),
            AtomicFact::LessFact(_)
            | AtomicFact::GreaterFact(_)
            | AtomicFact::LessEqualFact(_)
            | AtomicFact::GreaterEqualFact(_) => {
                self.infer_numeric_order_sign_from_order_atomic(atomic_fact)
            }
            _ => Ok(InferResult::new()),
        }
    }
}