"Support" for `choose` in evaluators.
"Support" for `choose` in evaluators.

What this commit really introduces is a graceful failure when asked to
evaluate a `choose` expression. In particular, it makes it possible for
codegen evaluator to compile functions that contain `choose`
expressions, and even evaluate them, as long as the execution path
doesn't meet a `choose` expressions.

epfl-lara/stainless,epfl-lara/stainless,epfl-lara/stainless,epfl-lara/stainless