| 5222 | let mut env = KEnv::<Meta>::new(); |
| 5223 | let e = LeanExpr::app( |
| 5224 | LeanExpr::sort(Level::zero()), |
| 5225 | LeanExpr::sort(Level::zero()), |
| 5226 | ); |
| 5227 | let k1 = lean_expr_to_zexpr_with_kenv(&e, &[], &mut env, None, None); |
| 5228 | let k2 = lean_expr_to_zexpr_with_kenv(&e, &[], &mut env, None, None); |
| 5229 | // Cache hit → same interned result. |
| 5230 | assert!(k1.ptr_eq(&k2)); |
| 5231 | } |
| 5232 | |
| 5233 | #[test] |
| 5234 | fn callsite_ingress_uses_canon_meta_for_collapsed_canonical_arg() { |
| 5235 | let head_name = mk_name("Head.rec"); |
| 5236 | let arg_name = mk_name("GoodArg"); |
| 5237 | let bad_name = mk_name("BadArg"); |
| 5238 | let head_name_addr = lean_name_to_addr(&head_name); |
| 5239 | let arg_name_addr = lean_name_to_addr(&arg_name); |
| 5240 | let bad_name_addr = lean_name_to_addr(&bad_name); |
| 5241 | let head_ref_addr = Address::hash(b"head-content"); |
| 5242 | let arg_ref_addr = Address::hash(b"arg-content"); |
| 5243 | |
| 5244 | let mut names = FxHashMap::default(); |
| 5245 | names.insert(head_name_addr.clone(), head_name.clone()); |
| 5246 | names.insert(arg_name_addr.clone(), arg_name.clone()); |
| 5247 | names.insert(bad_name_addr.clone(), bad_name); |
| 5248 | |
| 5249 | let mut arena = ExprMeta::default(); |
| 5250 | let bad_entry_meta = arena.alloc(ExprMetaData::Ref { name: bad_name_addr }); |
| 5251 | let arg_canon_meta = arena.alloc(ExprMetaData::Ref { name: arg_name_addr }); |
| 5252 | let root = arena.alloc(ExprMetaData::CallSite { |
| 5253 | name: head_name_addr, |
| 5254 | entries: vec![CallSiteEntry::Collapsed { |
| 5255 | sharing_idx: 0, |
| 5256 | meta: bad_entry_meta, |
| 5257 | }], |
| 5258 | canon_meta: vec![arg_canon_meta], |
| 5259 | orig_head: None, |
| 5260 | }); |
| 5261 | |
| 5262 | let ixon = IxonExpr::app( |