InstructionSequenceValidator

Validator of sequences of Instruction nodes.

From

Typing of instruction sequences is defined recursively.

Empty Instruction Sequence: ϵ

• The empty instruction sequence is valid with type [t*] => [t*], for any sequence of value types t*.

Non-empty Instruction Sequence: instr* instrN

• The instruction sequence instr* must be valid with type [t*^1] => [t*2], for some sequences of value types t*^1 and t*^2.
• The instruction instrN must be valid with type [t*] => [t*^3], for some sequences of value types t* and t*^3.
• There must be a sequence of value types t*^0, such that t*^2 = t*^0 t*.
• Then the combined instruction sequence is valid with type [t*^1] => [t*^0 t*^3].

Validates the given node, and if necessary: its children (recursively, using other ValidationVisitor instances).