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

use crate::prelude::*;
use std::fmt;

#[derive(Clone)]
pub struct ForallFact {
    pub params_def_with_type: Vec<ParamGroupWithParamType>,
    pub dom_facts: Vec<ExistOrAndChainAtomicFact>,
    pub then_facts: Vec<ExistOrAndChainAtomicFact>,
    pub line_file: LineFile,
}

impl ForallFact {
    pub fn new(
        params_def_with_type: Vec<ParamGroupWithParamType>,
        dom_facts: Vec<ExistOrAndChainAtomicFact>,
        then_facts: Vec<ExistOrAndChainAtomicFact>,
        line_file: LineFile,
    ) -> Self {
        ForallFact {
            params_def_with_type,
            dom_facts,
            then_facts,
            line_file,
        }
    }
}

impl fmt::Display for ForallFact {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self.dom_facts.len() {
            0 => write!(
                f,
                "{} {}{}\n{}",
                FORALL,
                vec_to_string_join_by_comma(&self.params_def_with_type),
                COLON,
                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 1)
            ),
            _ => write!(
                f,
                "{} {}{}\n{}\n{}{}\n{}",
                FORALL,
                vec_to_string_join_by_comma(&self.params_def_with_type),
                COLON,
                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.dom_facts, 1),
                to_string_and_add_four_spaces_at_beginning_of_each_line(&RIGHT_ARROW, 1),
                COLON,
                vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.then_facts, 2)
            ),
        }
    }
}