File size: 986 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 | (* PH1.S3 — Instruction Set
From SKC-LISP-WORLD-COQ-001 <instruction-set> *)
Inductive instruction : Type :=
| CONST (* Load constant *)
| LOOKUP (* Resolve binding *)
| BIND (* Create/replace binding *)
| PUSH (* Push value stack *)
| POP (* Pop value stack *)
| CONS (* Allocate cons *)
| CAR | CDR (* Access cons *)
| SET_CAR | SET_CDR (* Mutate cons *)
| 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
| PATCH_CODE (* Validated code patch *)
| DEFINE_CODE
| REPLACE_FUNCTION
| REWRITE_DISPATCH
| COMMIT_GENERATION (* New world generation *)
| ROLLBACK_GENERATION
| HALT.
Definition instruction_count : nat := 30.
|