Skip to main content

macroonz_compiler/expansion/
type_contract.rs

1//! The constant answers this home's one roster settles, and the contracts a binding refusal stands under.
2//!
3//! The table is total, so a pair admitted later stops the compiler here until somebody says what its position and its sentence are.
4
5use super::{BINDING_FACT, BindError};
6use crate::bounded::Bounded;
7use crate::diagnostic::{
8    BINDING_FAMILY, Family, LineBody, Observed, Phase, REPAIR_LIMIT, RefusalClass, Refused, Repair,
9};
10use crate::identity::human_projection;
11use core::fmt;
12
13impl BindError {
14    /// This pair's position in the declared roster, written ahead of the two identities it disagreed over.
15    ///
16    /// Appended and never renumbered: the byte stands inside every related identity derived over a binding refusal.
17    #[must_use]
18    pub const fn slot(&self) -> u8 {
19        match self {
20            Self::ClosureProvedAgainstAnotherPlan { .. } => 0,
21            Self::ExplanationAnsweredOverAnotherPlan { .. } => 1,
22            Self::ExplanationAnsweredOverAnotherClosure { .. } => 2,
23        }
24    }
25}
26
27impl fmt::Display for BindError {
28    fn fmt(&self, into: &mut fmt::Formatter<'_>) -> fmt::Result {
29        into.write_str(match self {
30            Self::ClosureProvedAgainstAnotherPlan { .. } => {
31                "the closure proves a rendering against a plan other than the one bound beside it"
32            }
33            Self::ExplanationAnsweredOverAnotherPlan { .. } => {
34                "the explanation was answered over a plan other than the one bound beside it"
35            }
36            Self::ExplanationAnsweredOverAnotherClosure { .. } => {
37                "the explanation was answered over a proof other than the one bound beside it"
38            }
39        })
40    }
41}
42
43impl core::error::Error for BindError {}
44
45impl Refused for BindError {
46    const PHASE: Phase = Phase::Binding;
47    const FAMILY: Family = BINDING_FAMILY;
48
49    fn class(&self) -> RefusalClass {
50        RefusalClass::ExpansionNotBound
51    }
52
53    fn first(&self) -> String {
54        self.to_string()
55    }
56
57    /// Every pair is two identities that had to match and did not.
58    fn observed(&self) -> Observed {
59        Observed::IdentityDisagreement
60    }
61
62    /// One disagreement, always.
63    ///
64    /// The binding compares each pair in turn and refuses at the first that disagrees, so there is no body behind the cause and nothing for a line to count.
65    fn body(&self) -> LineBody {
66        LineBody::SingleCause
67    }
68
69    /// A single cause enumerates nothing: the primary cause is the summary's own subject, never a member of its related set.
70    fn related(&self) -> Vec<Vec<u8>> {
71        Vec::new()
72    }
73
74    /// The one repair, citing this home's own declared fact.
75    ///
76    /// Unlike a refusal about what a caller declared, the law here is this compiler's, so the fact is this home's to cite.
77    fn repairs(&self) -> Bounded<Repair, REPAIR_LIMIT> {
78        Bounded::from_array([Repair {
79            declared_by: BINDING_FACT,
80            description: human_projection!(
81                "an expansion binds the plan its proof was taken against and the explanation answered over the two, so a proof or an explanation belonging to another expansion is refused rather than bound under one identity"
82            ),
83        }])
84    }
85}