Function ground_expr

crates/compile/src/ground.rs:150–203

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

            return Err(GroundError::Indc(Box::new((val.clone(), ci))));
          },
        }
      }
      ground_expr(&val.cnst.typ, env, univs, binds, stt)
    },
    ConstantInfo::CtorInfo(val) => {
      ground_expr(&val.cnst.typ, env, univs, binds, stt)
    },
    ConstantInfo::RecInfo(val) => {
      for rule in &val.rules {
        ground_expr(&rule.rhs, env, univs, binds, stt)?;
      }
      ground_expr(&val.cnst.typ, env, univs, binds, stt)
    },
  }
}

fn ground_expr(
  expr: &Expr,
  env: &Env,
  univs: &[Name],
  binds: usize,
  stt: &mut GroundState,
) -> Result<(), GroundError> {
  let key = (binds, expr.clone());
  if stt.expr_cache.contains(&key) {
    return Ok(());
  }
  stt.expr_cache.insert(key);
  match expr.as_data() {
    ExprData::Mdata(_, e, _) => ground_expr(e, env, univs, binds, stt),
    ExprData::Bvar(idx, _) => {
      if *idx >= Nat(binds.into()) {
        return Err(GroundError::Var(expr.clone(), binds));
      }
      Ok(())
    },
    ExprData::Sort(level, _) => ground_level(level, univs, stt),
    ExprData::Const(name, levels, _) => {
      for level in levels {
        ground_level(level, univs, stt)?;
      }
      if !env.contains_key(name) {
        return Err(GroundError::Ref(name.clone()));
      }
      Ok(())
    },
    ExprData::App(f, a, _) => {
      ground_expr(f, env, univs, binds, stt)?;
      ground_expr(a, env, univs, binds, stt)
    },
    ExprData::Lam(_, t, b, ..) | ExprData::ForallE(_, t, b, ..) => {
      ground_expr(t, env, univs, binds, stt)?;
      ground_expr(b, env, univs, binds + 1, stt)
    },
    ExprData::LetE(_, t, v, b, ..) => {
      ground_expr(t, env, univs, binds, stt)?;
      ground_expr(v, env, univs, binds, stt)?;