Compile a Lean DataValue to Ixon DataValue.
(dv: &LeanDataValue, stt: &CompileState)
| 1454 | .map_or_else(|| "?".into(), |n| n.pretty()); |
| 1455 | CompileError::MissingConstant { |
| 1456 | name: type_name.pretty(), |
| 1457 | caller: format!("{who} @ compile_expr(Proj)"), |
| 1458 | } |
| 1459 | })?; |
| 1460 | |
| 1461 | let (ref_idx, _) = cache.refs.insert_full(type_addr.clone()); |
| 1462 | let name_addr = compile_name(type_name, stt); |
| 1463 | |
| 1464 | stack.push(Frame::BuildProj(ref_idx as u64, idx_u64, name_addr)); |
| 1465 | stack.push(Frame::Compile(struct_val.clone())); |
| 1466 | }, |
| 1467 | |
| 1468 | ExprData::Mdata(kv, inner, _) => { |
| 1469 | // Compile KV map |
| 1470 | let mut pairs = Vec::new(); |
| 1471 | for (k, v) in kv { |
| 1472 | let k_addr = compile_name(k, stt); |
| 1473 | let v_data = compile_data_value(v, stt); |
| 1474 | pairs.push((k_addr, v_data)); |
| 1475 | } |
| 1476 | // Mdata becomes a separate arena node wrapping inner |
| 1477 | stack.push(Frame::WrapMdata(vec![pairs])); |
| 1478 | stack.push(Frame::Compile(inner.clone())); |
| 1479 | }, |
| 1480 | |
| 1481 | ExprData::Fvar(n, _) => { |
| 1482 | return Err(CompileError::UnsupportedExpr { |
| 1483 | desc: format!("free variable '{}'", n.pretty()), |
| 1484 | }); |
| 1485 | }, |
| 1486 |
no test coverage detected