( cnst: &'a MutConst, exprs: &mut Vec<(&'a LeanExpr, &'a [Name])>, )
| 585 | caller: format!("{caller} @ preseed(Const)"), |
| 586 | } |
| 587 | })?; |
| 588 | refs.push(const_addr); |
| 589 | } |
| 590 | }, |
| 591 | ExprData::App(fun, arg, _) => { |
| 592 | stack.push(arg); |
| 593 | stack.push(fun); |
| 594 | }, |
| 595 | ExprData::Lam(_, ty, body, _, _) |
| 596 | | ExprData::ForallE(_, ty, body, _, _) => { |
| 597 | stack.push(body); |
| 598 | stack.push(ty); |
| 599 | }, |
| 600 | ExprData::LetE(_, ty, value, body, _, _) => { |
| 601 | stack.push(body); |
| 602 | stack.push(value); |
| 603 | stack.push(ty); |
| 604 | }, |
| 605 | ExprData::Lit(Literal::NatVal(n), _) => { |
| 606 | refs.push(store_nat(n, stt)); |
| 607 | }, |
| 608 | ExprData::Lit(Literal::StrVal(s), _) => { |
| 609 | refs.push(store_string(s, stt)); |
| 610 | }, |
| 611 | ExprData::Proj(type_name, _, struct_val, _) => { |
| 612 | let type_addr = stt.resolve_addr(type_name).ok_or_else(|| { |
| 613 | CompileError::MissingConstant { |
| 614 | name: type_name.pretty(), |
no test coverage detected