MCPcopy Create free account
hub / github.com/argumentcomputer/ix / check_recursor

Method check_recursor

crates/kernel/src/inductive.rs:4014–4034  ·  view source on GitHub ↗

Validate a recursor block. A pure recursor block is checked once and the result is shared by all sibling recursors.

(&mut self, id: &KId<M>)

Source from the content-addressed store, hash-verified

4012 "populate_recursor_rules_from_block: flat/generated length mismatch: flat={} generated={}",
4013 flat.len(),
4014 generated_snapshot.len()
4015 )));
4016 }
4017 if generated_snapshot
4018 .iter()
4019 .zip(flat.iter())
4020 .all(|(g, member)| g.rules.len() == member.ctors.len())
4021 {
4022 return Ok(());
4023 }
4024
4025 let n_motives = flat.len() as u64;
4026 let n_minors = flat.iter().try_fold(0u64, |sum, member| {
4027 checked_metadata_sum::<M>(
4028 "generated recursor minors",
4029 &[sum, member.ctors.len() as u64],
4030 )
4031 })?;
4032 let prefix_base = checked_metadata_sum::<M>(
4033 "generated recursor params + motives + minors",
4034 &[n_params_u64, n_motives, n_minors],
4035 )?;
4036
4037 // Position-by-position alignment.

Callers

nothing calls this directly

Calls 7

try_get_blockMethod · 0.80
check_recursor_memberMethod · 0.80
check_recursor_blockMethod · 0.80
get_constMethod · 0.45
cloneMethod · 0.45
getMethod · 0.45
insertMethod · 0.45

Tested by

no test coverage detected