Major Section: EVENTS
Examples: ACL2 !>(defstub subr1 (* * state) => (mv * state)) ACL2 !>(defstub add-hash (* * hashtable) => hashtable) General Forms: (defstub name args-sig => output-sig) (defstub name args-sig => output-sig :doc doc-string)
Name is a new function symbol and (name . args-sig) => output-sig) is
a signature. If the optional doc-string is supplied it should be
a documentation string. See also the ``Old Style'' heading below.
Defstub macro expands into an encapsulate event
(see encapsulate). Thus, no axioms are available about name but it may
be used wherever a function of the given signature is permitted. Exception:
if output-sig is of the form (mv ...), then a
:type-prescription rule is introduced stating that name returns
a value satisfying true-listp.
Old Style:
Old Style General Form: (defstub name formals output) (defstub name formals output :doc doc-string)where
name is a new function symbol, formals is its list of formal
parameters, and output is either a symbol (indicating that the function
returns one result) or a term of the form (mv s1 ... sn), where each
si is a symbol (indicating that the function returns n results).
Whether and where the symbol state occurs in formals and output
indicates how the function handles state. It should be the case that
(name formals output) is in fact a signature (see signature).Note that with the old style notation it is impossible to stub-out a function that uses any single-threaded object other than state. The old style is preserved for compatibility with earlier versions of ACL2.
