Stratify opcodes and instructions.

We call opcodes the instructions that do not take subprograms as argument nor have special treatment in the type-checker or evaluator. Most of the instructions in Michelson fall into this category, putting them aside makes the number of constructors of the instruction ASTs much smaller which is needed when reasoning on the syntax.

In particular, many optimisations at the Michelson level require to reason about several terms in these ASTs by nesting destructs which was not tractable with more than 80 constructors.

Moreover, this MR introduces a distinction between instructions and instruction sequences that simplify the splitting of smart contracts for functional verification.

This MR also improves the readability of smart contracts in the typed syntax by providing scoped notations very close to Michelson code.