Function Definitions

A function's definition binds the function's name to the function's body, thereby describing the way in which the function is to be evaluated.

Syntax

FunctionDefinition =
     FunctionName FunctionBody ";".
FunctionBody =
     PatternAlternative | Sentence.

A function definition of the form Fname Snt; is equivalent to the definition Fname \{ Snt; }; .

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.