\section{Functions}

\subsection{Functions in Expressions}

At the syntax level function calls are introduced with the following construct: 

\[
\begin{array}{rcl}
  \mathscr E & += & \mathscr X \mathscr E^*
\end{array}
\]

In the concrete syntax function call looks conventional:

\begin{lstlisting}
     $f$ ($e_1, e_2, \dots, e_k$)
\end{lstlisting}

where $f$~--- a function name, $e_i$~--- its actual parameters.

Surpisingly, such a mild extension results in a complete redefinition of the semantics. Indeed, as function body can perform
arbitrary actions on state, input and output streams, expressions with function calls can now have side effects. In order to express these
side effects we need to redefine the semantics completely, this time using big-step operational style.

We extend the configuration, used in the semantic description for statements, with a fourth component~--- an optional integer value:

\[
\mathscr C = \Sigma \times \mathbb Z^* \times \mathbb Z^* \times \mathbb Z^?
\]

This component will correspond to an optional return value for function/procedure calls (either integer value $n$ or ``$\hbox{---}$'', nothing).

The rules inself are summarized in the Fig.~\ref{bs_expr}. Note the use of double environment for evaluating the body of function in the rule
\rulename{Call}; note also, that now semantics of expressions and statements are mutually recursive.

\setarrow{\xRightarrow}
\setsubarrow{_{\mathscr E}}

\begin{figure}
  \[\withenv{\Phi}{\trans{\inbr{\sigma, i, o, \hbox{---}}}{n}{\inbr{\sigma, i, o, n}}} \ruleno{Const} \]
  \[\withenv{\Phi}{\trans{\inbr{\sigma, i, o, \hbox{---}}}{x}{\inbr{\sigma, i, o, \sigma\;x}}} \ruleno{Var} \]
  \[\trule{\withenv{\Phi}{\trans{c}{A}{c^\prime=\inbr{\_,\, \_,\, \_,\, a}}},\;
           \withenv{\Phi}{\trans{c^\prime}{B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, b}}}
          }
          {\withenv{\Phi}{\trans{c}{A\otimes B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, a\oplus b}}}}
          \ruleno{Binop}
  \]
  \[\trule{\begin{array}{c}
             \withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}},\\
             \Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}},\\
             {\setsubarrow{}
             \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, n}}}}
           \end{array}
          }
          {\withenv{\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, n}}}}
          \ruleno{Call}
  \]
\caption{Big-step Operational Semantics for Expressions}
\label{bs_expr}
\end{figure}

\subsection{Return Statement}

In order to make it possible to return values from procedures we add a return statement to the language of statements:

\[
\mathscr S += \llang{return $\;\mathscr E^?$}
\]

And, again, this small addition leads to redefinition of the semantics in \emph{continuation-passing style} (CPS).

First, we define the following meta-operator ``$\diamond$'' on statements:

\[
\begin{array}{rcl}
  s \diamond \llang{skip} & = & s\\
  s_1 \diamond s_2 & = & \llang{$s_1$; $\;s_2$}
\end{array}
\]

\setsubarrow{}

Then, we add another environment component, $K$, in the description of semantic relation ``$\withenv{...}{\trans{...}{...}{...}}$''. Informally
speaking, now

\[
\withenv{K,\,\Phi}{\trans{c}{s}{c^\prime}}
\]

is read ``the execution of $s$, immediately followed by $K$, in the configuration $c$ results in the configuration $c^\prime$''. Statement $K$ is called \emph{continuation}.
The rules themselves are shown on Fig.~\ref{bs_cps}. Note, the rule for the call statement is exactly the same, as for the call expression.

\begin{figure}
  \[\withenv{\llang{skip},\,\Phi}{\trans{c}{\llang{skip}}{c}}\ruleno{SkipSkip}\]
  \[\trule{\withenv{\llang{skip},\,\Phi}{\trans{c}{K}{c^\prime}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{skip}}{c^\prime}}}
    \ruleno{Skip}
  \]
  \[\trule{{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
           \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma[x\gets n],\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}
          }
          {\withenv{K,\,\Phi}{\trans{c}{\llang{$x\,$:=$\,e$}}{c^\prime}}}
    \ruleno{Assign}
  \]
  \[\trule{{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
           \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o@[n],\,\hbox{---}}}{K}{c^\prime}}
          }
          {\withenv{K,\,\Phi}{\trans{c}{\llang{write ($e$)}}{c^\prime}}}
    \ruleno{Write}
  \]
  \[\trule{
           \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma[x\gets z],\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}
          }
          {\withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,z:i,\,o,\,\hbox{---}}}{\llang{read ($x$)}}{c^\prime}}}
    \ruleno{Read}
  \]

  \[\trule{\withenv{s_2\diamond K,\,\Phi}{\trans{c}{\llang{$s_1$}}{c^\prime}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{$s_1$; $\;s_2$}}{c^\prime}}}
    \ruleno{Seq}
  \]

  \[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
           \withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_1$}}{c^\prime}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{if $\;e\;$ then $\;s_1\;$ else $\;s_2$}}{c^\prime}}}
          {n\ne 0}
    \ruleno{IfTrue}
  \]

  \[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
           \withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_2$}}{c^\prime}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{if $\;e\;$ then $\;s_1\;$ else $\;s_2$}}{c^\prime}}}
          {n= 0}
    \ruleno{IfFalse}
  \]

  \[\crule{\begin{array}{c}
             {\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}}\\
             \withenv{\llang{while $\;e\;$ do $\;s$}\diamond K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s$}}{c^\prime}}
           \end{array}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{while $\;e\;$ do $\;s$}}{c^\prime}}}
          {n\ne 0}
    \ruleno{WhileTrue}
  \]

    \[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
           \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{while $\;e\;$ do $\;s$}}{c^\prime}}}
          {n = 0}
    \ruleno{WhileFalse}
  \]

  \[\trule{\begin{array}{c}
           {\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}}}\\
            \Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}} \\
            \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, \hbox{---}}}}\\
            \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, \hbox{---}}}{K}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}
           \end{array}}
          {\withenv{K,\,\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}}
          \ruleno{Call}
  \]
  
  \[
    \withenv{K,\,\Phi}{\trans{c}{\llang{return}}{c}}
    \ruleno{ReturnEmpty}
  \]

  \[
    \trule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{c^\prime}}}}
          {\withenv{K,\,\Phi}{\trans{c}{\llang{return $\;e\;$}}{c^\prime}}}
    \ruleno{Return}
  \]  
  
  \caption{Continuation-passing Style Semantics for Statements}
  \label{bs_cps}
\end{figure}
