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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147

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

#[derive(Clone)]
pub enum ImportStmt {
    ImportRelativePath(ImportRelativePathStmt),
    ImportGlobalModule(ImportGlobalModuleStmt),
}

#[derive(Clone)]
pub struct ImportRelativePathStmt {
    pub path: String,
    pub as_mod_name: Option<String>,
    pub line_file: LineFile,
}

#[derive(Clone)]
pub struct ImportGlobalModuleStmt {
    pub mod_name: String,
    pub as_mod_name: Option<String>,
    pub line_file: LineFile,
}

#[derive(Clone)]
pub struct RunFileStmt {
    pub file_path: String,
    pub line_file: LineFile,
}

impl RunFileStmt {
    pub fn new(file_path: String, line_file: LineFile) -> Self {
        RunFileStmt {
            file_path,
            line_file,
        }
    }
}

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

impl fmt::Display for ImportStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            ImportStmt::ImportRelativePath(import_relative_path) => {
                write!(f, "{}", import_relative_path)
            }
            ImportStmt::ImportGlobalModule(import_global_mod) => write!(f, "{}", import_global_mod),
        }
    }
}

impl ImportRelativePathStmt {
    pub fn new(path: String, as_mod_name: Option<String>, line_file: LineFile) -> Self {
        ImportRelativePathStmt {
            path,
            as_mod_name,
            line_file,
        }
    }
}

impl ImportGlobalModuleStmt {
    pub fn new(mod_name: String, as_mod_name: Option<String>, line_file: LineFile) -> Self {
        ImportGlobalModuleStmt {
            mod_name,
            as_mod_name,
            line_file,
        }
    }
}

impl fmt::Display for ImportRelativePathStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match &self.as_mod_name {
            Some(name) => write!(
                f,
                "{} {}{}{} {} {}",
                IMPORT, DOUBLE_QUOTE, self.path, DOUBLE_QUOTE, AS, name
            ),
            None => write!(
                f,
                "{} {}{}{}",
                IMPORT, DOUBLE_QUOTE, self.path, DOUBLE_QUOTE
            ),
        }
    }
}

impl fmt::Display for ImportGlobalModuleStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match &self.as_mod_name {
            Some(name) => write!(f, "{} {} {} {}", IMPORT, self.mod_name, AS, name),
            None => write!(f, "{} {}", IMPORT, self.mod_name),
        }
    }
}

impl ImportStmt {
    pub fn line_file(&self) -> LineFile {
        match self {
            ImportStmt::ImportRelativePath(import_relative_path) => {
                import_relative_path.line_file.clone()
            }
            ImportStmt::ImportGlobalModule(import_global_mod) => {
                import_global_mod.line_file.clone()
            }
        }
    }
}

#[derive(Clone)]
pub struct DoNothingStmt {
    pub line_file: LineFile,
}

impl DoNothingStmt {
    pub fn new(line_file: LineFile) -> Self {
        DoNothingStmt { line_file }
    }
}

impl fmt::Display for DoNothingStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", DO_NOTHING)
    }
}

#[derive(Clone)]
pub struct ClearStmt {
    pub line_file: LineFile,
}

impl ClearStmt {
    pub fn new(line_file: LineFile) -> Self {
        ClearStmt { line_file }
    }
}

impl fmt::Display for ClearStmt {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", CLEAR)
    }
}