PLFA 2025 10 27: change how eval is defined (#1141)

Following a suggestion of Conrad Watt, changed the definition of `eval`
to add information. Recall that the evaluator takes an amount of gas and
a term and returns a reduction sequence. If the evaluator runs out of
gas it returns a sequence of length equal to the amount of gas, while if
it terminates in returns a sequence of length less than the amount of
gas and ending in a value.

---------

Co-authored-by: Wen Kokke <wenkokke@users.noreply.github.com>

Author: wadler