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.