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 msg: Option<String>,
18    pub cite_what: Fact,
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 msg: Option<String>,
35    pub verify_what: Fact,
36    pub cite_what: Fact,
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, msg: Option<String>) -> Self {
148        Self::Fact(VerifiedByFactResult { msg, cite_what })
149    }
150
151    /// Same statement as goal and citation; optional human note in `msg`.
152    pub fn fact_with_note(goal: Fact, msg: Option<String>) -> Self {
153        let cite_what = goal.clone();
154        Self::cited_fact(goal, cite_what, msg)
155    }
156
157    pub fn cached_fact(fact: Fact, cite_fact_source: LineFile) -> Self {
158        let cite_what = fact.with_line_file(cite_fact_source);
159        Self::Fact(VerifiedByFactResult {
160            msg: None,
161            cite_what,
162        })
163    }
164
165    pub fn wrap_bys(children: Vec<VerifiedBysEnum>) -> Self {
166        Self::VerifiedBys(VerifiedBysResult {
167            cite_what: children,
168        })
169    }
170
171    pub fn tree_is_builtin_rules_only(&self) -> bool {
172        match self {
173            VerifiedByResult::BuiltinRule(r) => !r.msg.is_empty(),
174            VerifiedByResult::Fact(_) => false,
175            VerifiedByResult::VerifiedBys(w) => {
176                !w.cite_what.is_empty() && w.cite_what.iter().all(|b| b.is_builtin_rule())
177            }
178        }
179    }
180
181    pub fn first_builtin_rule_label(&self) -> Option<&str> {
182        match self {
183            VerifiedByResult::BuiltinRule(r) => {
184                if r.msg.is_empty() {
185                    None
186                } else {
187                    Some(r.msg.as_str())
188                }
189            }
190            VerifiedByResult::VerifiedBys(w) => {
191                for b in w.cite_what.iter() {
192                    if let VerifiedBysEnum::ByBuiltinRule(r) = b {
193                        return Some(r.msg.as_str());
194                    }
195                }
196                for b in w.cite_what.iter() {
197                    if let Some(l) = b.first_builtin_rule_label() {
198                        return Some(l);
199                    }
200                }
201                None
202            }
203            VerifiedByResult::Fact(_) => None,
204        }
205    }
206
207    fn first_cited_fact_line_file(&self) -> Option<LineFile> {
208        match self {
209            VerifiedByResult::BuiltinRule(_) => None,
210            VerifiedByResult::Fact(r) => Some(r.cite_what.line_file()),
211            VerifiedByResult::VerifiedBys(w) => {
212                for b in &w.cite_what {
213                    if let Some(lf) = b.first_cited_fact_line_file() {
214                        return Some(lf);
215                    }
216                }
217                None
218            }
219        }
220    }
221}
222
223impl VerifiedBysEnum {
224    pub fn builtin_rule(msg: String, verify_what: Fact) -> Self {
225        VerifiedBysEnum::ByBuiltinRule(FactVerifiedByBuiltinRuleInVerifiedBys { msg, verify_what })
226    }
227
228    pub fn cited_fact(verify_what: Fact, cite_what: Fact, msg: Option<String>) -> Self {
229        VerifiedBysEnum::ByFact(FactVerifiedByFactInVerifiedBys {
230            msg,
231            verify_what,
232            cite_what,
233        })
234    }
235
236    pub fn fact_with_note(verify_what: Fact, msg: Option<String>) -> Self {
237        let cite_what = verify_what.clone();
238        Self::cited_fact(verify_what, cite_what, msg)
239    }
240
241    fn from_verified_by_result(verify_what: Fact, verified_by: VerifiedByResult) -> Vec<Self> {
242        match verified_by {
243            VerifiedByResult::BuiltinRule(r) => vec![Self::builtin_rule(r.msg, verify_what)],
244            VerifiedByResult::Fact(r) => {
245                vec![Self::cited_fact(verify_what, r.cite_what, r.msg)]
246            }
247            VerifiedByResult::VerifiedBys(w) => w.cite_what,
248        }
249    }
250
251    fn is_builtin_rule(&self) -> bool {
252        match self {
253            VerifiedBysEnum::ByBuiltinRule(r) => !r.msg.is_empty(),
254            VerifiedBysEnum::ByFact(_) => false,
255        }
256    }
257
258    fn first_builtin_rule_label(&self) -> Option<&str> {
259        match self {
260            VerifiedBysEnum::ByBuiltinRule(r) => Some(r.msg.as_str()),
261            VerifiedBysEnum::ByFact(_) => None,
262        }
263    }
264
265    fn first_cited_fact_line_file(&self) -> Option<LineFile> {
266        match self {
267            VerifiedBysEnum::ByBuiltinRule(_) => None,
268            VerifiedBysEnum::ByFact(r) => Some(r.cite_what.line_file()),
269        }
270    }
271
272    fn display_line(&self) -> String {
273        match self {
274            VerifiedBysEnum::ByBuiltinRule(r) => r.msg.clone(),
275            VerifiedBysEnum::ByFact(r) => {
276                if let Some(d) = &r.msg {
277                    if !d.is_empty() {
278                        return d.clone();
279                    }
280                }
281                r.cite_what.to_string()
282            }
283        }
284    }
285}
286
287impl VerifiedByResult {
288    pub fn display_line(&self) -> String {
289        match self {
290            VerifiedByResult::BuiltinRule(r) => r.msg.clone(),
291            VerifiedByResult::Fact(r) => {
292                if let Some(d) = &r.msg {
293                    if !d.is_empty() {
294                        return d.clone();
295                    }
296                }
297                r.cite_what.to_string()
298            }
299            VerifiedByResult::VerifiedBys(w) => {
300                if w.cite_what.is_empty() {
301                    return String::new();
302                }
303                w.cite_what
304                    .iter()
305                    .map(|b| b.display_line())
306                    .collect::<Vec<_>>()
307                    .join("; ")
308            }
309        }
310    }
311}
312
313impl NonFactualStmtSuccess {
314    pub fn new(stmt: Stmt, infers: InferResult, inside_results: Vec<StmtResult>) -> Self {
315        NonFactualStmtSuccess {
316            stmt,
317            infers,
318            inside_results,
319        }
320    }
321
322    pub fn new_with_stmt(stmt: Stmt) -> Self {
323        Self::new(stmt, InferResult::new(), vec![])
324    }
325}
326
327fn merge_verified_by_with_steps(
328    _goal: Fact,
329    verified_by: VerifiedByResult,
330    step_results: Vec<StmtResult>,
331) -> VerifiedByResult {
332    if step_results.is_empty() {
333        return verified_by;
334    }
335    let mut items = VerifiedBysEnum::from_verified_by_result(_goal, verified_by);
336    for r in step_results {
337        items.extend(verified_by_items_from_stmt_result(r));
338    }
339    VerifiedByResult::wrap_bys(items)
340}
341
342pub(crate) fn verified_by_items_from_stmt_result(result: StmtResult) -> Vec<VerifiedBysEnum> {
343    match result {
344        StmtResult::FactualStmtSuccess(f) => {
345            VerifiedBysEnum::from_verified_by_result(f.stmt, f.verified_by)
346        }
347        StmtResult::NonFactualStmtSuccess(n) => {
348            let items = n
349                .inside_results
350                .into_iter()
351                .flat_map(verified_by_items_from_stmt_result)
352                .collect::<Vec<_>>();
353            items
354        }
355        StmtResult::StmtUnknown(_) => Vec::new(),
356    }
357}
litex/result/runtime_success.rs

litex/result/
runtime_success.rs
