litex-lang 0.9.75-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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102

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

#[derive(Clone)]
pub struct ByStructBinding {
    pub name: String,
    pub tuple: Obj,
    pub struct_ty: StructAsParamType,
}

#[derive(Clone)]
pub struct ByStructValueBinding {
    pub name: String,
    pub value: Obj,
}

#[derive(Clone)]
pub struct ByStructStmt {
    pub struct_bindings: Vec<ByStructBinding>,
    pub value_bindings: Vec<ByStructValueBinding>,
    pub forall_fact: ForallFact,
    pub line_file: LineFile,
}

impl ByStructBinding {
    pub fn new(name: String, tuple: Obj, struct_ty: StructAsParamType) -> Self {
        ByStructBinding {
            name,
            tuple,
            struct_ty,
        }
    }
}

impl ByStructValueBinding {
    pub fn new(name: String, value: Obj) -> Self {
        ByStructValueBinding { name, value }
    }
}

impl ByStructStmt {
    pub fn new(
        struct_bindings: Vec<ByStructBinding>,
        value_bindings: Vec<ByStructValueBinding>,
        forall_fact: ForallFact,
        line_file: LineFile,
    ) -> Self {
        ByStructStmt {
            struct_bindings,
            value_bindings,
            forall_fact,
            line_file,
        }
    }
}

impl fmt::Display for ByStructBinding {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(
            f,
            "{} {} {} {} {}",
            self.name, FROM, self.tuple, AS, self.struct_ty.name
        )?;
        if !self.struct_ty.args.is_empty() {
            write!(
                f,
                "{}{}{}",
                LEFT_BRACE,
                vec_to_string_join_by_comma(&self.struct_ty.args),
                RIGHT_BRACE
            )?;
        }
        Ok(())
    }
}

impl fmt::Display for ByStructValueBinding {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{} {} {}", self.name, EQUAL, self.value)
    }
}

impl fmt::Display for ByStructStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let mut parts = Vec::new();
        for binding in self.struct_bindings.iter() {
            parts.push(binding.to_string());
        }
        for binding in self.value_bindings.iter() {
            parts.push(binding.to_string());
        }
        write!(
            f,
            "{} {} {}{} {}",
            BY,
            STRUCT,
            vec_to_string_join_by_comma(&parts),
            COLON,
            self.forall_fact
        )
    }
}