WebSTG Docs

Evaluation rules

Shared rules

LET

let x=obj in e; s; H; enve; s; H[a]=obj; env[x↦a]where a=addr(obj) {\texttt{let}\ x = obj\ \IN\ e ;\ \Ss ;\ \SH;\ \SENV} \over {e;\ \Ss;\ \SH[a] = obj;\ \SENV[x \mapsto a] \quad \text{where } a = addr(obj)}

Allocate objects on the heap and bind their addresses to names in the local enviroment

LETREC

letrec x=obj in e; s; H; enve; s; H[a]=obj; env[x↦a]where a=addr(obj) {\texttt{letrec}\ x = obj\ \IN\ e ;\ \Ss ;\ \SH;\ \SENV} \over {e;\ \Ss;\ \SH[a] = obj;\ \SENV[x \mapsto a] \quad \text{where } a = addr(obj)}

Allocate objects on the heap and bind their addresses to names in the local enviroment

CASECON

case v of{…; C x1…xn -> e; …}; s; H[v]=CON(C a1…an); enve; s; H; env[x1↦a1…xn↦an] {\CASE\ v\ \OF \LBRACE\ldots ;\ C\, x_1 \ldots x_n\ \ARROW\ e;\ \ldots\RBRACE;\ \Ss;\ \SH[v] = \CON(C\ a_1\ldots a_n);\ \SENV} \over {e;\ \Ss;\ \SH;\ \SENV[x_1 \mapsto a_1 \ldots x_n \mapsto a_n]}

Match object to constructor alternative

CASEANY

case v of{…; x -> e}; s; H; enve; s; H; env[x↦v] {\CASE\ v\ \OF \LBRACE\ldots ;\ x\ \ARROW\ e\RBRACE;\ \Ss;\ \SH;\ \SENV} \over {e;\ \Ss;\ \SH;\ \SENV[x \mapsto v]}

Match object to default alternative

CASE

case e of{…}; s; H; enve; (case∙of{…},env):s; H; env {\CASE\ e\ \OF \LBRACE \ldots \RBRACE;\ \Ss;\ \SH;\ \SENV} \over {e;\ (\CASE \bullet \OF \LBRACE \ldots \RBRACE, \SENV):\Ss;\ \SH;\ \SENV}

Evaluate case scrutinee and push continuation onto stack

THUNK

