litex/result/
runtime_success.rs

1use crate::prelude::*;
2
3#[derive(Debug)]
4pub struct NonFactualStmtSuccess {
5    pub stmt: Stmt,
6    pub infers: InferResult,
7    pub inside_results: Vec<StmtResult>,
8}
9
10#[derive(Debug)]
11pub struct VerifiedByBuiltinRuleResult {
12    pub msg: String,
13}
14
15#[derive(Debug)]
16pub struct VerifiedByFactResult {
17    pub detail: Option<String>,
18    pub cite_what: Box<Stmt>,
19}
20
21#[derive(Debug)]
22pub struct VerifiedBysResult {
23    pub cite_what: Vec<VerifiedBysEnum>,
24}
25
26#[derive(Debug)]
27pub struct FactVerifiedByBuiltinRuleInVerifiedBys {
28    pub msg: String,
29    pub verify_what: Fact,
30}
31
32#[derive(Debug)]
33pub struct FactVerifiedByFactInVerifiedBys {
34    pub detail: Option<String>,
35    pub verify_what: Fact,
36    pub cite_what: Box<Stmt>,
37}
38
39#[derive(Debug)]
40pub enum VerifiedBysEnum {
41    ByBuiltinRule(FactVerifiedByBuiltinRuleInVerifiedBys),
42    ByFact(FactVerifiedByFactInVerifiedBys),
43}
44
45#[derive(Debug)]
46pub enum VerifiedByResult {
47    BuiltinRule(VerifiedByBuiltinRuleResult),
48    Fact(VerifiedByFactResult),
49    VerifiedBys(VerifiedBysResult),
50}
51
52#[derive(Debug)]
53pub struct FactualStmtSuccess {
54    pub stmt: Fact,
55    pub infers: InferResult,
56    pub verified_by: VerifiedByResult,
57}
58
59impl FactualStmtSuccess {
60    pub fn verification_display_line(&self) -> String {
61        self.verified_by.display_line()
62    }
63
64    pub fn new_with_verified_by_builtin_rules(
65        stmt: Fact,
66        infers: InferResult,
67        verified_by: VerifiedByResult,
68    ) -> Self {
69        FactualStmtSuccess {
70            stmt,
71            infers,
72            verified_by,
73        }
74    }
75
76    pub fn new_with_verified_by_builtin_rules_recording_stmt(
77        stmt: Fact,
78        builtin_rule_label: String,
79        step_results: Vec<StmtResult>,
80    ) -> Self {
81        let infers = InferResult::from_fact(&stmt);
82        let verified_by = merge_verified_by_with_steps(
83            stmt.clone(),
84            VerifiedByResult::builtin_rule(builtin_rule_label, stmt.clone()),
85            step_results,
86        );
87        Self::new_with_verified_by_builtin_rules(stmt, infers, verified_by)
88    }
89
90    pub fn new_with_verified_by_builtin_rules_label_and_steps(
91        stmt: Fact,
92        infers: InferResult,
93        builtin_rule_label: String,
94        step_results: Vec<StmtResult>,
95    ) -> Self {
96        let verified_by = merge_verified_by_with_steps(
97            stmt.clone(),
98            VerifiedByResult::builtin_rule(builtin_rule_label, stmt.clone()),
99            step_results,
100        );
101        Self::new_with_verified_by_builtin_rules(stmt, infers, verified_by)
102    }
103
104    pub fn new_with_verified_by_known_fact_and_infer(
105        stmt: Fact,
106        infers: InferResult,
107        verified_by: VerifiedByResult,
108        step_results: Vec<StmtResult>,
109    ) -> Self {
110        let verified_by = merge_verified_by_with_steps(stmt.clone(), verified_by, step_results);
111        FactualStmtSuccess {
112            stmt,
113            infers,
114            verified_by,
115        }
116    }
117
118    pub fn new_with_verified_by_known_fact(
119        stmt: Fact,
120        verified_by: VerifiedByResult,
121        step_results: Vec<StmtResult>,
122    ) -> Self {
123        Self::new_with_verified_by_known_fact_and_infer(
124            stmt,
125            InferResult::new(),
126            verified_by,
127            step_results,
128        )
129    }
130
131    pub fn line_file_for_verified_by_known_fact_in_json(&self) -> LineFile {
132        self.verified_by
133            .first_cited_fact_line_file()
134            .unwrap_or_else(|| self.stmt.line_file())
135    }
136
137    pub fn is_verified_by_builtin_rules_only(&self) -> bool {
138        self.verified_by.tree_is_builtin_rules_only()
139    }
140}
141
142impl VerifiedByResult {
143    pub fn builtin_rule(msg: impl Into<String>, _goal: Fact) -> Self {
144        Self::BuiltinRule(VerifiedByBuiltinRuleResult { msg: msg.into() })
145    }
146
147    pub fn cited_fact(_goal: Fact, cite_what: Fact, detail: Option<String>) -> Self {
148        Self::cited_stmt(_goal, cite_what.into_stmt(), detail)
149    }
150
151    pub fn cited_stmt(_goal: Fact, cite_what: Stmt, detail: Option<String>) -> Self {
152        Self::Fact(VerifiedByFactResult {
153            detail,
154            cite_what: Box::new(cite_what),
155        })
156    }
157
158    /// Same statement as goal and citation; optional human note in `msg`.
159    pub fn fact_with_note(goal: Fact, msg: Option<String>) -> Self {
160        let cite_what = goal.clone();
161        Self::cited_fact(goal, cite_what, msg)
162    }
163
164    pub fn cached_fact(fact: Fact, cite_fact_source: LineFile) -> Self {
165        let cite_what = fact.with_line_file(cite_fact_source);
166        Self::Fact(VerifiedByFactResult {
167            detail: None,
168            cite_what: Box::new(cite_what.into_stmt()),
169        })
170    }
171
172    pub fn wrap_bys(children: Vec<VerifiedBysEnum>) -> Self {
173        Self::VerifiedBys(VerifiedBysResult {
174            cite_what: children,
175        })
176    }
177
178    pub fn tree_is_builtin_rules_only(&self) -> bool {
179        match self {
180            VerifiedByResult::BuiltinRule(r) => !r.msg.is_empty(),
181            VerifiedByResult::Fact(_) => false,
182            VerifiedByResult::VerifiedBys(w) => {
183                !w.cite_what.is_empty() && w.cite_what.iter().all(|b| b.is_builtin_rule())
184            }
185        }
186    }
187
188    pub fn first_builtin_rule_label(&self) -> Option<&str> {
189        match self {
190            VerifiedByResult::BuiltinRule(r) => {
191                if r.msg.is_empty() {
192                    None
193                } else {
194                    Some(r.msg.as_str())
195                }
196            }
197            VerifiedByResult::VerifiedBys(w) => {
198                for b in w.cite_what.iter() {
199                    if let VerifiedBysEnum::ByBuiltinRule(r) = b {
200                        return Some(r.msg.as_str());
201                    }
202                }
203                for b in w.cite_what.iter() {
204                    if let Some(l) = b.first_builtin_rule_label() {
205                        return Some(l);
206                    }
207                }
208                None
209            }
210            VerifiedByResult::Fact(_) => None,
211        }
212    }
213
214    fn first_cited_fact_line_file(&self) -> Option<LineFile> {
215        match self {
216            VerifiedByResult::BuiltinRule(_) => None,
217            VerifiedByResult::Fact(r) => Some(r.cite_what.line_file()),
218            VerifiedByResult::VerifiedBys(w) => {
219                for b in &w.cite_what {
220                    if let Some(lf) = b.first_cited_fact_line_file() {
221                        return Some(lf);
222                    }
223                }
224                None
225            }
226        }
227    }
228}
229
230impl VerifiedBysEnum {
231    pub fn builtin_rule(msg: String, verify_what: Fact) -> Self {
232        VerifiedBysEnum::ByBuiltinRule(FactVerifiedByBuiltinRuleInVerifiedBys { msg, verify_what })
233    }
234
235    pub fn cited_fact(verify_what: Fact, cite_what: Fact, detail: Option<String>) -> Self {
236        Self::cited_stmt(verify_what, cite_what.into_stmt(), detail)
237    }
238
239    pub fn cited_stmt(verify_what: Fact, cite_what: Stmt, detail: Option<String>) -> Self {
240        VerifiedBysEnum::ByFact(FactVerifiedByFactInVerifiedBys {
241            detail,
242            verify_what,
243            cite_what: Box::new(cite_what),
244        })
245    }
246
247    pub fn fact_with_note(verify_what: Fact, msg: Option<String>) -> Self {
248        let cite_what = verify_what.clone();
249        Self::cited_fact(verify_what, cite_what, msg)
250    }
251
252    fn from_verified_by_result(verify_what: Fact, verified_by: VerifiedByResult) -> Vec<Self> {
253        match verified_by {
254            VerifiedByResult::BuiltinRule(r) => vec![Self::builtin_rule(r.msg, verify_what)],
255            VerifiedByResult::Fact(r) => {
256                vec![Self::cited_stmt(verify_what, *r.cite_what, r.detail)]
257            }
258            VerifiedByResult::VerifiedBys(w) => w.cite_what,
259        }
260    }
261
262    fn is_builtin_rule(&self) -> bool {
263        match self {
264            VerifiedBysEnum::ByBuiltinRule(r) => !r.msg.is_empty(),
265            VerifiedBysEnum::ByFact(_) => false,
266        }
267    }
268
269    fn first_builtin_rule_label(&self) -> Option<&str> {
270        match self {
271            VerifiedBysEnum::ByBuiltinRule(r) => Some(r.msg.as_str()),
272            VerifiedBysEnum::ByFact(_) => None,
273        }
274    }
275
276    fn first_cited_fact_line_file(&self) -> Option<LineFile> {
277        match self {
278            VerifiedBysEnum::ByBuiltinRule(_) => None,
279            VerifiedBysEnum::ByFact(r) => Some(r.cite_what.line_file()),
280        }
281    }
282
283    fn display_line(&self) -> String {
284        match self {
285            VerifiedBysEnum::ByBuiltinRule(r) => r.msg.clone(),
286            VerifiedBysEnum::ByFact(r) => {
287                if let Some(d) = &r.detail {
288                    if !d.is_empty() {
289                        return d.clone();
290                    }
291                }
292                r.cite_what.to_string()
293            }
294        }
295    }
296}
297
298impl VerifiedByResult {
299    pub fn display_line(&self) -> String {
300        match self {
301            VerifiedByResult::BuiltinRule(r) => r.msg.clone(),
302            VerifiedByResult::Fact(r) => {
303                if let Some(d) = &r.detail {
304                    if !d.is_empty() {
305                        return d.clone();
306                    }
307                }
308                r.cite_what.to_string()
309            }
310            VerifiedByResult::VerifiedBys(w) => {
311                if w.cite_what.is_empty() {
312                    return String::new();
313                }
314                w.cite_what
315                    .iter()
316                    .map(|b| b.display_line())
317                    .collect::<Vec<_>>()
318                    .join("; ")
319            }
320        }
321    }
322}
323
324impl NonFactualStmtSuccess {
325    pub fn new(stmt: Stmt, infers: InferResult, inside_results: Vec<StmtResult>) -> Self {
326        NonFactualStmtSuccess {
327            stmt,
328            infers,
329            inside_results,
330        }
331    }
332
333    pub fn new_with_stmt(stmt: Stmt) -> Self {
334        Self::new(stmt, InferResult::new(), vec![])
335    }
336}
337
338fn merge_verified_by_with_steps(
339    _goal: Fact,
340    verified_by: VerifiedByResult,
341    step_results: Vec<StmtResult>,
342) -> VerifiedByResult {
343    if step_results.is_empty() {
344        return verified_by;
345    }
346    let mut items = VerifiedBysEnum::from_verified_by_result(_goal, verified_by);
347    for r in step_results {
348        items.extend(verified_by_items_from_stmt_result(r));
349    }
350    VerifiedByResult::wrap_bys(items)
351}
352
353pub(crate) fn verified_by_items_from_stmt_result(result: StmtResult) -> Vec<VerifiedBysEnum> {
354    match result {
355        StmtResult::FactualStmtSuccess(f) => {
356            VerifiedBysEnum::from_verified_by_result(f.stmt, f.verified_by)
357        }
358        StmtResult::NonFactualStmtSuccess(n) => {
359            let items = n
360                .inside_results
361                .into_iter()
362                .flat_map(verified_by_items_from_stmt_result)
363                .collect::<Vec<_>>();
364            items
365        }
366        StmtResult::StmtUnknown(_) => Vec::new(),
367    }
368}
litex/result/runtime_success.rs

litex/result/
runtime_success.rs
