mant_protocol/explanation/
support.rs1use schemars::JsonSchema;
3use serde::{Deserialize, Serialize};
4
5#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
8#[serde(
9 tag = "kind",
10 rename_all = "kebab-case",
11 rename_all_fields = "camelCase",
12 deny_unknown_fields
13)]
14pub enum ExplanationSupport {
15 OwnedEntry {
17 block: mant_ir::Block,
19 },
20 DeclarationGroup {
23 block_path: String,
25 group: mant_ir::DeclarationGroup,
27 members: Vec<crate::OutlineTrail>,
29 block: mant_ir::Block,
32 },
33 ContainedDeclarationGroup {
37 block_path: String,
39 group: mant_ir::DeclarationGroup,
41 members: Vec<crate::OutlineTrail>,
43 support: usize,
45 path: Vec<super::ExplanationBlockStep>,
47 },
48}
49
50impl ExplanationSupport {
51 #[must_use]
54 pub fn items(&self) -> Option<&[mant_ir::DefinitionItem]> {
55 let Self::DeclarationGroup {
56 group,
57 members,
58 block,
59 ..
60 } = self
61 else {
62 return None;
63 };
64 let mant_ir::Block::DefinitionList {
65 items,
66 declaration_groups,
67 ..
68 } = block
69 else {
70 return None;
71 };
72 let width = group.end_item.checked_sub(group.start_item)?;
73 let local = mant_ir::DeclarationGroup {
74 start_item: 0,
75 end_item: width,
76 };
77 if width > crate::MAX_EXPLANATION_RESULTS as usize
78 || items.len() != width
79 || members.len() != width
80 || declaration_groups.as_slice() != [local]
81 || items.iter().zip(members).any(|(item, member)| {
82 mant_ir::EntryOwner::Definition(item)
83 .facts()
84 .is_none_or(|facts| facts.id.as_str() != member.node.id())
85 })
86 {
87 return None;
88 }
89 local.resolve(items)
90 }
91
92 #[must_use]
95 pub fn items_in<'a>(&'a self, pool: &'a [Self]) -> Option<&'a [mant_ir::DefinitionItem]> {
96 let (block, group) = self.fragment(pool)?;
97 let mant_ir::Block::DefinitionList { items, .. } = block else {
98 return None;
99 };
100 group.resolve(items)
101 }
102
103 #[must_use]
105 pub fn members(&self) -> &[crate::OutlineTrail] {
106 match self {
107 Self::OwnedEntry { .. } => &[],
108 Self::DeclarationGroup { members, .. }
109 | Self::ContainedDeclarationGroup { members, .. } => members,
110 }
111 }
112
113 #[must_use]
116 pub fn materialized<'a>(&'a self, pool: &'a [Self]) -> Option<&'a mant_ir::Block> {
117 if let Self::OwnedEntry { block } = self {
118 return block.entry_owner().map(|_| block);
119 }
120 self.fragment(pool)?;
121 match self {
122 Self::OwnedEntry { .. } => None,
123 Self::DeclarationGroup { block, .. } => Some(block),
124 Self::ContainedDeclarationGroup { support, .. } => match pool.get(*support)? {
125 Self::DeclarationGroup { block, .. } | Self::OwnedEntry { block } => Some(block),
126 Self::ContainedDeclarationGroup { .. } => None,
127 },
128 }
129 }
130
131 fn fragment<'a>(
132 &'a self,
133 pool: &'a [Self],
134 ) -> Option<(&'a mant_ir::Block, mant_ir::DeclarationGroup)> {
135 match self {
136 Self::OwnedEntry { .. } => None,
137 Self::DeclarationGroup { block, .. } => Some((
138 block,
139 mant_ir::DeclarationGroup {
140 start_item: 0,
141 end_item: self.items()?.len(),
142 },
143 )),
144 Self::ContainedDeclarationGroup {
145 group,
146 members,
147 support,
148 path,
149 ..
150 } => {
151 let parent = pool.get(*support)?;
152 let block = match parent {
153 Self::DeclarationGroup { block, .. } => {
154 parent.items()?;
155 block
156 }
157 Self::OwnedEntry { block } => {
158 block.entry_owner()?;
159 block
160 }
161 Self::ContainedDeclarationGroup { .. } => return None,
162 };
163 if path.is_empty() {
164 return None;
165 }
166 let block = super::locations::block_at(block, path)?;
167 let mant_ir::Block::DefinitionList {
168 items,
169 declaration_groups,
170 ..
171 } = block
172 else {
173 return None;
174 };
175 let items = group.resolve(items)?;
176 if !declaration_groups.contains(group)
177 || items.len() != members.len()
178 || items.len() > crate::MAX_EXPLANATION_RESULTS as usize
179 || items.iter().zip(members).any(|(item, member)| {
180 item.entry
181 .as_ref()
182 .is_none_or(|facts| facts.id.as_str() != member.node.id())
183 })
184 {
185 return None;
186 }
187 Some((block, *group))
188 }
189 }
190 }
191}
192
193impl super::ExplanationContent {
194 #[must_use]
196 pub fn referenced_owner<'a>(
197 &self,
198 pool: &'a [ExplanationSupport],
199 ) -> Option<mant_ir::EntryOwner<'a>> {
200 if let Self::SharedEntry {
201 support,
202 path,
203 item_index,
204 } = self
205 {
206 let fragment = pool.get(*support)?;
207 if matches!(
208 fragment,
209 ExplanationSupport::ContainedDeclarationGroup { .. }
210 ) {
211 return None;
212 }
213 let block = super::locations::block_at(fragment.materialized(pool)?, path)?;
214 return match block {
215 mant_ir::Block::DefinitionList { items, .. } => {
216 items.get(*item_index).map(mant_ir::EntryOwner::Definition)
217 }
218 mant_ir::Block::List { items, .. } => {
219 items.get(*item_index).map(mant_ir::EntryOwner::List)
220 }
221 _ => None,
222 };
223 }
224 let Self::DeclarationMember {
225 support,
226 item_index,
227 } = self
228 else {
229 return None;
230 };
231 Some(mant_ir::EntryOwner::Definition(
232 pool.get(*support)?.items_in(pool)?.get(*item_index)?,
233 ))
234 }
235
236 #[must_use]
238 pub fn resolve_range<'a>(
239 &'a self,
240 pool: &'a [ExplanationSupport],
241 range: &super::ExplanationContentRange,
242 ) -> Option<super::ExplanationTextRoot<'a>> {
243 use super::{ExplanationBlockStep as Step, ExplanationContentRange as Range};
244 match self {
245 Self::SharedEntry {
246 support,
247 path,
248 item_index,
249 } => {
250 self.referenced_owner(pool)?;
251 remap_range(range, path, *item_index)?
252 .resolve(pool.get(*support)?.materialized(pool)?)
253 }
254 Self::Entry { block } | Self::Block { block } => range.resolve(block),
255 Self::DeclarationMember {
256 support,
257 item_index,
258 } => {
259 self.referenced_owner(pool)?;
260 let (block, group) = pool.get(*support)?.fragment(pool)?;
261 let item_index = group.start_item.checked_add(*item_index)?;
262 let mut mapped = range.clone();
263 let path = match &mut mapped {
264 Range::DefinitionTerm {
265 path,
266 item_index: index,
267 ..
268 } if path.is_empty() => {
269 if *index != 0 {
270 return None;
271 }
272 *index = u32::try_from(item_index).ok()?;
273 return mapped.resolve(block);
274 }
275 Range::BlockText { path, .. } | Range::DefinitionTerm { path, .. } => path,
276 };
277 let Some(Step::DefinitionItem { index }) = path.first_mut() else {
278 return None;
279 };
280 if *index != 0 {
281 return None;
282 }
283 *index = u32::try_from(item_index).ok()?;
284 mapped.resolve(block)
285 }
286 }
287 }
288}
289
290impl super::ExplanationEvidence {
291 #[must_use]
294 pub fn source_reference(&self, pool: &[ExplanationSupport]) -> Option<usize> {
295 if self.covered_by_support(pool) {
296 self.support
297 } else {
298 self.shared_entry(pool)
299 }
300 }
301 #[must_use]
303 pub fn shared_entry(&self, pool: &[ExplanationSupport]) -> Option<usize> {
304 let content @ super::ExplanationContent::SharedEntry { support, .. } =
305 self.content.as_ref()?
306 else {
307 return None;
308 };
309 (self.class == super::EvidenceClass::DirectEntry
310 && self.support.is_none()
311 && !self.content_omitted
312 && content
313 .referenced_owner(pool)
314 .is_some_and(|owner| self.matches_owner(owner)))
315 .then_some(*support)
316 }
317 #[must_use]
320 pub fn covered_by_support(&self, pool: &[ExplanationSupport]) -> bool {
321 let Some(content @ super::ExplanationContent::DeclarationMember { support, .. }) =
322 &self.content
323 else {
324 return false;
325 };
326 self.support == Some(*support)
327 && self.class == super::EvidenceClass::DirectEntry
328 && !self.content_omitted
329 && !self.support_omitted
330 && content
331 .referenced_owner(pool)
332 .is_some_and(|owner| self.matches_owner(owner))
333 }
334
335 fn matches_owner(&self, owner: mant_ir::EntryOwner<'_>) -> bool {
336 owner
337 .facts()
338 .is_some_and(|facts| facts.id.as_str() == self.outline.node.id())
339 && owner.forms().is_some_and(|forms| {
340 self.entry.as_ref().is_none_or(|entry| {
341 entry.forms.is_empty() || forms.iter().eq(entry.forms.iter().map(Vec::as_slice))
342 })
343 })
344 }
345
346 fn valid_references(&self, pool: &[ExplanationSupport]) -> bool {
347 use super::{EvidenceBasis, ExplanationContent, ExplanationOccurrence};
348 if matches!(self.content, Some(ExplanationContent::SharedEntry { .. }))
349 && self.shared_entry(pool).is_none()
350 || self.support_omitted && self.class != super::EvidenceClass::DirectEntry
351 || self.content_omitted && self.content.is_some()
352 || self.support.is_some() && !self.covered_by_support(pool)
353 || self.support.is_some_and(|index| pool.get(index).is_none())
354 || self.support.is_some() && self.support_omitted
355 || matches!(
356 self.content,
357 Some(ExplanationContent::DeclarationMember { .. })
358 ) && !self.covered_by_support(pool)
359 {
360 return false;
361 }
362 let valid_content = |range: &super::ExplanationContentRange| {
363 self.content
364 .as_ref()
365 .is_some_and(|content| content.resolve_range(pool, range).is_some())
366 };
367 let valid_occurrence = |occurrence: &ExplanationOccurrence| {
368 occurrence.forms.iter().all(|range| {
369 self.entry
370 .as_ref()
371 .is_some_and(|entry| range.resolve(&entry.forms).is_some())
372 }) && occurrence.content.iter().all(&valid_content)
373 };
374 self.bases.iter().all(|basis| match basis {
375 EvidenceBasis::Name { matches } => matches
376 .iter()
377 .all(|m| m.occurrences.iter().all(&valid_occurrence)),
378 EvidenceBasis::Form { matches } => matches
379 .iter()
380 .all(|m| m.occurrences.iter().all(&valid_occurrence)),
381 _ => true,
382 }) && self.entry.as_ref().is_none_or(|entry| {
383 entry.name_bindings.iter().all(|binding| {
384 (binding.name_index as usize) < entry.names.len()
385 && binding.occurrences.iter().all(&valid_occurrence)
386 })
387 }) && self
388 .previews
389 .iter()
390 .all(|p| p.content_ranges.iter().all(&valid_content))
391 }
392}
393
394fn valid_pool(pool: &[ExplanationSupport]) -> bool {
395 pool.len() <= crate::MAX_EXPLANATION_RESULTS as usize
396 && pool
397 .iter()
398 .all(|support| support.materialized(pool).is_some())
399}
400
401fn remap_range(
402 range: &super::ExplanationContentRange,
403 prefix: &[super::ExplanationBlockStep],
404 owner: usize,
405) -> Option<super::ExplanationContentRange> {
406 use super::{ExplanationBlockStep as Step, ExplanationContentRange as Range};
407 let mut mapped = range.clone();
408 let owner = u32::try_from(owner).ok()?;
409 let path = match &mut mapped {
410 Range::DefinitionTerm {
411 path, item_index, ..
412 } if path.is_empty() => {
413 if *item_index != 0 {
414 return None;
415 }
416 *item_index = owner;
417 path.extend_from_slice(prefix);
418 return Some(mapped);
419 }
420 Range::BlockText { path, .. } | Range::DefinitionTerm { path, .. } => path,
421 };
422 let (Step::DefinitionItem { index } | Step::ListItem { index }) = path.first_mut()? else {
423 return None;
424 };
425 if *index != 0 {
426 return None;
427 }
428 *index = owner;
429 path.splice(0..0, prefix.iter().copied());
430 Some(mapped)
431}
432
433impl super::QueryExplanation {
434 pub fn validate_references(&self) -> Result<(), &'static str> {
440 (valid_pool(&self.supports)
441 && self
442 .evidence
443 .iter()
444 .all(|e| e.valid_references(&self.supports)))
445 .then_some(())
446 .ok_or("invalid explanation source reference or position")
447 }
448}
449
450impl crate::ScopeExplanation {
451 pub fn validate_references(&self) -> Result<(), &'static str> {
457 (self.documents.iter().all(|d| valid_pool(&d.supports))
458 && self.evidence.iter().all(|e| {
459 self.documents
460 .get(e.document_index)
461 .is_some_and(|d| e.evidence.valid_references(&d.supports))
462 }))
463 .then_some(())
464 .ok_or("invalid scoped explanation source reference or position")
465 }
466}