Accelerator.SM121.Lowering

A select whose arms may be expensive redexes. The machine evaluates a function's arguments before the call, so a table call (or a union, a drain, a rebuilt prefix) sitting in a plain select's arm runs for every cell whether the arm is taken or not (measured: the read-after-write table costs ~450 dispatch steps, paid per pending entry per operand register -- two thirds of the schedule). Both arms thunked behind lambdas are already values when passed; the taken one alone runs when the result is applied. Plain `sm121LowerSelect` stays for cheap arms, where the two closures would cost more than they save.

471def sm121LowerSelectLazy =
472  (lambda erased value : Type 0 .
473    (lambda unrestricted condition : Nat .
474      (lambda unrestricted whenTrue : (pi unrestricted u : Nat . value) .
475        (lambda unrestricted whenFalse : (pi unrestricted u : Nat . value) .
476          (app
477            (nat-eliminate
478              (lambda unrestricted current : Nat . (pi unrestricted u : Nat . value))
479              whenFalse
480              (lambda unrestricted predecessor : Nat .
481                (lambda unrestricted induction : (pi unrestricted u : Nat . value) . whenTrue))
482              condition)
483            zero)))))