2.4. Evaluation¶

This chapter specifies the operational semantics of abstract instructions within an abstract stack machine, to indirectly give semantics of a Kink program. Abstract instructions are transformed from a Kink program through desugaring and translation steps.

abstract stack machine¶: An abstract machine which evaluates abstract instructions.
abstract instruction¶: An instruction which is evaluated by abstract stack machine.

Multiple abstract stack machines can exist in a single runtime, and they can evaluate abstract instructions in parallel. They share the same set of vals, and other resources within the runtime.

The abstract stack machine and abstract instructions are defined just to show how Kink programs should behave. Thus, an implementation of runtime need not implement the abstract stack machine literally, however, the observable behavior must obey the definition.

2.4.1. Conventions¶

2.4.1.1. Abstract instruction¶

An abstract instruction is parenthesized like the following:

(varref "op_store")

Here, varref is the opcode of the instruction, and "op_store" is the operand of the instruction.

Every instruction has a location as an implicit operand.

2.4.1.2. Data types¶

The following data types are used as operands of abstract instructions:

val : a Kink val.
str : an immutable, finite length sequence of unicode codepoints, which can be represented by a str val.
num : a combination of (Mantissa, Scale), which can be represented by a num val.
location : a combination of (Program_name, Program_text, Pos), which can be represented by a location val.
a sequence of instructions.

2.4.1.3. Sequence of instructions¶

A sequence of instructions is represented by just placing instructions in order like the following:

(emptyvec) (binding) (load "X") (add)

A sequence of no instruction is represented as follows:

∅

2.4.1.4. Stack¶

An abstract stack machine operates on its stack.

A stack consists of a sequence of instructions, and the sequence of instructions is updated every time a reduction rule is applied.

A stack is represented like the following:

^ (str "Foo") (dup) (remove) $

Here, ^ is the mark of the beginning of the stack, and $ is the mark of the end of the stack.

2.4.1.5. Reduction rules¶

A reduction rule is written like the following:

(val V) (dup) → (val V) (val V)

It means that if there is a sub-sequence of instructions (val V) (dup) in the stack, the reduction rule is applied, and the sub-sequence is updated to (val V) (val V). Note that V is a metavariable, and it represents a Kink val.

Additional conditions of a reduction rule can be given using comment lines which start with #.

If there are multiple reduction rules which can be applied for a stack, the leftmost rule is applied.

2.4.1.6. Metavariable¶

In this chapter, metavariables of the following formats are used to represent an abstract instruction, a sequence of abstruct instructions, and other data.

_snake_case_with_underscore_as_prefix_and_suffix_: A sequence of instructions.
Capitalized_snake_case: An abstract instructions, a val, a str, a num, or a location.

2.4.2. Initial state¶

Evaluation of an abstract stack machine starts invoking a fun with no args. When evaluation is started with a fun val Fun, the initial state of the stack is:

^ (val Fun) (nada) (emptyvec) (call "..root..") $

2.4.3. Terminal state¶

When the stack is in the following states, no more reduction rule can be applied. These states are terminal states.

^ (val V) $

This terminal state means that the abstract stack machine terminates returining a val.

^ (uncaught Exc) $

This terminal state means the abstract stack machine terminates with an uncaught exception.

2.4.4. Abstract instructions¶

2.4.4.1. val instruction¶

val instruction places an arbitrary type of val on the stack.

syntax

(val V)

There is no reduction rule for val instruction.

A single val instruction can be a terminal state of the abstract stack machine.

2.4.4.2. uncaught instruction¶

uncaught instruction means an exception which is not caught within the abstract stack machine.

syntax

(uncaught Exc)

Exc is an exception val.

reduction rule

(uncaught Exc) Any → (uncaught Exc)

Any is any instruction

This rule means that the uncaught exception is propagated until the terminal state.

2.4.4.3. num instruction¶

num instruction produces a num val.

syntax

(num Num)

Num parameter is a num.

reduction rule

(num Num)

→ (val Num_val)
# where `Num_val` is a num val converted from `Num`.

2.4.4.4. str instruction¶

str instruction produces a str val.

syntax

(str Str)

Str parameter is a str.

reduction rule

(str Str)

→ (val Str_val)
# where `Str_val` is a str val converted from `Str`

2.4.4.5. nada instruction¶

nada instruction produces nada val.

syntax

(nada)

reduction rule

(nada)

→ (val Nada_val)
# where `Nada_val` is `nada` val

2.4.4.6. fun instruction¶

fun instruction produces a function val.

syntax

(fun _insns_)

_insns_ is a sequence of instructions.

reduction rule

(val Enclosing_binding) (fun _insns_)
# where
# • `Enclosing_binding` is a binding val.

