litex/result/
runtime_result.rs1use 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 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}