File size: 616 Bytes
119e586 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | (* 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.
|