→ (val Fun)
# where
# • `Fun` is a fun val with instructions copied from `_insns_`,
#   replacing every occurrence of (enclosingbinding) by (val Enclosing_binding).

function¶: A value which holds an immutable sequence of abstract instructions. Function can be abbreviated to fun. The companion module of functions is kink/FUN.

2.4.4.7. emptyvec instruction¶

emptyvec instruction produces a newly created vec val with no element.

syntax

(emptyvec)

reduction rule

(emptyvec)

→ (val Empty_vec)
# where `Empty_vec` is a newly created vec val with no element

2.4.4.8. add instruction¶

add instruction produces a newly created vec val adding an element to the back of an existing vec.

syntax

(add)

reduction rule

(val Vec) (val Elem) (add)
# where `Vec` is a vec val

→ (val New_vec)
# where `New_vec` is a newly created vec val containing the elements of `Vec`
# at the front, and `Elem` at the back.

2.4.4.9. concat instruction¶

concat instruction sets up doconcat instruction.

syntax

(concat)

reduction rules

(concat)

→ (doconcat) (trace "" Location)
# where
# • `Location` is the location of the implicit location of the `concat` instruction.

concat and doconcat are separated, so that the trace of the location of spreading can be added to the stack overflow exception.

2.4.4.10. doconcat instruction¶

doconcat instruction produces a newly created vec val concatenating two vec vals.

syntax

(doconcat)

reduction rules

(val X) (val Y) (doconcat)
# where
# • `X` is a vec val
# • `Y` is a vec val

→ (val New_vec)
# where `New_vec` is a newly created vec val
# concatenating `X` at the front, and `Y` at the back.

(val X) (val Non_vec) (doconcat)
# where
# • `X` is a vec val
# • `Non_vec` is not a vec val

→ (str Message) (traces) (exception) (raise)
# where
# • `Message` is an error message.

2.4.4.11. dup instruction¶

dup instruction duplicates the preceding val on the stack.

syntax

(dup)

reduction rule

(val V) (dup) → (val V) (val V)

2.4.4.12. flip instruction¶

flip instruction swaps the preceding two vals on the stack.

syntax

(flip)

reduction rule

(val A) (val B) (flip) → (val B) (val A)

2.4.4.13. remove instruction¶

remove instruction removes the preceding val from the stack.

syntax

(remove)

reduction rule

(val V) (remove) → ∅

2.4.4.14. varref instruction¶

varref instruction produces a varref val.

syntax

(varref Symbol)

Symbol is a str.

reduction rule

(val Owner) (varref Symbol)

→ (val Varref)
# where `Varref` is a varref val whose owner is `Owner`, and whose symbol is `Symbol`.

2.4.4.15. load instruction¶

load instruction does variable load operation for a variable.

syntax

(load Symbol)

Symbol is a a str.

reduction rules

(val Owner) (load Symbol)
# where the content of variable (`Owner`, `Symbol`) is not empty

→ (val Content)
# where `Content` is the content of the variable (`Owner`, `Symbol`)

(val Owner) (load Symbol)
# where the content of variable (`Owner`, `Symbol`) is empty

→ (str Message) (traces) (exception) (raise) (trace "" Location)
# where
# • `Message` is an error message.
# • `Location` is the implicit location of the `load` instruction.

2.4.4.16. checkfun instruction¶

checkfun instruction ensures that the preceding val is a fun val.

syntax

(checkfun)

reduction rules

(val Fun) (checkfun)
# where
# • `Not_fun` is a fun val.

→ ∅

(val Not_fun) (checkfun)
# where
# • `Not_fun` is not a fun val.

→ (str Message) (traces) (exception) (raise) (trace "" Location)
# where
# • `Message` is an error message.
# • `Location` is the implicit location of the `checkfun` instruction.

2.4.4.17. call instruction¶

call instruction sets up invocation of a fun.

syntax

(call Symbol)

Symbol is a str.

reduction rules

(val Fun) (val Recv) (val Args) (call Symbol) (tail)
# where
# • `Fun` is a fun val.
# • `Args` is a vec val.

→ (val Fun) (val Recv) (val Args) (tailcall) (tailtrace Symbol Location)
# where
# • `Location` is the implicit location of the `call` instruction.

(val Fun) (val Recv) (val Args) (call Symbol) Non_tail
# where
# • `Non_tail` is an instruction which is not `tail`

→ (val Fun) (val Recv) (val Args) (docall) (trace Symbol Location) Non_tail
# where
# • `Location` is the implicit location of the `call` instruction.

2.4.4.18. tailcall instruction¶

tailcall instruction sets up tail traces and invocation of a fun.

