The register plan, 1 when it holds for the shape: an admitted shape's
program names exactly the registers below its allocation's span (so its
derived register count is the allocation's, and no index wrapped). The
program sits under the admitted branch's binder, not in an argument of
naturalSelect: for an open shape the admission can be undecided, and the
checker's weak head of a stuck select quotes (and so evaluates) every
argument it captured -- here a program generated for an open shape, about
40 s per cell, where the binder keeps it unevaluated.
312def linearStepSM86RegisterPlanHolds =
313 (lambda unrestricted m : Nat . (lambda unrestricted k : Nat .
314 (nat-eliminate
315 (lambda unrestricted admitted : Nat . Nat)
316 1
317 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
318 (naturalEqual (sm86RegisterSpan (linearStepSM86ProgramFor m k)) (linearStepSM86RegisterSpanFor m k))))
319 (linearStepSM86ShapeAdmitted m k))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.