Skip to main content

litex/result/
runtime_result.rs

1use crate::prelude::*;
2
3#[derive(Debug)]
4pub enum StmtResult {
5    NonFactualStmtSuccess(NonFactualStmtSuccess),
6    FactualStmtSuccess(FactualStmtSuccess),
7    StmtUnknown(StmtUnknown),
8}
9
10impl From<NonFactualStmtSuccess> for StmtResult {
11    fn from(v: NonFactualStmtSuccess) -> Self {
12        StmtResult::NonFactualStmtSuccess(v)
13    }
14}
15
16impl From<FactualStmtSuccess> for StmtResult {
17    fn from(v: FactualStmtSuccess) -> Self {
18        StmtResult::FactualStmtSuccess(v)
19    }
20}
21
22impl From<StmtUnknown> for StmtResult {
23    fn from(v: StmtUnknown) -> Self {
24        StmtResult::StmtUnknown(v)
25    }
26}
27
28const VERIFIED_BY: &str = "verified by";
29const INFER_COLON: &str = "infer:";
30
31impl StmtResult {
32    pub fn with_infers(mut self, infer_result: InferResult) -> Self {
33        match &mut self {
34            StmtResult::NonFactualStmtSuccess(x) => x.infers.new_infer_result_inside(infer_result),
35            StmtResult::FactualStmtSuccess(x) => x.infers.new_infer_result_inside(infer_result),
36            StmtResult::StmtUnknown(_) => {}
37        }
38        self
39    }
40}
41
42impl StmtResult {
43    fn infer_block_string(infer_result: &InferResult) -> String {
44        if infer_result.is_empty() {
45            return String::new();
46        }
47        format!(
48            "\n\n{}\n{}",
49            INFER_COLON,
50            infer_result.join_infer_lines("\n")
51        )
52    }
53
54    /// Returns the result body string without any line/file prefix (for tests or when location is not needed).
55    pub fn body_string(&self) -> String {
56        match self {
57            StmtResult::NonFactualStmtSuccess(x) => {
58                format!(
59                    "{}\n{}{}",
60                    SUCCESS_COLON,
61                    x.stmt,
62                    Self::infer_block_string(&x.infers)
63                )
64            }
65            StmtResult::FactualStmtSuccess(x) => {
66                format!(
67                    "{}\n{}\n{}\n{}{}",
68                    SUCCESS_COLON,
69                    x.stmt,
70                    VERIFIED_BY,
71                    x.verification_display_line(),
72                    Self::infer_block_string(&x.infers)
73                )
74            }
75            StmtResult::StmtUnknown(x) => x.to_string(),
76        }
77    }
78}
79
80impl StmtResult {
81    #[allow(dead_code)]
82    pub fn line_file(&self) -> LineFile {
83        match self {
84            StmtResult::NonFactualStmtSuccess(x) => x.stmt.line_file(),
85            StmtResult::FactualStmtSuccess(x) => x.stmt.line_file(),
86            StmtResult::StmtUnknown(_) => default_line_file(),
87        }
88    }
89}
90
91impl StmtResult {
92    pub fn is_true(&self) -> bool {
93        match self {
94            StmtResult::NonFactualStmtSuccess(_) => true,
95            StmtResult::FactualStmtSuccess(_) => true,
96            StmtResult::StmtUnknown(_) => false,
97        }
98    }
99
100    pub fn is_unknown(&self) -> bool {
101        match self {
102            StmtResult::StmtUnknown(_) => true,
103            StmtResult::NonFactualStmtSuccess(_) => false,
104            StmtResult::FactualStmtSuccess(_) => false,
105        }
106    }
107}