Evaluation
Let the definition of a function Fname be of the form
Fname Palt
Then evaluating a function call <Fname Ge> amounts to
evaluating the source Ge : Palt. If the result obtained is a ground
expression Ge' or an error $error(Ge'), it is taken to be
the result of evaluating the call. Otherwise, if the result is a failure
$fail(k), the following actions depend on the function
Fname having been declared either failing or unfailing. If the function
is a failing one, the result returned is $fail(0), otherwise, if the
function is an unfailing one, the result returned is $error(Fname "Unexpected
fail").
{},0,St |- Ge : Palt => Ge',St'
-------------------------------
St |- <Fname Ge> => Ge',St'
{},0,St |- Ge : Palt => $fail(k),St'
------------------------------------
St |- <Fname Ge> => $fail(0),St'
where the function Fname is a failing one,
i.e. it has been declared as
$func? Fname Farg = Fres;.
{},0,St |- Ge : Palt => $fail(k),St'
-------------------------------------------------------
St |- <Fname Ge> => $error(Fname "Unexpected fail"),St'
where the function Fname is an unfailing one,
i.e. it has been declared as
$func Fname Farg = Fres;.
{},0,St |- Ge : Palt => $error(Ge'),St'
---------------------------------------
St |- <Fname Ge> => $error(Ge'),St'
The above inference rules assume the function Fname to have the
definition Fname Palt.