+ | _,TermLambda _
+ | _,TermPrimfun _
+ | _,TermConstructor _
+ | _,TermDestructor _
+ | _,TermLiteral _ -> AlreadyResult (result_of_term term)
+
+ | fi,TermVar var -> ...
+
+ (* notice we never evaluate a yes/no branch until it is chosen *)
+ | _,TermIf((_,TermLiteral(Bool true)),yes,no) ->
+ ReducedTo yes
+ | _,TermIf((_,TermLiteral(Bool false)),yes,no) ->
+ ReducedTo no
+ | fi,TermIf(test,yes,no) ->
+ (match reduce_head_once test env with
+ | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
+ | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
+ | ReducedTo test' -> ReducedTo(fi,TermIf(test',yes,no)))