Skip to main content

lemma/evaluation/
proof.rs

1use 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}