lemma/evaluation/
proof.rs1use 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}