1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<html>
<head><title>DEFSTUB.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFSTUB</h2>stub-out a function symbol
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Examples:
ACL2 !>(defstub subr1 (* * state) => (mv * state))
ACL2 !>(defstub add-hash (* * hash-table) => hash-table)
<p>
General Forms:
(defstub name args-sig => output-sig)
(defstub name args-sig => output-sig :doc doc-string)
</pre>
<p>
<code>Name</code> is a new function symbol and <code>(name . args-sig) => output-sig)</code>
is a <a href="SIGNATURE.html">signature</a>. If the optional <code><a href="DOC-STRING.html">doc-string</a></code> is supplied
it should be a documentation string. See also the ``Old Style''
heading below.<p>
<code>Defstub</code> macro expands into an <code><a href="ENCAPSULATE.html">encapsulate</a></code> event
(see <a href="ENCAPSULATE.html">encapsulate</a>). Thus, no axioms are available about <code>name</code>
but it may be used wherever a function of the given signature is
permitted.<p>
Old Style:
<pre>
Old Style General Form:
(defstub name formals output)
(defstub name formals output :doc doc-string)
</pre>
where <code>name</code> is a new function symbol, <code>formals</code> is its list of
formal parameters, and <code>output</code> is either a symbol (indicating
that the function returns one result) or a term of the form
<code>(mv s1 ... sn)</code>, where each <code>si</code> is a symbol (indicating that the
function returns <code>n</code> results). Whether and where the symbol
<code><a href="STATE.html">state</a></code> occurs in <code>formals</code> and <code>output</code> indicates how the
function handles <a href="STATE.html">state</a>. It should be the case that
<code>(name formals output)</code> is in fact a signature (see <a href="SIGNATURE.html">signature</a>).<p>
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.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
