Function resolve_kvmap

crates/ixon/src/metadata.rs:313–354

Resolve an Ixon KVMap (address-based) to Lean-level MData (name/value pairs). Used by kernel ingress to convert expression metadata from the content-addressed Ixon representation to the named kernel representation.

(
  kvm: &KVMap,
  ixon_env: &super::env::Env,
)

      },
      I::Axio { name, lvls, arena: a, .. }
      | I::Quot { name, lvls, arena: a, .. } => {
        names.push(name.clone());
        names.extend(lvls.iter().cloned());
        arena = Some(a);
      },
      I::Indc { name, lvls, ctors, all, ctx, arena: a, .. } => {
        names.push(name.clone());
        names.extend(lvls.iter().cloned());
        names.extend(ctors.iter().cloned());
        names.extend(all.iter().cloned());
        names.extend(ctx.iter().cloned());
        arena = Some(a);
      },
      I::Ctor { name, lvls, induct, arena: a, .. } => {
        names.push(name.clone());
        names.extend(lvls.iter().cloned());
        names.push(induct.clone());
        arena = Some(a);
      },
      I::Rec { name, lvls, rules, all, ctx, arena: a, .. } => {
        names.push(name.clone());
        names.extend(lvls.iter().cloned());
        names.extend(rules.iter().cloned());
        names.extend(all.iter().cloned());
        names.extend(ctx.iter().cloned());
        arena = Some(a);
      },
      I::Muts { all, .. } => {
        for class in all {
          names.extend(class.iter().cloned());
        }
      },
    }
    if let Some(a) = arena {
      for node in &a.nodes {
        match node {
          ExprMetaData::Leaf | ExprMetaData::App { .. } => {},
          ExprMetaData::Binder { name, .. }
          | ExprMetaData::LetBinder { name, .. }
          | ExprMetaData::Ref { name }
          | ExprMetaData::CallSite { name, .. } => names.push(name.clone()),
          ExprMetaData::Prj { struct_name, .. } => {
            names.push(struct_name.clone());
          },
          ExprMetaData::Mdata { mdata, .. } => {