pub struct View<K: Kind> { /* private fields */ }Expand description
One complete explanation: every question a kind owes, answered exactly once, over the plan and the proof the answers are ABOUT.
Holding one is the coverage proof, and there is no partial view — a set of answers that could not be completed is a refusal instead.
§Authority
The parentage is taken and never supplied. A view assembled from two identities beside the answers would name a plan and a closure it was never written over: every question answered correctly, about a different expansion of the same kind, and the type parameter cannot catch that because a kind is not an expansion.
§Ordering
The universal seats stand in the compiler’s roster order and the declared seats in the kind’s, never in the order a caller supplied them. That order is what the identity is derived over, so one set of answers is one explanation however it was assembled.
Implementations§
Source§impl<K: Kind> View<K>
impl<K: Kind> View<K>
Sourcepub fn complete(
plan: &Plan<K>,
closure: &Closure<K::Role>,
universal: Vec<UniversalAnswer>,
declared: Vec<<K::Question as Question>::Answer>,
) -> Result<Self, ExplanationError>
pub fn complete( plan: &Plan<K>, closure: &Closure<K::Role>, universal: Vec<UniversalAnswer>, declared: Vec<<K::Question as Question>::Answer>, ) -> Result<Self, ExplanationError>
Complete one view over the universal questions and the kind’s own, answered over one plan and the proof of its rendering.
§The parentage is taken, never supplied
The plan arrives as the PLAN and the closure as the PROOF, and both identities are read off them here.
A road that took two identities beside the answers would take two values any caller can spell, and the view it built would name a parentage it was never written over — which is a complete, well-formed explanation about something else.
A Closure is reachable only by proving a rendering against a plan, so a caller standing here has done that or has nothing to hand in, and its role roster is the kind’s own.
§The explanation transcript
This is a mint site, so its content grammar is stated in full.
The identity is derived under Role::Explanation, anchored on the CLOSURE’s identity at full width — an explanation is written after a closure and over it — at position zero, over
content = bytes(plan) || u64be(universal seats) || seat* || u64be(declared seats) || seat*where each seat is the question’s roster position in two big-endian bytes followed by the answer’s own canonical bytes, in that roster’s declared order.
The two rosters are written behind two counts, so the split between them is framed rather than inferred: a universal seat and a declared seat may share a position.
Human prose is not a member — a rendered line is a projection of a typed answer, so a preimage carrying one would commit to a rendering rather than to what was answered.
§Errors
Returns ExplanationError naming every unanswered question, every doubled question, every answer standing outside its own roster, the seat bound where a kind’s roster outgrows it, and an output answer that does not restate the proof’s own rendered roster.
All of them together: a caller repairing a view one question per attempt is a caller the protocol failed.
Sourcepub const fn identity(&self) -> ExplanationId
pub const fn identity(&self) -> ExplanationId
This view’s own identity — the name a binding commits to.
Sourcepub const fn provenance(&self) -> &Provenance
pub const fn provenance(&self) -> &Provenance
The record of how that identity was derived.
Sourcepub const fn plan(&self) -> PlanId
pub const fn plan(&self) -> PlanId
The plan this view was answered over.
Read back so a binding establishes that the plan it seals is the plan the answers are about, rather than assuming it.
Sourcepub const fn closure(&self) -> ClosureId
pub const fn closure(&self) -> ClosureId
The proved closure this view was answered over, on the same terms.
Sourcepub fn universal(&self) -> &[UniversalAnswer]
pub fn universal(&self) -> &[UniversalAnswer]
The universal answers, in the compiler’s roster order.