syntax

(tailcall)

reduction rule

(tailcall) _tail_traces_
# where
# • `_tail_traces_` is a sequence of 0 or more `tailtrace` instructions.

→ (docall) _snipped_tail_traces_
# where
# • `_snipped_tail_traces_` is a sequence of `tailtrace` instructions,
#   snipped from `_tail_traces_` following the the rule below.

tail trace snipping rule

The specification requires that successive tail calls do not cause stack overflow. Such requirement is called tail call elimination. To guarantee it, the sequence of tailtrace instructions is snipped as follows:

Each tailtrace instruction can be remvoed.
Each tailtrace instruction can be converted to (tailtrace "" (program name="", program text="", pos index in the program text=0))
The length of the sequence must be kept less than or equal to the constant maximum number which the runtime defines.

tail call¶: The function call done by tailcall instruction.
tail call elimination¶: The requirement that successive tail calls do not cause stack overflow.

2.4.4.19. docall instruction¶

docall instruction invokes a fun.

syntax

(docall)

reduction rule

(val Fun) (val Recv) (val Args) (docall)
# where
# • `Fun` is a fun val.
# • `Args` is a vec val.

→ (val Recv) (val Args_copy) _fun_insns_ (tail)
# where
# • `_fun_insns_` is the insns within `Fun`.
# • `Args_copy` is a newly created vec val copying the elements of `Args`.

2.4.4.20. traces instruction¶

traces instruction makes a vec of trace vals from trace and tailtrace instructions on the stack.

syntax

(traces)

reduction rules

(traces) _insns_ $
# where `_insns_` is a sequence of instructions.

→ (val Traces) _insns_ $
# where
# • `Traces` is a newly created vec val of trace vals,
#   converted from `trace`, `tailtrace`, and `delimit` instructions in `_insns_` as follows,
#   reverting the order.
#   • From a `trace` instruction, a non-tail trace val is produced.
#   • From a `tailtrace` instruction, a tail trace val is produced.
#   • From a `delimit` instruction, a non-tail trace val is produced with symbol="..kont tag..",
#     and location=("", "", 0).

2.4.4.21. exception instruction¶

exception instruction produces an exception value.

exception¶: A value which consists of a message string, a vec of traces, and optionally the next exception in the chain. The companion module of exceptions is kink/EXCEPTION.

syntax

(exception)

reduction rule

(val Message) (val Traces) (exception)
# where
# • `Message` is a str val
# • `Traces` is a vec of trace vals

→ (val Exc)
# where `Exc` is an exception val made from `Message` and `Traces`

2.4.4.22. raise instruction¶

raise instruction raises an exception.

syntax

(raise)

reduction rules

(val Exc) (raise) _no_jump_tag_ (val Escape_tag) (delimit)
# where
# • `Escape_tag` is the escape tag (see kink/KONT_TAG.escape_tag).
# • `_no_jump_tag_` is a sequence of instructions
#   which does not contain (delimit) directly preceded by (val Escape_tag).

→ (val Fun) (val Escape_tag) (delimit)
# where `Fun` is a fun val like {(:cont_raised :cont_jump) cont_raised(Exc) }

(val Exc) (raise) _no_jump_tag_ $
# where
# • `_no_jump_tag_` is a sequence of instructions
#   which does not contain (delimit) directly preceded by (val Escape_tag).

→ (uncaught Exc) _no_jump_tag_ $

2.4.4.23. binding instruction¶

binding instruction is the place-holder of the current binding.

syntax

(binding)

2.4.4.24. enclosingbinding instruction¶

enclosingbinding instruction is the place-holder of the enclosing binding.

syntax

(enclosingbinding)

2.4.4.25. clonebinding instruction¶

clonebinding instruction makes a new binding from the enclosing binding.

syntax

(clonebinding)

reduction rule

(val Enclosing_binding) (clonebinding)
# where
# • `Enclosing_binding` is a binding val.

→ (val Binding)
# where
# • `Binding` is a newly created binding val,
#   copying all the vars of `Enclosing_binding`.

2.4.4.26. setbinding instruction¶

setbinding instruction sets the current binding.

syntax

(setbinding)

reduction rule

(val Binding) (setbinding) _until_tail_ (tail)
# where
# • `Binding` is a binding val.
# • `_until_tail_` is a sequence of instructions
#   which does not contain `tail` instruction.

→ _converted_until_tail_ (tail)
# where
# • `_converted_until_tail_` is a sequence of instructions
#   copied from `_converted_until_tail_`,
#   replacing every occurrence of (binding) by (val Binding).

2.4.4.27. storerecvargs instruction¶

