Convert a Nat literal to constructor form: 0 → Nat.zero, n+1 → Nat.succ(n-1).
(&mut self, val: &Nat)
| 1664 | e: &KExpr<M>, |
| 1665 | depth: u16, |
| 1666 | ) -> Result<(KExpr<M>, Nat), TcError<M>> { |
| 1667 | Ok( |
| 1668 | self |
| 1669 | .nat_offset(e, depth)? |
| 1670 | .unwrap_or_else(|| (e.clone(), Nat(num_bigint::BigUint::ZERO))), |
| 1671 | ) |
| 1672 | } |
| 1673 | |
| 1674 | /// Syntactic, no-delta evaluator for Nat offset constants. |
| 1675 | /// |
| 1676 | /// This is intentionally weaker than WHNF: it only recognizes already |
| 1677 | /// exposed Nat literals/constructors and primitive Nat arithmetic whose |
| 1678 | /// arguments are themselves syntactically evaluable. It is used to avoid |
| 1679 | /// rewriting closed arithmetic offsets before `try_reduce_nat` can compute |
| 1680 | /// them, and to evaluate the literal offset side of `Nat.add`. |
| 1681 | fn eval_nat_offset_literal( |
| 1682 | &mut self, |
| 1683 | e: &KExpr<M>, |
| 1684 | depth: u16, |
| 1685 | ) -> Option<Nat> { |
| 1686 | const MAX_NAT_OFFSET_EVAL_DEPTH: u16 = 256; |
| 1687 | if depth >= MAX_NAT_OFFSET_EVAL_DEPTH { |
| 1688 | return None; |
| 1689 | } |
| 1690 | |
| 1691 | if let Some(n) = extract_nat_value(e, &self.prims) { |
| 1692 | return Some(n); |
no test coverage detected