Symbolic evaluator

[romac]

Following the discussion in epfl-lara/stainless#104:

@jad-hamza:
For the general case with free variables, we could take inspiration from the Coq "simpl" tactic. This tactic simplifies the terms that appear in your goal (or in your premises) by applying reductions rules (beta-reduction, etc.). But it doesn't evaluate blindly, and tries to only apply reductions that make the terms more readable (and to avoid non-termination).

For instance, given the definitions in #96, plus(n,m) would not be simplified further (even though there is a valid beta-reduction rule that can be applied), but plus(S(n),m) would be simplified to S(plus(n,m)).

@samarion:
For simplifications of non-ground terms, I also agree with @jad-hamza. Note that Inox actually already does this pretty extensively in SimplifierWithPC. However, no beta-reduction is performed for named functions, so that could be an interesting new simplification to consider. The challenge is to choose good heuristics about when a function inlining can be considered 'useful'. Possibly basing ourselves off the simp tactic could indeed be useful, but I would prefer automatic this as much as possible.

[romac]

Closing as per #61 (comment).