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

use crate::prelude::*;

impl Runtime {
    pub fn exec_def_family_stmt(
        &mut self,
        def_family_stmt: &DefFamilyStmt,
    ) -> Result<StmtResult, RuntimeErrorStruct> {
        let family_definition_infer_result = self.run_in_local_env(|rt| {
            rt.def_family_stmt_check_well_defined(def_family_stmt)
        })?;

        self.store_def_family(def_family_stmt)
            .map_err(|store_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    def_family_stmt.clone().into(),
                    "failed to store family definition".to_string(),
                    Some(store_error.into()),
                    vec![],
                )
            })?;

        Ok((NonFactualStmtSuccess::new(
                def_family_stmt.clone().into(),
                family_definition_infer_result,
                vec![],
            )).into())
    }

    fn def_family_stmt_check_well_defined(
        &mut self,
        def_family_stmt: &DefFamilyStmt,
    ) -> Result<InferResult, RuntimeErrorStruct> {
        let verify_state = VerifyState::new(0, false);
        let mut family_definition_infer_result = self
            .define_params_with_type(&def_family_stmt.params_def_with_type, false)
            .map_err(|define_params_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    def_family_stmt.clone().into(),
                    "".to_string(),
                    Some(define_params_error),
                    vec![],
                )
            })?;

        for dom_fact in def_family_stmt.dom_facts.iter() {
            let dom_fact_infer_result = self
                .verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
                    dom_fact,
                    &verify_state,
                )
                .map_err(|inner_exec_error| {
                    RuntimeErrorStruct::exec_stmt_new_with_stmt(
                        def_family_stmt.clone().into(),
                        "".to_string(),
                        Some(RuntimeError::from(inner_exec_error)),
                        vec![],
                    )
                })?;
            family_definition_infer_result.new_infer_result_inside(dom_fact_infer_result);
        }

        self.verify_obj_well_defined_and_store_cache(&def_family_stmt.equal_to, &verify_state)
            .map_err(|well_defined_error| {
                RuntimeErrorStruct::exec_stmt_new_with_stmt(
                    def_family_stmt.clone().into(),
                    "".to_string(),
                    Some(well_defined_error.into()),
                    vec![],
                )
            })?;

        Ok(family_definition_infer_result)
    }
}