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)]
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)]
54pub enum ValueSource {
55    Fact { fact_ref: FactPath },
56    Literal,
57    Computed,
58}
59
60#[derive(Debug, Clone, Serialize)]
61pub struct Branch {
62    pub condition: Option<Box<ProofNode>>,
63    pub result: Box<ProofNode>,
64    pub clause_index: Option<usize>,
65    pub source_location: Option<Source>,
66}
67
68#[derive(Debug, Clone, Serialize)]
69pub struct NonMatchedBranch {
70    pub condition: Box<ProofNode>,
71    pub result: Option<Box<ProofNode>>,
72    pub clause_index: Option<usize>,
73    pub source_location: Option<Source>,
74}
lemma/evaluation/proof.rs

lemma/evaluation/
proof.rs
