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 * * *))The first of these says that
hdis a function of one argument, while the other two say that
pairand
fooare functions that each take two arguments. The first two say that
hdand
pairreturn a single value. The third says that
fooreturns 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 (except that for ACL2(r), also see the remark
about
:CLASSICALP later in this topic).or
defabsstobj.
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.