Function preseed_expr_tables

crates/compile/src/compile.rs:545–585

(
  exprs: &[(&LeanExpr, &[Name])],
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
  caller: &str,
)

}

fn univ_params_key(univ_params: &[Name]) -> Address {
  let mut hasher = blake3::Hasher::new();
  for name in univ_params {
    hasher.update(name.get_hash().as_bytes());
  }
  Address::from_blake3_hash(hasher.finalize())
}

fn collect_expr_tables(
  expr: &LeanExpr,
  univ_params: &[Name],
  mut_ctx: &MutCtx,
  cache: &mut BlockCache,
  stt: &CompileState,
  refs: &mut Vec<Address>,
  univs: &mut Vec<Arc<Univ>>,
  seen_exprs: &mut FxHashMap<(Address, Address), ()>,
  caller: &str,
) -> Result<(), CompileError> {
  let ctx_key = univ_params_key(univ_params);
  let mut stack = vec![expr];
  while let Some(e) = stack.pop() {
    let key = Address::from_blake3_hash(*e.get_hash());
    if seen_exprs.insert((key, ctx_key.clone()), ()).is_some() {
      continue;
    }

    match e.as_data() {
      ExprData::Bvar(..) => {},
      ExprData::Sort(level, _) => {
        univs.push(compile_univ(level, univ_params, cache)?);
      },
      ExprData::Const(name, levels, _) => {
        for level in levels {
          univs.push(compile_univ(level, univ_params, cache)?);
        }
        if !mut_ctx.contains_key(name) {
          let const_addr = stt.resolve_addr(name).ok_or_else(|| {
            CompileError::MissingConstant {
              name: name.pretty(),
              caller: format!("{caller} @ preseed(Const)"),
            }
          })?;
          refs.push(const_addr);