Extend interpreter to do symbolic evaluation

[edsko]

At the moment the evaluator (Interpreter.hs) does not do symbolic evaluation, but it would be nice if it did. For example (see tests/backend/passfold-eval-2.wpl), we could change something like

var x := 0;
for i in [0, 5] { x := x + x }

with

x + + x + x + x + x

Or, somewhat more useful, we could replace

var x : arr[2] int;
x[0] := a;
x[1] := b;
return x;

with just

{a, b}

This latter example is useful, because there is a pass in the compiler (asgn-letref) that attempts to recognize something of the form

x[start:len] := var y in { ... ; return y }

and changes this so that the operations on y follows by a copy to x become direct operation on x instead. However, this pass recognizes only very fixed patterns. If the evaluator did symbolic execution, we could make this much more general.

Symbolic execution however is not so easy (see tests/backend/passfold-eval-3.wpl for some examples). For example, consider a simple swap algorithm such as

var tmp in {
  tmp := x;
  x := y;
  y := tmp;
}

If we do symbolic execution, we record that we have a local variable tmp; then when we execute the assignment tmp := x we record that tmp has (symbolic) value x; but now when we see the assignment to x we cannot execute it because x is a free variable, so we have to leave the assigment as is. Then when we get to the y := tmp assignment, it's not no longer okay to simply lookup the value of tmp and conclude it must be x. Instead, we must make sure that when we assign to x we write the explicit assignment to tmp (because the symbolic value of tmp mentions x and hence would no longer be valid after this assignment to x). Note that this would be simpler if the program was in SSA form, because we would have a unique reference point for each variable.