Extraction of user-defined effects (#886)

[victor-dumitrescu]

Code which uses non-primitive effects is extracted using a simple approach, similar to the one used for SMT encoding. Terms which have a reifiable computation type are reified using the normalizer, inlining applications of return and bind.

To avoid duplication, I also refactored the relevant bits from FStar.SMTEncoding.Encode.fs into separate functions in FStar.TypeChecker.Util.fs. Other additions include fixes for some issues that only became apparent when attempting to extract code with user-defined effects, including a fix for #1001 due to @mtzguido.

Currently, effect actions are extracted as projectors of the effect, belonging to a namespace that is also named after the effect (e.g. action get for effect RAND is extracted as uu___RAND___proj__RAND__item__get). This works, but is perhaps a bit brittle and convoluted. One potential improvement we discussed was to extract effect definitions as modules (so in the previous example, we would get something like RAND.get). Implementing this would require supporting submodules in the extracted ML syntax.

4/05/16: For the naming issue, the solution used in the end is to extract both actions and bind and return as projectors and to not qualify them with the effect name (e.g. __proj__EFF__item__bind)