vize_l3 0.553.0

L3 - the Davinci reactivity IR (codename Impeto): flat scheduled ops with explicit state and effect edges
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

use vize_l0::Span;

use super::{BindingId, BindingOrigin, EffectSet, EscapeKind, ReactivityClass};

/// Epistemic axis for a lattice classification.
///
/// One axis for every fact group: P4-6a moved the type into
/// `vize_l0::diag` so witnesses and the verifier share it, and the
/// lattice re-exports it with its folio spellings unchanged.
pub use vize_l0::diag::Verdict;

/// Summary provided by the retained-AST analyzer.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct BindingInput {
    pub id: BindingId,
    pub origin: BindingOrigin,
    pub effects: EffectSet,
    pub escape: EscapeKind,
    pub verdict: Verdict,
    pub span: Span,
}

impl BindingInput {
    /// A local binding with no effects or escape.
    #[must_use]
    pub const fn local(id: BindingId, span: Span) -> Self {
        Self {
            id,
            origin: BindingOrigin::Local,
            effects: EffectSet::empty(),
            escape: EscapeKind::None,
            verdict: Verdict::Proven,
            span,
        }
    }

    /// Override the binding origin.
    #[must_use]
    pub const fn with_origin(mut self, origin: BindingOrigin) -> Self {
        self.origin = origin;
        self
    }

    /// Override the effect set.
    #[must_use]
    pub const fn with_effects(mut self, effects: EffectSet) -> Self {
        self.effects = effects;
        self
    }

    /// Override the escape-analysis result.
    #[must_use]
    pub const fn with_escape(mut self, escape: EscapeKind) -> Self {
        self.escape = escape;
        self
    }

    /// Override the epistemic verdict.
    #[must_use]
    pub const fn with_verdict(mut self, verdict: Verdict) -> Self {
        self.verdict = verdict;
        self
    }
}

/// Published lattice fact for one binding.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct BindingFact {
    pub id: BindingId,
    pub class: ReactivityClass,
    pub verdict: Verdict,
    pub origin: BindingOrigin,
    pub effects: EffectSet,
    pub escape: EscapeKind,
    pub span: Span,
}

impl BindingFact {
    /// Returns the class only when the epistemic axis is proven.
    #[must_use]
    pub const fn proven_class(self) -> Option<ReactivityClass> {
        if self.verdict.is_proven() {
            Some(self.class)
        } else {
            None
        }
    }

    /// Consumer helper: facts never fire when their verdict is not proven.
    #[must_use]
    pub const fn fires_as(self, class: ReactivityClass) -> bool {
        self.verdict.is_proven() && self.class as u8 == class as u8
    }
}