Method build_rule_rhs

crates/kernel/src/inductive.rs:3572–3830

Build the rule RHS for a single constructor. The RHS is: `λ (params) (motives) (minors) (fields), minor[idx] fields ihs` where each IH = `λ (xs...), rec[target] params motives minors indices (field xs...)`

(
    &mut self,
    member_idx: usize,
    ctor_local_idx: usize,
    ctor_id: &KId<M>,
    member: &FlatBlockMember<M>,
    flat: &[FlatBlockMember<M>],
    peer_recs: &[KId<M>],
    rec_ty_for_memb

    let is_large = univ_offset > 0;
    let n_params = u64_to_usize::<M>(n_params_u64)?;
    let mut generated_with_rules = generated_snapshot;

    for gi in 0..flat.len() {
      let member = &flat[gi];
      let rec_ty_for_member = generated_with_rules[gi].ty.clone();
      let mut rules = Vec::with_capacity(member.ctors.len());
      for (ci, ctor_id) in member.ctors.iter().enumerate() {
        let ctor_fields = match self.get_const(ctor_id)? {
          KConst::Ctor { fields, .. } => fields,
          _ => {
            return Err(TcError::Other(
              "populate_recursor_rules_from_block: ctor not found".into(),
            ));
          },
        };
        let rhs = self.build_rule_rhs(
          gi,
          ci,
          ctor_id,
          member,
          &flat,
          &peer_recs,
          &rec_ty_for_member,
          n_params,
          is_large,
          univ_offset,
        )?;
        rules.push(super::constant::RecRule {
          ctor: ctor_id.name.clone(),
          fields: ctor_fields,
          rhs,
        });
      }
      generated_with_rules[gi].rules = rules;
    }

    if let Some(cached) = self.env.recursor_cache.get_mut(ind_block_id) {
      if cached.len() != generated_with_rules.len() {
        return Err(TcError::Other(format!(
          "populate_recursor_rules_from_block: cache changed length: cached={} generated={}",
          cached.len(),
          generated_with_rules.len()
        )));
      }
      for (dst, src) in cached.iter_mut().zip(generated_with_rules.into_iter())
      {
        dst.rules = src.rules;
      }
    }

    Ok(())
  }

  /// Build the rule RHS for a single constructor.
  ///
  /// The RHS is: `λ (params) (motives) (minors) (fields), minor[idx] fields ihs`
  /// where each IH = `λ (xs...), rec[target] params motives minors indices (field xs...)`
  fn build_rule_rhs(