SIGNATURE

Major Section:  MISCELLANEOUS

We start with a gentle introduction to signatures, where we pretend that there are no single-threaded objects (more on that below -- for now, if you don't know anything about single-threaded objects, that's fine!). Here are some simple examples of signatures.

((hd *) => *)
((pair * *) => *)
((foo * *) => (mv * * *))

(defun bar (x y)
  (mv y x (cons x y)))

Corresponding ``old-style'' signatures are as follows. In each case, a function symbol is followed by a list of formal parameters and then either t, to denote a single value return, or (mv t t t), to denote a multiple value return (in this case, returning three values).

(hd (x) t)
(pair (x y) t)
(foo (x y) (mv t t t))

That concludes our gentle introduction. The documentation below is more general, for example covering single-threaded objects and keyword values such as :guard. When reading what follows below, it is sufficient to know about single-threaded objects (or ``stobjs'') that each 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 or defabsstobj. An object that is not a single-threaded object is said to be ``ordinary.'' For a discussion of single-threaded objects, see stobj.

Examples:
((hd *) => *)
((hd *) => * :formals (x) :guard (consp x))
((printer * state) => (mv * * state))
((mach * mach-state * state) => (mv * mach-state))

General Form:
((fn ...) => *)
((fn ...) => stobj)
or
((fn ...) => (mv ...))
or for part1 and part2 as above,
(part1 => part2 :kwd1 val1 ... :kwdn valn)

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.

A signature typically has the form ((fn x1 ... xn) => val). Such 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, and a stobj name may appear in val only if appears among the xi.

A signature may have the form ((fn x1 ... xn) => val . k), where k is a keyword-value-listp, i.e., an alternating list of keywords and values starting with a keyword. In this case ((fn x1 ... xn) => val) must be a legal signature as described above. The legal keywords in k are :GUARD and :FORMALS (except that for ACL2(r), also see the remark about :CLASSICALP later in this topic). The value following :FORMALS is to be the list of formal parameters of fn, while the value following :GUARD is a term that is to be the guard of fn. Note that this guard is never actually evaluated, and is not subject to the guard verification performed on functions introduced by defun (see verify-guards). Said differently: this guard need not itself have a guard of t. Indeed, the guard is only used for attachments; see defattach. Note that if :GUARD is supplied then :FORMALS must also be supplied (in order to related the variables occurring in the guard to the parameters of fn). One final observation about guards: if the :GUARD keyword is omitted, then the guard defaults to T.

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 . k)

where fn is the constrained function symbol, formals is a suitable list of formal parameters for it, k is an optional keyword-value-listp (see below), 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!

The optional k is as described above for newer-style signatures, except that the user is also allowed to declare which symbols (besides state) are to be considered single-threaded object names. Thus :STOBJS is also a legal keyword. The form

(fn formals result ... :stobjs names ...)

As promised above, we conclude with a remark about an additional keyword, :CLASSICALP, that is legal for ACL2(r) (see real). The value of this keyword must be t (the default) or nil, indicating respectively whether fn is classical or not.