open should be forgotten at the end of a module

[andrejbauer]

An open statement works forever for printing. It should only have an effect until the end of the module in which it appears.

[andrejbauer]

As it turns out, there are more problems than just printing:

1. Forbidden bound variable names are also remembered forever.
2. If a module raises an exception or runs an unhandled operation, then its effects (adding rules to nucleus, definitions of types, etc.) are forgotten, but not any changes it made to references.

We need to think about the top-level monad and the interaction between various effects.

[andrejbauer]

Following OCaml, if a module raises an exception, it should be undefined.

[andrejbauer]

The following top-level interaction is a bit worrisome:

# let secret = ref ML.None ;;
val secret :> ref (ML.option _α) = ref ML.None
# exception Die ;;
Exception Die is declared.
# module M = struct rule A type ;; secret := ML.Some A ;; raise Die ;; end ;;
Processing module M
Rule M.A is postulated.
- :> mlunit = ()
File "?", line 2, characters 57-65:
Runtime error: uncaught exception Die
# M.A ;;
File "?", line 2, characters 1-3:
Type error: unknown name M.A
# let (ML.Some ?illegal) = !secret ;;
val illegal :> _α = ⊢ M.A type
# illegal ;;
- :> _α = ⊢ M.A type