| (* PH4.S1 — All 30 Instructions (Exact from XML) *) | |
| Inductive instruction : Type := | |
| | CONST | |
| | LOOKUP | |
| | BIND | |
| | PUSH | |
| | POP | |
| | CONS | |
| | CAR | |
| | CDR | |
| | SET_CAR | |
| | SET_CDR | |
| | MAKE_CLOSURE | |
| | CALL | |
| | TAIL_CALL | |
| | RETURN | |
| | JUMP | |
| | JUMP_IF_FALSE | |
| | PUSH_FRAME | |
| | POP_FRAME | |
| | CAPTURE_CONTINUATION | |
| | RESTORE_CONTINUATION | |
| | RAISE | |
| | INSTALL_HANDLER | |
| | REMOVE_HANDLER | |
| | REQUEST_EFFECT | |
| | HALT | |
| | PATCH_CODE | |
| | DEFINE_CODE | |
| | REPLACE_FUNCTION | |
| | REWRITE_DISPATCH | |
| | COMMIT_GENERATION | |
| | ROLLBACK_GENERATION. | |
| Definition instruction_count : nat := 30. | |