File: ASSIGN.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (40 lines) | stat: -rw-r--r-- 1,695 bytes parent folder | download
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
<html>
<head><title>ASSIGN.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ASSIGN</h2>assign to a global variable in <code><a href="STATE.html">state</a></code>
<pre>Major Section:  <a href="OTHER.html">OTHER</a>
</pre><p>


<pre>
Examples:
(assign x (expt 2 10))
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))
<p>
General Form:
(assign symbol term)
</pre>

where <code>symbol</code> is any symbol (with certain enforced exclusions to
avoid overwriting ACL2 system ``globals'') and <code>term</code> is any ACL2
term that could be evaluated at the top-level.  <code>Assign</code> evaluates
the term, stores the result as the value of the given symbol in the
<code>global-table</code> of <code><a href="STATE.html">state</a></code>, and returns the result.  (Note:  the
actual implementation of the storage of this value is much more
efficient than this discussion of the logic might suggest.)
<code>Assign</code> is a macro that effectively expands to the more
complicated but understandable:

<pre>
(pprogn (f-put-global 'symbol term state)
        (mv nil (f-get-global 'symbol term state) state)).
</pre>

The macro <code><a href="_at_.html">@</a></code> gives convenient access to the value of such globals.
The <code>:</code><code><a href="UBT.html">ubt</a></code> operation has no effect on the <code>global-table</code> of <code><a href="STATE.html">state</a></code>.
Thus, you may use these globals to hang onto useful data structures
even though you may undo back past where you computed and saved
them.
<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>