Skip to main content

lemma/evaluation/
proof.rs

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