storerecvargs instruction sets _Recv and _Args vars of the current binding.

syntax

(storerecvargs)

reduction rule

(val Recv) (val Args) (val Binding) (storerecvargs)
# where
# • `Args` is a vec val.
# • `Binding` is a binding val.

→ ∅

When this reduction rule is applied, Recv is assigined to _Recv variable of Binding, and Args is assigined to _Args variable of Binding.

2.4.4.28. tail instruction¶

tail instruction is the marker of tail context.

syntax

(tail)

reduction rule

(tail) → ∅

This rule means that tail instruction acts as NOP.

2.4.4.29. hostcall instruction¶

hostcall instruction invokes a host procedure.

host procedure¶: Information to specify a procedure within the host system, such as a function address, closure, object reference. A host procedure should take a single value as the argument, and return a single value as the result.

syntax

(hostcall Host_proc)

Host_proc is a host procedure.

reduction rule

(val Arg) (call Host_proc)

→ (val Result)
# where
# • `Result` is the result of `Host_proc` with the argument `Arg`.

2.4.4.30. canshift instruction¶

canshift instruction tests whether the current continuation is delimited by a continuation tag.

syntax

(canshift)

reduction rules

(val Kont_tag) (canshift) _insns_ (val Kont_tag) (delimit)
# where
# • `Kont_tag` is a continuation tag.
→ (val True) _insns_ (val Kont_tag) (delimit)
# where
# • `True` is true val.

(val Kont_tag) (canshift) _no_delimit_ $
# where
# • `Kont_tag` is a continuation tag.
# • `_no_delimit_` is a sequence of instructions
#   which does not contain (delimit) directly preceded by (val Kont_tag).
→ (val False) _no_delimit_ $
# where
# • `False` is false val.

2.4.4.31. kont instruction¶

kont instruction extracts a delimited continuation function from the stack.

delimited continuation¶: A function created by kont instruction. Delimited continuation can be abbreviated to kont. See kink/KONT_TAG for creation and usage in the real world.

syntax

(kont)

reduction rule

(val Kont_tag) (kont) (val Kont_tag) (abort) _no_delimit_ (val Kont_tag) (delimit)
# where
# • `Kont_tag` is a continuation tag.
# • `_no_delimit_` is a sequence of instructions which does not contain (delimit)
#   directly preceded by (val Kont_tag).

→ (val Kont_fun) (val Kont_tag) (abort) _no_delimit_ (val Kont_tag) (delimit)
# where
# • `Kont_fun` is a delimited continuation created as follows:

making of a delimited continuation

In the previous reduction rule, Kont_fun is a function which takes a single argument. When the function is called, at the tail of the invocation, the following sequence of instructions is evaluated:

{push the argument of Kont_fun}
_no_delimit_
(val Kont_tag)
(delimit)

2.4.4.32. abort instruction¶

abort instruction moves to the corresponding delimit.

syntax

(abort)

reduction rule

(val Abort_fun) (val Kont_fun) (val Kont_tag) (abort) _no_delimit_ (val Kont_tag) (delimit)
# where
# • `Abort_fun` is a fun val.
# • `Kont_fun` is a fun val.
# • `Kont_tag` is a continuation tag.
# • `_no_delimit_` is a  sequence of instructions which does not contain (delimit)
#   directly preceded by (val Kont_tag).

→ (val Abort_fun) (nada) (emptyvec) (val Kont_fun) (add) (call "call") (val Kont_tag) (delimit)

2.4.4.33. delimit instruction¶

delimit instruction is a marker of a continuation tag in the stack.

continuation tag¶: A value used to mark the delimiter of a delimited continuation. The companion module of continuation tags is kink/KONT_TAG.

syntax

(delimit)

reduction rule

(val X) (val Kont_tag) (delimit) → (val X)

2.4.4.34. trace instruction¶

trace instruction places a non-tail trace.

syntax

(trace Symbol Location)

Symbol is a str. Location is a tuple of (program name, program text, pos index in the program text).

reduction rule

(trace Symbol Location) → ∅

This rule means that trace instruction acts as NOP.

2.4.4.35. tailtrace instruction¶

tailtrace instruction places a tail trace.

syntax

(tailtrace Symbol Location)

Symbol is a str. Location is a tuple of (program name, program text, pos index in the program text).

reduction rule

(tailtrace Symbol Location) → ∅

This rule means that tailtrace instruction acts as NOP.

2.4.5. Resource error¶

The following reduction rule can be applied anytime, when any type of resource error happens, for example, when the length of the sequence of instructions of the stack becomes too long (stack overflow).

reduction rule

^

→ ^ (str Message) (traces) (exception) (raise)
# where
# • `Message` is an error message.