litex-lang 0.9.86-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

use crate::prelude::*;

impl Runtime {
    /// If the fact string is in the known-facts cache, return the cached verification result.
    pub fn verify_fact_from_cache_using_display_string(&self, fact: &Fact) -> Option<StmtResult> {
        let key = fact.to_string();
        let (cache_ok, cite_fact_source) = self.cache_known_facts_contains(&key);
        if cache_ok {
            Some(
                (FactualStmtSuccess::new_with_verified_by_known_fact(
                    fact.clone(),
                    VerifiedByResult::cached_fact(fact.clone(), cite_fact_source),
                    Vec::new(),
                ))
                .into(),
            )
        } else {
            None
        }
    }

    /// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
    pub fn verify_param_type_nonempty_if_required(
        &mut self,
        param_type: &ParamType,
        check_type_nonempty: bool,
    ) -> Result<(), RuntimeError> {
        if !check_type_nonempty {
            return Ok(());
        }
        match param_type {
            ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
            ParamType::Obj(param_set) => match param_set {
                Obj::FnSet(fn_set) => {
                    let ret_nonempty = IsNonemptySetFact::new(
                        fn_set.body.ret_set.as_ref().clone(),
                        default_line_file(),
                    )
                    .into();
                    self.verify_fact_well_defined_and_store_and_infer(
                        ret_nonempty,
                        &VerifyState::new(2, false),
                    )?;
                    Ok(())
                }
                Obj::AnonymousFn(anon) => {
                    let ret_nonempty = IsNonemptySetFact::new(
                        anon.body.ret_set.as_ref().clone(),
                        default_line_file(),
                    )
                    .into();
                    self.verify_fact_well_defined_and_store_and_infer(
                        ret_nonempty,
                        &VerifyState::new(2, false),
                    )?;
                    Ok(())
                }
                _ => {
                    let nonempty_fact =
                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
                    let ret =
                        self.verify_fact(&nonempty_fact.into(), &VerifyState::new(0, false))?;
                    if ret.is_unknown() {
                        return Err(RuntimeError::from(VerifyRuntimeError(
                            RuntimeErrorStruct::new_with_just_msg(
                                "param type is not nonempty".to_string(),
                            ),
                        )));
                    }
                    Ok(())
                }
            },
        }
    }
}