Try to reduce a projection-headed application: App(Prj(S, i, v), args...). Returns Some((reduced_proj, remaining_args)) if the projection reduced.
(
&mut self,
e: &KExpr<M>,
flags: WhnfFlags,
)
| 1507 | } |
| 1508 | |
| 1509 | fn apply_iota_arg( |
| 1510 | &mut self, |
| 1511 | result: KExpr<M>, |
| 1512 | arg: &KExpr<M>, |
| 1513 | transient: bool, |
| 1514 | ) -> KExpr<M> { |
| 1515 | if transient { |
| 1516 | if let ExprData::Lam(_, _, _, body, _) = result.data() { |
| 1517 | let body = body.clone(); |
| 1518 | return subst_no_intern(&body, arg, 0); |
| 1519 | } |
| 1520 | KExpr::app(result, arg.clone()) |
| 1521 | } else { |
| 1522 | self.intern(KExpr::app(result, arg.clone())) |
| 1523 | } |
| 1524 | } |
| 1525 | |
| 1526 | /// Nat literal iota can create a long chain of distinct predecessor terms. |
| 1527 | /// These terms are useful only while the current WHNF is executing; keeping |
| 1528 | /// each one in the global WHNF caches makes RSS linear in the literal. |
| 1529 | /// Allocation-free spine probe: head expression and arg count without |
| 1530 | /// materializing the spine. The transient-nat probes below run on |
| 1531 | /// *every* whnf call **before** the cache lookup, so they must not |
| 1532 | /// heap-allocate on the (overwhelmingly common) non-Nat-recursor path — |
| 1533 | /// the previous implementation paid two `collect_app_spine` Vec |
| 1534 | /// allocations plus a `KConst::Recr` clone per call, defeating the |
| 1535 | /// cache on the hottest path in a full check. (Ported from jcb/fixes |
| 1536 | /// H-15.) |
no test coverage detected