x; s; H[x]=THUNK(e,env′); enve; Upd x ∙:s; H[x]=BLACKHOLE; env′ {x;\ \Ss;\ \SH[x] = \THUNK (e, \SENV');\ \SENV} \over {e;\ \texttt{Upd x}\ \bullet :\Ss;\ \SH[x] = \BLACKHOLE;\ \SENV'}

Enter a thunk and push an update frame onto the stack

INDIRECTION

x; s; H[x]=INDIRECTION y; envy; s; H; env {x;\ \Ss;\ \SH[x] = \INDIRECTION\ y;\ \SENV} \over {y;\ \Ss;\ \SH;\ \SENV}

Follow an indirection

RET

v; (case∙of{…},env′):s; H; envcase v of{…}; s; H; env′ {v;\ (\CASE \bullet \OF \{ \ldots \}, \SENV'):\Ss;\ \SH;\ \SENV} \over {\CASE\ v\ \OF \{ \ldots \};\ \Ss;\ \SH;\ \SENV'}

Pop case continuation off the stack

UPDATE

y; Upd x ∙:s; H; envy; s; H[x]=INDIRECTION y; env {y;\ \texttt{Upd x}\ \bullet :\Ss;\ \SH;\ \SENV} \over {y;\ \Ss;\ \SH[x] = \INDIRECTION\ y;\ \SENV}

Pop update frame and update thunk with an indirection

KNOWNCALL

fn a1…an; s; H[f]=FUN(x1…xn→e,envf); enve; s; H; envf[x1↦a1…xn↦an] {f^n\ a_1 \ldots a_n;\ \Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {e;\ \Ss;\ \SH;\ \SENV_f[x_1 \mapsto a_1 \ldots x_n \mapsto a_n]}

Call to a known function

PRIMOP

a1 op a2; s; H; envop in {+#,-#,*#,/#,%#,>=#,>#,==#,<#,<=#,!=#}a; s; H; envwhere a is the result of the primitive operation over a1 and a2 {\begin{array}{c} \scriptstyle a_1\ op\ a_2;\ \Ss;\ \SH;\ \SENV \\ \tiny op\ \IN\ \{ \ADD,\SUB,\MUL,\DIV,\MOD,\GEQ,\GTH,\EQU,\LTH,\LEQ,\NEQ \} \end{array}} \over {\begin{array}{c} \scriptstyle a;\ \Ss;\ \SH;\ \SENV \\ \text{\tiny where $a$ is the result of the primitive operation over $a_1$ and $a_2$}\end{array}}

Apply primitive operation to arguments

Push/Enter rules

PUSH

fk a1…am; s; H; envf; Arg a1:…:Arg am:s; H; env {f^k\ a_1 \ldots a_m;\ \Ss;\ \SH;\ \SENV} \over {f;\ \texttt{Arg}\ a_1: \ldots :\texttt{Arg}\ a_m:\Ss;\ \SH;\ \SENV}

Push function arguments onto the stack

FENTER

f; Arg a1:…:Arg an:s; H[f]=FUN(x1…xn→e,envf); enve; s; H; envf[x1↦a1…xn↦xn] {f;\ \texttt{Arg}\ a_1: \ldots :\texttt{Arg}\ a_n:\Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {e;\ \Ss;\ \SH;\ \SENV_f[x_1 \mapsto a_1 \ldots x_n \mapsto x_n]}

Collect function arguments off the stack and enter function body

PAP1

f; Arg a1:…:Arg am:s; H[f]=FUN(x1…xn→e,envf); envp; s; H[p]=PAP(f a1…am); env1≤m<n {f;\ \texttt{Arg}\ a_1: \ldots :\texttt{Arg}\ a_m:\Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {p;\ \Ss;\ \SH[p] = \PAP(f\ a_1 \ldots a_m);\ \SENV \quad \mathit{1 \le m < n}}

Construct partial application

PENTER

f; Arg an+1:s; H[f]=PAP(g a1…an); envg; Arg a1:…:Arg an:Arg an+1:s; H; env {f;\ \texttt{Arg}\ a_{n+1}:\Ss;\ \SH[f] = \mathtt{PAP}(g\ a_1 \ldots a_n);\ \SENV} \over {g;\ \texttt{Arg}\ a_1: \ldots :\texttt{Arg}\ a_n: \texttt{Arg}\ a_{n+1}:\Ss;\ \SH;\ \SENV}

Enter partial application and push combined arguments onto the stack

Eval/Apply rules

EXACT

f∙ a1…an; s; H[f]=FUN(x1…xn→e,envf); enve; s; H; envf[x1↦a1…xn↦an] {f^\bullet\ a_1 \ldots a_n;\ \Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {e;\ \Ss;\ \SH;\ \SENV_f[x_1 \mapsto a_1 \ldots x_n \mapsto a_n]}

Call of an unknown function with a matching number of arguments

CALLK

fk a1…am; s; H[f]=FUN(x1…xn→e,envf); enve; (∙ an+1…am):s; H; envf[x1↦a1…xn↦an]m>n {f^k\ a_1 \ldots a_m;\ \Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {e;\ (\bullet\ a_{n+1} \ldots a_m):\Ss;\ \SH;\ \SENV_f[x_1 \mapsto a_1 \ldots x_n \mapsto a_n] \quad m > n}

Function call with too many arguments, the excess of which is pushed onto the stack

PAP2

fk a1…am; s; H[f]=FUN(x1…xn→e,envf); envp; s; H[p]=PAP(f a1…am); envm<n {f^k\ a_1 \ldots a_m;\ \Ss;\ \SH[f] = \FUN(x_1 \ldots x_n \rightarrow e, \SENV_f);\ \SENV} \over {p;\ \Ss;\ \SH[p] = \PAP(f\ a_1 \ldots a_m);\ \SENV \quad m < n}

Function call with too few arguments, a partial application is constructed

TCALL

f∙ a1…am; s; H[f]=THUNK(e,env′); envf; (∙ a1…am):s; H; env {f^\bullet\ a_1 \ldots a_m;\ \Ss;\ \SH[f] = \THUNK(e, \SENV');\ \SENV} \over {f;\ (\bullet\ a_1 \ldots a_m):\Ss;\ \SH;\ \SENV}

Calling a thunk (it may return a PAP or FUN, so the arguments must be pushed onto the stack)

PCALL

fk an+1…am; s; H[f]=PAP(g a1…an); envg∙ a1…an an+1…am; s; H; env {f^k\ a_{n+1} \ldots a_m;\ \Ss;\ \SH[f] = \PAP(g\ a_1 \ldots a_n);\ \SENV} \over {g^\bullet\ a_1 \ldots a_n\ a_{n+1} \ldots a_m;\ \Ss;\ \SH;\ \SENV}

Providing additional arguments to a partial application

RETFUN

f; (∙ a1…an):s; H[f]∈{FUN,PAP}; envf∙ a1…an; s; H; env {f;\ (\bullet\ a_1 \ldots a_n):\Ss;\ \SH[f] \in \{\FUN, \PAP\};\ \SENV} \over {f^\bullet\ a_1 \ldots a_n;\ \Ss;\ \SH;\ \SENV}

Construct a function call with returned function (or partial application) and arguments from stack