1use crate::{ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0, AbstractPropertyValueV0};
2use omena_syntax::ident::AuthoredPropertyTextV0;
3use serde::Serialize;
4use std::collections::{BTreeMap, BTreeSet};
5
6#[derive(Debug, Clone, Serialize)]
12#[serde(rename_all = "camelCase")]
13pub struct CascadeValueFamilyV0 {
14 pub schema_version: &'static str,
15 pub product: &'static str,
16 pub framing: &'static str,
17 pub claim_level: &'static str,
18 pub property_name: AuthoredPropertyTextV0,
19 pub supported_readings: Vec<&'static str>,
20 pub context_value_count: usize,
21 pub restriction_map_count: usize,
22 pub property_consistent: bool,
23 pub dangling_restriction_count: usize,
24 pub theorem_claimed: bool,
25 pub members: Vec<CascadeValueFamilyMemberV0>,
26 pub restriction_maps: Vec<CascadeRestrictionMapV0>,
27}
28
29impl PartialEq for CascadeValueFamilyV0 {
30 fn eq(&self, other: &Self) -> bool {
31 self.schema_version == other.schema_version
32 && self.product == other.product
33 && self.framing == other.framing
34 && self.claim_level == other.claim_level
35 && self
36 .property_name
37 .to_property_name()
38 .same_as(&other.property_name.to_property_name())
39 && self.supported_readings == other.supported_readings
40 && self.context_value_count == other.context_value_count
41 && self.restriction_map_count == other.restriction_map_count
42 && self.property_consistent == other.property_consistent
43 && self.dangling_restriction_count == other.dangling_restriction_count
44 && self.theorem_claimed == other.theorem_claimed
45 && self.members == other.members
46 && self.restriction_maps == other.restriction_maps
47 }
48}
49
50impl Eq for CascadeValueFamilyV0 {}
51
52#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
53#[serde(rename_all = "camelCase")]
54pub struct CascadeContextV0 {
55 pub id: String,
56 #[serde(skip_serializing_if = "Option::is_none")]
57 pub parent_id: Option<String>,
58 pub selectors: Vec<String>,
59 pub conditions: Vec<String>,
60 pub layers: Vec<String>,
61}
62
63#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
64#[serde(rename_all = "camelCase")]
65pub struct CascadeValueFamilyMemberV0 {
66 pub context: CascadeContextV0,
67 pub value: AbstractPropertyValueV0,
68}
69
70#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
71#[serde(rename_all = "camelCase")]
72pub struct CascadeRestrictionMapV0 {
73 pub parent_context_id: String,
74 pub child_context_id: String,
75 pub morphism: CascadeMorphismV0,
76}
77
78#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
79#[serde(rename_all = "camelCase")]
80pub struct CascadeMorphismV0 {
81 pub kind: &'static str,
82 pub direction: &'static str,
83 pub preserves_property_name: bool,
84 pub evidence: Vec<&'static str>,
85}
86
87#[derive(Debug, Clone, Serialize)]
88#[serde(rename_all = "camelCase")]
89pub struct CascadeStalkEvaluationV0 {
90 pub schema_version: &'static str,
91 pub product: &'static str,
92 pub claim_level: &'static str,
93 pub property_name: AuthoredPropertyTextV0,
94 pub requested_context_id: String,
95 pub requested_context_exists: bool,
96 #[serde(skip_serializing_if = "Option::is_none")]
97 pub resolved_context_id: Option<String>,
98 pub restriction_path: Vec<String>,
99 pub used_restriction_map_count: usize,
100 pub bounded_by_context_count: usize,
101 pub bounded_resolution_ready: bool,
102 pub theorem_claimed: bool,
103 #[serde(skip_serializing_if = "Option::is_none")]
104 pub value: Option<AbstractPropertyValueV0>,
105 pub resolved: bool,
106 #[serde(skip_serializing_if = "Option::is_none")]
107 pub blocked_reason: Option<&'static str>,
108}
109
110impl PartialEq for CascadeStalkEvaluationV0 {
111 fn eq(&self, other: &Self) -> bool {
112 self.schema_version == other.schema_version
113 && self.product == other.product
114 && self.claim_level == other.claim_level
115 && self
116 .property_name
117 .to_property_name()
118 .same_as(&other.property_name.to_property_name())
119 && self.requested_context_id == other.requested_context_id
120 && self.requested_context_exists == other.requested_context_exists
121 && self.resolved_context_id == other.resolved_context_id
122 && self.restriction_path == other.restriction_path
123 && self.used_restriction_map_count == other.used_restriction_map_count
124 && self.bounded_by_context_count == other.bounded_by_context_count
125 && self.bounded_resolution_ready == other.bounded_resolution_ready
126 && self.theorem_claimed == other.theorem_claimed
127 && self.value == other.value
128 && self.resolved == other.resolved
129 && self.blocked_reason == other.blocked_reason
130 }
131}
132
133impl Eq for CascadeStalkEvaluationV0 {}
134
135#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
136#[serde(rename_all = "camelCase")]
137pub struct CascadeRestrictionCycleSummaryV0 {
138 pub schema_version: &'static str,
139 pub product: &'static str,
140 pub claim_level: &'static str,
141 pub cycle_detection_model: &'static str,
142 pub context_count: usize,
143 pub restriction_map_count: usize,
144 pub cycle_count: usize,
145 pub cycles: Vec<CascadeRestrictionCycleV0>,
146 pub theorem_claimed: bool,
147}
148
149#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
150#[serde(rename_all = "camelCase")]
151pub struct CascadeRestrictionCycleV0 {
152 pub path: Vec<String>,
153}
154
155pub fn summarize_context_indexed_cascade_value_family_v0(
156 property_name: AuthoredPropertyTextV0,
157 members: Vec<CascadeValueFamilyMemberV0>,
158 restriction_maps: Vec<CascadeRestrictionMapV0>,
159) -> CascadeValueFamilyV0 {
160 let mut members = members;
161 members.sort_by(|left, right| left.context.id.cmp(&right.context.id));
162 members.dedup_by(|left, right| left.context.id == right.context.id);
163
164 let mut restriction_maps = restriction_maps;
165 restriction_maps.sort();
166 restriction_maps.dedup();
167
168 let context_ids = members
169 .iter()
170 .map(|member| member.context.id.as_str())
171 .collect::<BTreeSet<_>>();
172 let property_consistent = members.iter().all(|member| {
173 property_value_name(&member.value)
174 .to_property_name()
175 .same_as(&property_name.to_property_name())
176 });
177 let dangling_restriction_count = restriction_maps
178 .iter()
179 .filter(|restriction| {
180 !context_ids.contains(restriction.parent_context_id.as_str())
181 || !context_ids.contains(restriction.child_context_id.as_str())
182 })
183 .count();
184 let restriction_map_count = restriction_maps.len();
185
186 CascadeValueFamilyV0 {
187 schema_version: "0",
188 product: "omena-abstract-value.cascade-value-family",
189 framing: "framingNeutralCascadeFamily",
190 claim_level: ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0,
191 property_name,
192 supported_readings: vec!["restrictionMapCompatible", "aggregationCompatible"],
193 context_value_count: members.len(),
194 restriction_map_count,
195 property_consistent,
196 dangling_restriction_count,
197 theorem_claimed: false,
198 members,
199 restriction_maps,
200 }
201}
202
203#[deprecated(
204 since = "0.4.0",
205 note = "use summarize_context_indexed_cascade_value_family_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
206)]
207pub fn summarize_cascade_value_family_v0(
208 property_name: AuthoredPropertyTextV0,
209 members: Vec<CascadeValueFamilyMemberV0>,
210 restriction_maps: Vec<CascadeRestrictionMapV0>,
211) -> CascadeValueFamilyV0 {
212 let mut family =
213 summarize_context_indexed_cascade_value_family_v0(property_name, members, restriction_maps);
214 family.supported_readings = vec!["presheafCompatible", "cosheafCompatible"];
215 family
216}
217
218pub fn derive_context_indexed_cascade_restriction_maps_v0(
219 members: &[CascadeValueFamilyMemberV0],
220) -> Vec<CascadeRestrictionMapV0> {
221 let context_ids = members
222 .iter()
223 .map(|member| member.context.id.as_str())
224 .collect::<BTreeSet<_>>();
225 let mut maps = members
226 .iter()
227 .filter_map(|member| {
228 let parent_id = member.context.parent_id.as_deref()?;
229 context_ids
230 .contains(parent_id)
231 .then(|| CascadeRestrictionMapV0 {
232 parent_context_id: parent_id.to_string(),
233 child_context_id: member.context.id.clone(),
234 morphism: context_indexed_cascade_refinement_morphism_v0(),
235 })
236 })
237 .collect::<Vec<_>>();
238 maps.sort();
239 maps.dedup();
240 maps
241}
242
243#[deprecated(
244 since = "0.4.0",
245 note = "use derive_context_indexed_cascade_restriction_maps_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
246)]
247pub fn derive_cascade_restriction_maps_v0(
248 members: &[CascadeValueFamilyMemberV0],
249) -> Vec<CascadeRestrictionMapV0> {
250 derive_context_indexed_cascade_restriction_maps_v0(members)
251 .into_iter()
252 .map(|mut restriction| {
253 restriction.morphism.evidence = vec![
254 "contextIndexedValueFamily",
255 "parentChildCascadeContext",
256 "noSheafTheoremClaim",
257 ];
258 restriction
259 })
260 .collect()
261}
262
263pub fn context_indexed_cascade_refinement_morphism_v0() -> CascadeMorphismV0 {
264 CascadeMorphismV0 {
265 kind: "contextRefinement",
266 direction: "parentToChildRestriction",
267 preserves_property_name: true,
268 evidence: vec![
269 "contextIndexedValueFamily",
270 "parentChildCascadeContext",
271 "noCategoricalGluingTheoremClaim",
272 ],
273 }
274}
275
276#[deprecated(
277 since = "0.4.0",
278 note = "use context_indexed_cascade_refinement_morphism_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
279)]
280pub fn cascade_context_refinement_morphism_v0() -> CascadeMorphismV0 {
281 let mut morphism = context_indexed_cascade_refinement_morphism_v0();
282 morphism.evidence = vec![
283 "contextIndexedValueFamily",
284 "parentChildCascadeContext",
285 "noSheafTheoremClaim",
286 ];
287 morphism
288}
289
290pub fn cascade_value_for_context<'a>(
291 family: &'a CascadeValueFamilyV0,
292 context_id: &str,
293) -> Option<&'a AbstractPropertyValueV0> {
294 family
295 .members
296 .iter()
297 .find(|member| member.context.id == context_id)
298 .map(|member| &member.value)
299}
300
301pub fn cascade_family_context_values(
302 family: &CascadeValueFamilyV0,
303) -> BTreeMap<String, AbstractPropertyValueV0> {
304 family
305 .members
306 .iter()
307 .map(|member| (member.context.id.clone(), member.value.clone()))
308 .collect()
309}
310
311pub fn evaluate_cascade_stalk_v0(
312 family: &CascadeValueFamilyV0,
313 context_id: &str,
314) -> CascadeStalkEvaluationV0 {
315 let values = cascade_family_context_values(family);
316 let requested_context_exists = values.contains_key(context_id);
317 let parent_by_child = family
318 .restriction_maps
319 .iter()
320 .map(|restriction| {
321 (
322 restriction.child_context_id.clone(),
323 restriction.parent_context_id.clone(),
324 )
325 })
326 .collect::<BTreeMap<_, _>>();
327 let mut restriction_path = Vec::new();
328 let mut current = context_id.to_string();
329 let bound = family.context_value_count.max(1);
330
331 for _ in 0..=bound {
332 restriction_path.push(current.clone());
333 if let Some(value) = values.get(¤t)
334 && !property_value_is_bottom(value)
335 {
336 return CascadeStalkEvaluationV0 {
337 schema_version: "0",
338 product: "omena-abstract-value.cascade-stalk-evaluation",
339 claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
340 property_name: family.property_name.clone(),
341 requested_context_id: context_id.to_string(),
342 requested_context_exists,
343 resolved_context_id: Some(current),
344 used_restriction_map_count: restriction_path.len().saturating_sub(1),
345 bounded_by_context_count: bound,
346 bounded_resolution_ready: true,
347 theorem_claimed: false,
348 value: Some(value.clone()),
349 resolved: true,
350 blocked_reason: None,
351 restriction_path,
352 };
353 }
354 let Some(parent) = parent_by_child.get(¤t) else {
355 break;
356 };
357 current = parent.clone();
358 }
359
360 CascadeStalkEvaluationV0 {
361 schema_version: "0",
362 product: "omena-abstract-value.cascade-stalk-evaluation",
363 claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
364 property_name: family.property_name.clone(),
365 requested_context_id: context_id.to_string(),
366 requested_context_exists,
367 resolved_context_id: None,
368 restriction_path,
369 used_restriction_map_count: 0,
370 bounded_by_context_count: bound,
371 bounded_resolution_ready: true,
372 theorem_claimed: false,
373 value: None,
374 resolved: false,
375 blocked_reason: Some("no non-bottom value found along bounded restriction path"),
376 }
377}
378
379pub fn summarize_cascade_restriction_cycles_v0(
380 family: &CascadeValueFamilyV0,
381) -> CascadeRestrictionCycleSummaryV0 {
382 let context_ids = family
383 .members
384 .iter()
385 .map(|member| member.context.id.clone())
386 .collect::<BTreeSet<_>>();
387 let mut adjacency = BTreeMap::<String, Vec<String>>::new();
388 for restriction in &family.restriction_maps {
389 adjacency
390 .entry(restriction.parent_context_id.clone())
391 .or_default()
392 .push(restriction.child_context_id.clone());
393 }
394 for targets in adjacency.values_mut() {
395 targets.sort();
396 targets.dedup();
397 }
398
399 let mut cycles = BTreeSet::<CascadeRestrictionCycleV0>::new();
400 for start in &context_ids {
401 collect_restriction_cycles_from(
402 start,
403 start,
404 &adjacency,
405 &mut Vec::new(),
406 &mut cycles,
407 family.context_value_count.max(1),
408 );
409 }
410 let cycles = cycles.into_iter().collect::<Vec<_>>();
411 CascadeRestrictionCycleSummaryV0 {
412 schema_version: "0",
413 product: "omena-abstract-value.cascade-restriction-cycle-summary",
414 claim_level: "fixtureWitnessBoundedRestrictionCycleDetection",
415 cycle_detection_model: "boundedRestrictionCycleWitnessNotCohomologyTheorem",
416 context_count: family.context_value_count,
417 restriction_map_count: family.restriction_map_count,
418 cycle_count: cycles.len(),
419 cycles,
420 theorem_claimed: false,
421 }
422}
423
424fn collect_restriction_cycles_from(
425 start: &str,
426 current: &str,
427 adjacency: &BTreeMap<String, Vec<String>>,
428 path: &mut Vec<String>,
429 cycles: &mut BTreeSet<CascadeRestrictionCycleV0>,
430 bound: usize,
431) {
432 if path.len() > bound {
433 return;
434 }
435 path.push(current.to_string());
436 if let Some(children) = adjacency.get(current) {
437 for child in children {
438 if child == start && path.len() > 1 {
439 let mut cycle = path.clone();
440 cycle.push(start.to_string());
441 cycles.insert(CascadeRestrictionCycleV0 {
442 path: canonical_restriction_cycle(cycle),
443 });
444 } else if !path.contains(child) {
445 collect_restriction_cycles_from(start, child, adjacency, path, cycles, bound);
446 }
447 }
448 }
449 path.pop();
450}
451
452fn canonical_restriction_cycle(mut cycle: Vec<String>) -> Vec<String> {
453 if cycle.len() <= 2 {
454 return cycle;
455 }
456 cycle.pop();
457 let Some((start_index, _)) = cycle
458 .iter()
459 .enumerate()
460 .min_by(|left, right| left.1.cmp(right.1))
461 else {
462 return cycle;
463 };
464 let mut canonical = (0..cycle.len())
465 .map(|offset| cycle[(start_index + offset) % cycle.len()].clone())
466 .collect::<Vec<_>>();
467 canonical.push(canonical[0].clone());
468 canonical
469}
470
471fn property_value_is_bottom(value: &AbstractPropertyValueV0) -> bool {
472 matches!(value, AbstractPropertyValueV0::Bottom { .. })
473}
474
475fn property_value_name(value: &AbstractPropertyValueV0) -> &AuthoredPropertyTextV0 {
476 match value {
477 AbstractPropertyValueV0::Bottom { property_name }
478 | AbstractPropertyValueV0::Exact { property_name, .. }
479 | AbstractPropertyValueV0::FiniteSet { property_name, .. }
480 | AbstractPropertyValueV0::CustomPropertyReference { property_name, .. }
481 | AbstractPropertyValueV0::Top { property_name } => property_name,
482 }
483}