( info: &LeanSourceInfo, stt: &CompileState, bytes: &mut Vec<u8>, )
| 1524 | stack.push(Frame::Compile(ty.clone())); |
| 1525 | }, |
| 1526 | |
| 1527 | ExprData::LetE(name, ty, val, body, non_dep, _) => { |
| 1528 | let name_addr = compile_name(name, stt); |
| 1529 | stack.push(Frame::BuildLet(name_addr, *non_dep)); |
| 1530 | stack.push(Frame::Compile(body.clone())); |
| 1531 | stack.push(Frame::Compile(val.clone())); |
| 1532 | stack.push(Frame::Compile(ty.clone())); |
| 1533 | }, |
| 1534 | |
| 1535 | ExprData::Lit(Literal::NatVal(n), _) => { |
| 1536 | let addr = store_nat(n, stt); |
| 1537 | let (ref_idx, _) = cache.refs.insert_full(addr); |
| 1538 | results.push(Expr::nat(ref_idx as u64)); |
| 1539 | cache.arena_roots.push(cache.arena.alloc(ExprMetaData::Leaf)); |
| 1540 | }, |
| 1541 | |
| 1542 | ExprData::Lit(Literal::StrVal(s), _) => { |
| 1543 | let addr = store_string(s, stt); |
| 1544 | let (ref_idx, _) = cache.refs.insert_full(addr); |
| 1545 | results.push(Expr::str(ref_idx as u64)); |
| 1546 | cache.arena_roots.push(cache.arena.alloc(ExprMetaData::Leaf)); |
| 1547 | }, |
| 1548 | |
| 1549 | ExprData::Proj(type_name, idx, struct_val, _) => { |
| 1550 | let idx_u64 = nat_to_u64(idx, "proj index too large")?; |
| 1551 |
no test coverage detected