Implement runtime constraint checks on assignment

[alastairreid]

Assignments (including assigning actual arguments to a function's formal arguments) should perform a runtime constraint check but currently does not do so.

let x : {0..7} := e;

should be expanded into code that performs a runtime check such as the following (though we might want a different error message if the assertion fails #115)

let tmp := e;
assert tmp in {0..7};
let x := tmp;