Function ground_const

crates/compile/src/ground.rs:100–148

(
  constant: &ConstantInfo,
  env: &Env,
  univs: &[Name],
  binds: usize,
  stt: &mut GroundState,
)

  match constant {
    ConstantInfo::AxiomInfo(val) => &val.cnst.level_params,
    ConstantInfo::DefnInfo(val) => &val.cnst.level_params,
    ConstantInfo::ThmInfo(val) => &val.cnst.level_params,
    ConstantInfo::OpaqueInfo(val) => &val.cnst.level_params,
    ConstantInfo::QuotInfo(val) => &val.cnst.level_params,
    ConstantInfo::InductInfo(val) => &val.cnst.level_params,
    ConstantInfo::CtorInfo(val) => &val.cnst.level_params,
    ConstantInfo::RecInfo(val) => &val.cnst.level_params,
  }
}

#[derive(Default)]
struct GroundState {
  expr_cache: FxHashSet<(usize, Expr)>,
  univ_cache: FxHashSet<Level>,
}

fn ground_const(
  constant: &ConstantInfo,
  env: &Env,
  univs: &[Name],
  binds: usize,
  stt: &mut GroundState,
) -> Result<(), GroundError> {
  match constant {
    ConstantInfo::AxiomInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)
    },
    ConstantInfo::DefnInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)?;
      ground_expr(&val.value, env, univs, binds, stt)
    },
    ConstantInfo::ThmInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)?;
      ground_expr(&val.value, env, univs, binds, stt)
    },
    ConstantInfo::OpaqueInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)?;
      ground_expr(&val.value, env, univs, binds, stt)
    },
    ConstantInfo::QuotInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)
    },
    ConstantInfo::InductInfo(val) => {
      for ctor in &val.ctors {
        let ci = env.get(ctor).map(|e| e.cloned());
        match ci.as_ref() {
          Some(ConstantInfo::CtorInfo(_)) => (),
          _ => {
            return Err(GroundError::Indc(Box::new((val.clone(), ci))));
          },
        }
      }