Modify the syntax to include a new construct [Do] and restrict [Eff] to values

Following @fpottier's suggestion, we include a new language construct Do that takes an arbitrary expression e as its only argument. The meaning of Do e is to launch the raising of an effect once the evaluation of e is complete. This is captured by the following new reduction rule:

(Do (Val v)); σ → (Eff v EmptyCtx); σ

There are two advantages in doing this: (1) the syntax of evaluation contexts become simpler because we no longer need to consider the context Eff [] k and (2) the users of the language can ignore the existence of Eff which is now only a detail of the operational semantics.