¶S₀ bytecode
Each S₀ instruction will be encoded into a 1-byte opcode. Some opcodes will have a variable amount of data following the opcode, as described below.
There will be four working stacks, so the top two bits of each opcode identify which stack the instruction operates on (the “target stack”).
Instructions needed:
¶Stack values
¶nil
Opcode: tt000000 Semantics: ⟦nilₜ⟧ ξₜ ≜ ξₜ⋅[]
The nil instruction pushes an empty stack value onto the target stack.
¶unpack
Opcode: tt000001 Semantics: ⟦unpackₜ⟧ ξₜ⋅[ξ] ≜ ξₜ⋅ξ
The unpack instruction pops a stack value from the target stack, and pushes the contents of the stack value onto the target stack.
¶pack
Opcode: tt000010 Semantics: ⟦packₜ⟧ ξₜ⋅v ≜ ξₜ⋅[v]
The pack instruction pops a value (“element”) from the target stack, and pushes a new stack value containing “element” onto the target stack.
¶cat
Opcode: tt000011 Semantics: ⟦catₜ⟧ ξₜ⋅[ξ₁]⋅[ξ₀] ≜ ξₜ⋅[ξ₁⋅ξ₀]
The cat instruction pops two stack values from the target stack, and pushes a new stack value containing the concatenation of their contents onto the target stack.
¶Stack manipulation
¶swap
Opcode: tt0001tt Semantics: ⟦swapₜ⟧ ξₜ⋅v₁⋅v₀ ≜ ξₜ⋅v₀⋅v₁
The swap instruction pops two values from the target stack, and pushes them back onto the target stack in reverse order.
¶to
Opcode: tt0001ss Semantics: ⟦ₛtoₜ⟧ ξₛ⋅v ξₜ ≜ ξₛ ξₜ⋅v
The to instruction pops a value from the source stack, and pushes it onto the target stack.
¶Tags and locks
¶newtag
Opcode: tt001000 Semantics: ⟦newtagₜ⟧ ξₜ ≜ ξₜ⋅α
The newtag instruction pushes a new tag onto the target stack.
¶droptag
Opcode: tt001001 Semantics: ⟦droptagₜ⟧ ξₜ⋅α ≜ ξₜ
The droptag instruction pops a tag from the target stack.
¶lock
Opcode: tt001010 Semantics: ⟦lockₜ⟧ ξₜ⋅α⋅v ≜ ξₜ⋅α⋅⦇v/α⦈
The lock instruction pops a value and a tag from the target stack, locks the value using the tag, and pushes the locked value and tag onto the target stack.
¶unlock
Opcode: tt001011 Semantics: ⟦unlockₜ⟧ ξₜ⋅α⋅⦇v/α⦈ ≜ ξₜ⋅α⋅v
The unlock instruction pops a locked value and a matching tag from the target stack, unlocks the value, and pushes the unlocked value and tag onto the target stack.
¶Quotations
¶apply
Opcode: tt11nnnn ⟨branch⟩ (1)
tt111111 nnnnnnnn ⟨branch⟩ (2)
Semantics: ⟦applyₜ⟧ ξₜ⋅{branch} ≜ ⟦branch⟧ ξ₊
The apply instruction pops a quotation from the target stack, and invokes the quotation's named branch.
Opcode variant (1) is used for a branch name with 15 or fewer bytes.
Opcode variant (2) is used for a branch name with 15 or more bytes.
¶quotation
Opcode: tt01iiii ⟨instructions⟩ (1)
tt011111 iiiiiiii iiiiiiii ⟨instructions⟩ (2)
tt10bbbb (branches*) (3)
tt100000 bbbbbbbb (branches*) (4)
Semantics: hard to describe in math at the moment
The quotation instruction (which includes the definition of a quotation) pops a value from the target stack, and pushes the quotation closed over that value onto the target stack.
Opcode variant (1) is used for a “branchless” quotation with fewer than 15 instructions.
Opcode variant (2) is used for a “branchless” quotation with 15 or more instructions.
Opcode variant (3) is used for a quotation with 1 to 15 branches, at least one of which has a name.
Opcode variant (4) is used for all other quotations.
¶upquote
Opcode: tt0011dd (1)
tt001111 dddddddd (2)
Semantics: hard to describe in math at the moment
The upquote instruction finds the d-th closest syntactically enclosing quotation, pops a value from the target stack, and pushes the quotation closed over that value onto the target stack.
Opcode variant (1) is used for a depth of less than 3.
Opcode variant (2) is used for all other depths.
¶The full table
Just for target stack 0:
00 nil₀ 01 unpack₀ 02 pack₀ 03 cat₀ 04 swap₀ 05 ₁to₀ 06 ₂to₀ 07 ₃to₀ 08 newtag₀ 09 droptag₀ 0a lock₀ 0b unlock₀ 0c upquote₀ 0 0d upquote₀ 1 0e upquote₀ 2 0f upquote₀ ≥3 10 quotation₀, branchless, 0 instructions 11 quotation₀, branchless, 1 instructions 12 quotation₀, branchless, 2 instructions 13 quotation₀, branchless, 3 instructions 14 quotation₀, branchless, 4 instructions 15 quotation₀, branchless, 5 instructions 16 quotation₀, branchless, 6 instructions 17 quotation₀, branchless, 7 instructions 18 quotation₀, branchless, 8 instructions 19 quotation₀, branchless, 9 instructions 1a quotation₀, branchless, 10 instructions 1b quotation₀, branchless, 11 instructions 1c quotation₀, branchless, 12 instructions 1d quotation₀, branchless, 13 instructions 1e quotation₀, branchless, 14 instructions 1f quotation₀, branchless, ≥15 instructions 20 quotation₀, ≥16 branches 21 quotation₀, 1 branch 22 quotation₀, 2 branches 23 quotation₀, 3 branches 24 quotation₀, 4 branches 25 quotation₀, 5 branches 26 quotation₀, 6 branches 27 quotation₀, 7 branches 28 quotation₀, 8 branches 29 quotation₀, 9 branches 2a quotation₀, 10 branches 2b quotation₀, 11 branches 2c quotation₀, 12 branches 2d quotation₀, 13 branches 2e quotation₀, 14 branches 2f quotation₀, 15 branches 30 apply, nameless branch 31 apply, 1-byte branch 32 apply, 2-byte branch 33 apply, 3-byte branch 34 apply, 4-byte branch 35 apply, 5-byte branch 36 apply, 6-byte branch 37 apply, 7-byte branch 38 apply, 8-byte branch 39 apply, 9-byte branch 3a apply, 10-byte branch 3b apply, 11-byte branch 3c apply, 12-byte branch 3d apply, 13-byte branch 3e apply, 14-byte branch 3f apply, ≥15-byte branch