Avoid reducing expressions in WHNF more than once

[majjoha]

Currently, in the case where we have an expression which is already in WHNF, we attempt to reduce it more than once. By using a tag to indicate whether it has already been reduced to WHNF, we could avoid this.