SIGNATURE

Major Section:  MISCELLANEOUS

Examples:
((hd *) => *)
((printer * state) => (mv * * state))
((mach * mach-state * state) => (mv * mach-state)


General Form:
((fn ...) => *)
((fn ...) => stobj)
or
((fn ...) => (mv ...))

where fn is the constrained function symbol, ... is a list of asterisks and/or the names of single-threaded objects and stobj is a single-threaded object name. ACL2 also supports an older style of signature described below after we describe the preferred style.

Signatures specify three syntactic aspects of a function symbol: (1) the ``arity'' or how many arguments the function takes, (2) the ``multiplicity'' or how many results it returns via MV, and (3) which of those arguments and results are single-threaded objects and which objects they are.

For a discussion of single-threaded objects, see stobj. For the current purposes it is sufficient to know that every single- threaded object has a unique symbolic name and that state is the name of the only built-in single-threaded object. All other stobjs are introduced by the user via defstobj. An object that is not a single-threaded object is said to be ``ordinary.''

The general form of a signature is ((fn x1 ... xn) => val). So a signature has two parts, separated by the symbol ``=>''. The first part, (fn x1 ... xn), is suggestive of a call of the constrained function. The number of ``arguments,'' n, indicates the arity of fn. Each xi must be a symbol. If a given xi is the symbol ``*'' then the corresponding argument must be ordinary. If a given xi is any other symbol, that symbol must be the name of a single-threaded object and the corresponding argument must be that object. No stobj name may occur twice among the xi.

The second part, val, of a signature is suggestive of a term and indicates the ``shape'' of the output of fn. If val is a symbol then it must be either the symbol ``*'' or the name of a single-threaded object. In either case, the multiplicity of fn is 1 and val indicates whether the result is ordinary or a stobj. Otherwise, val is of the form (mv y1 ... yk), where k > 1. Each yi must be either the symbol ``*'' or the name of a stobj. Such a val indicates that fn has multiplicity k and the yi indicate which results are ordinary and which are stobjs. No stobj name may occur twice among the yi.

Finally, a stobj name may appear in val only if appears among the xi.

Before ACL2 supported user-declared single-threaded objects there was only one single-threaded object: ACL2's built-in notion of state. The notion of signature supported then gave a special role to the symbol state and all other symbols were considered to denote ordinary objects. ACL2 still supports the old form of signature, but it is limited to functions that operate on ordinary objects or ordinary objects and state.

Old-Style General Form:
(fn formals result)

where fn is the constrained function symbol, formals is a suitable list of formal parameters for it, and result is either a symbol denoting that the function returns one result or else result is an mv expression, (mv s1 ... sn), where n>1, each si is a symbol, indicating that the function returns n results. At most one of the formals may be the symbol STATE, indicating that corresponding argument must be ACL2's built-in state. If state appears in formals then state may appear once in result. All ``variable symbols'' other than state in old style signatures denote ordinary objects, regardless of whether the symbol has been defined to be a single-threaded object name!

We also support a variation on old style signatures allowing the user to declare which symbols (besides state) are to be considered single-threaded object names. This form is

(fn formals result :stobjs names)