lemma/evaluation/
proof.rs1use crate::evaluation::operations::{ComputationKind, OperationResult};
2use crate::{FactPath, RulePath};
3use crate::{LiteralValue, Source};
4use serde::Serialize;
5
6#[derive(Debug, Clone, Serialize)]
7pub struct Proof {
8 pub rule_path: RulePath,
9 pub source: Option<Source>,
10 pub result: OperationResult,
11 pub tree: ProofNode,
12}
13
14#[derive(Debug, Clone, Serialize)]
15#[serde(rename_all = "snake_case")]
16pub enum ProofNode {
17 Value {
18 value: LiteralValue,
19 source: ValueSource,
20 source_location: Option<Source>,
21 },
22 RuleReference {
23 rule_path: RulePath,
24 result: OperationResult,
25 source_location: Option<Source>,
26 expansion: Box<ProofNode>,
27 },
28 Computation {
29 kind: ComputationKind,
30 original_expression: String,
31 expression: String,
32 result: LiteralValue,
33 source_location: Option<Source>,
34 operands: Vec<ProofNode>,
35 },
36 Branches {
37 matched: Box<Branch>,
38 non_matched: Vec<NonMatchedBranch>,
39 source_location: Option<Source>,
40 },
41 Condition {
42 original_expression: String,
43 expression: String,
44 result: bool,
45 source_location: Option<Source>,
46 operands: Vec<ProofNode>,
47 },
48 Veto {
49 message: Option<String>,
50 source_location: Option<Source>,
51 },
52}
53
54#[derive(Debug, Clone, Serialize)]
55#[serde(rename_all = "snake_case")]
56pub enum ValueSource {
57 Fact { fact_ref: FactPath },
58 Literal,
59 Computed,
60}
61
62#[derive(Debug, Clone, Serialize)]
63pub struct Branch {
64 pub condition: Option<Box<ProofNode>>,
65 pub result: Box<ProofNode>,
66 pub clause_index: Option<usize>,
67 pub source_location: Option<Source>,
68}
69
70#[derive(Debug, Clone, Serialize)]
71pub struct NonMatchedBranch {
72 pub condition: Box<ProofNode>,
73 pub result: Option<Box<ProofNode>>,
74 pub clause_index: Option<usize>,
75 pub source_location: Option<Source>,
76}