[kernel] termination checking backtracks on stuck case

The strategy is to backtrack when a constant is in head
position: we first try to see if the arguments are guarded,
if not we unfold.

Since `Case` is represented as a head (rather than as a context
as the reduction machine does) we did not backtrack there
and reduce (including delta) the scrutinized in order to
fire the iota redex.

This commit adds a choice point in that specific case, and
reduces eagerly (not step by step) the scrutinized in case
of failure.

0 files changed, 0 insertions, 0 deletions