Signature
How to specify the arity of a constrained function
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 * * *))
The first of these says that hd is a function of one argument, while
the other two say that pair and foo are functions that each take two
arguments. The first two say that hd and pair return a single
value. The third says that foo returns three values, much as the
following definition returns three values:
(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)
where fn is the constrained function symbol, ... is a list of
asterisks and/or the names of single-threaded objects, stobj is a
single-threaded object name, and the optional :kwdi and vali are as
described below. 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.
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 generally :GUARD and :FORMALS, but see remarks at the end of
this topic regarding :GLOBAL-STOBJS and :TRANSPARENT and, for
ACL2(r), :CLASSICALP. The value following :FORMALS is to be the
list of formal parameters of fn, which must be consistent with the
parameters specified in (fn x1 ... xn): they must both specify the same
arity (number of formal parameters) and the same stobj inputs. 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 as a list of distinct variables that
includes all variables occurring free in the specified guard. 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 the 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 ...)
specifies that names is either the name of a single-threaded object or
else is a list of such names. Every name in names must have been
previously defined as a stobj via defstobj or defabsstobj.
As promised above, we conclude with a remark about additional keywords.
The keyword :GLOBAL-STOBJS specifies the use of the macro,
with-global-stobj, in attachments (see defattach); see with-global-stobj for explanation of this keyword. The keyword
:TRANSPARENT specifies transparent functions; see transparent-functions. Finally, the keyword :CLASSICALP is legal for
ACL2(r) only (see real). The value of this keyword must be t (the
default) or nil, indicating respectively whether fn is classical or
not.
