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 (see stobj), dfs
(see df), and keyword values such as :guard. When reading what
follows below, all you need 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. We also
mention “dfs”, which are ACL2 expressions that denote Lisp
floating-point values; see df. An expression that is neither a stobj
name nor a df is said to be ``ordinary''.
Examples:
((hd *) => *)
((hd *) => * :formals (x) :guard (consp x))
((printer * state) => (mv * * state))
((mach * mach-state * state) => (mv * mach-state))
((df-mult3 :df :df :df) => :df)
General Form:
((fn ...) => *)
((fn ...) => s) ; where s is a stobj name
((fn ...) => :df)
or
((fn ...) => (mv x1 x2 ... xn)) ; where each xi is *, a stobj, or :df
or for part1 and part2 as above,
(part1 => part2 :kwd1 val1 ... :kwdn valn)
where fn is the constrained function symbol 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) the arguments and results
that are stobjs or dfs.
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, or else that symbol must be
:df and the corresponding argument must be a df (see df). 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 ``*'', the keyword :df, 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, a df, or a stobj.
Otherwise, val is of the form (mv y1 ... yk), where k > 1.
Each yi must be either the symbol ``*'', the keyword :df, or the
name of a stobj. Such a val indicates that fn has multiplicity
k and the yi indicate which results are ordinary, which are dfs, 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 stobjs names or dfs. Thus :STOBJS and
@9':DFS') are also legal keywords. The form
(fn formals result ... :stobjs stobj-names :dfs df-names ...)
specifies that stobj-names is either the name of a stobj or else is a
list of such names; also, both stobj-names and df-names are lists
that must be contained in the formals list. Every name in
stobj-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.
