WASM: Variable Scoping

[pkel]

In its current state, the WASM backend does not correctly handle variable scoping: Wasm variables are function-scoped and the translation assumes that Imp variable names are unique. In case of nested variables with the same name we will run into unexpected behaviour.

This is not yet fixed because we were unsure about the best way of solving the problem.

I claim it's feasible (and fun) to implement scoping in the OCaml code that translates Imp to Wasm. This would have the additional benefit, that local (function scoped) variables could be reused for multiple block-scoped Imp variables, e.g. after leaving a block. Currently there is one function scoped variable per variable name occurring in the Imp function.

On the other hand, it probably makes sense to do this error prone step in the proof assistant. For that, we would probably want to have another intermediate representation that is more Wasm-like (See #146).

[pkel]

Addressed in 8766b38 using OCaml. At some point it will be moved to Coq as part of #146.