|
|
|---|
|
|
|
|---|
Programming using the von Neumannesque ACL2 state object
This documentation section introduces some common techniques for programming using the ACL2 state object. A prerequisite is thus a basic understanding of that object; see state. We hope this section is useful, and we invite suggestions for improvements and additions.
A supplement to this section is the ACL2 source code, which uses most (and probably all) of the techniques discussed here. That code is thus a source of many examples, which can serve as ``templates'' to guide one's own programming with state.
Recall that ``ACL2'' stands for ``A Computational Logic for Applicative Common Lisp''. In particular, the language is applicative: there are no global variables or side effects. For many purposes this does not feel restrictive; for example, an ACL2 user who is programming in raw Lisp may well be more comfortable coding a factorial function applicatively, using recursion, rather than using iteration with repeated assignment to the same variable.
However, there are situations that call for reading or modifying the system state, such as performing input and output, signaling errors, saving information from one computation for use in a later one, or reading and updating system-level or environmental data. This section provides an introductory guide for writing functions that traffic in state. We emphasize that this guide is intended as an introduction; more complete documentation may often be found by following links to documentation of individual utilities, and again, more examples may be found by searching the ACL2 source code for uses of the functions and macros mentioned below. The rest of this section is organized as follows.
ENABLING PROGRAMMING WITH STATE STATE GLOBALS AND THE ACL2 LOGICAL WORLD A REMARK ON GUARDS ERRORS AND ERROR TRIPLES SEQUENTIAL PROGRAMMING BINDING VARIABLES USING ERROR TRIPLES BINDING STATE GLOBAL VARIABLES INPUT AND OUTPUT TIMINGS ENVIRONMENT AND SYSTEM REMARKS ON EVENTS AND LD ADVANCED TOPICS
ENABLING PROGRAMMING WITH STATE
In order to submit a definition that takes state as a formal
parameter, you must either declare
Consider for example the following trivial definition.
(defun foo (state) (mv 3 state))
If you submit the above definition in a fresh ACL2 session, you will get this error message.
ACL2 Error in ( DEFUN FOO ...): The variable symbol STATE should not be used as a formal parameter of a defined function unless you are aware of its unusual status and the restrictions enforced on its use. See :DOC set-state-ok.
If first you evaluate
(defun foo (state) (declare (xargs :stobjs state)) (mv 3 state))
A difference in the two approaches is that for the latter, a guard proof obligation is generated by default. See the section below entitled ``A remark on guards''.
STATE GLOBALS AND THE ACL2 LOGICAL WORLD
Recall (see state) that one of the fields of the ACL2 state object is the global-table, which logically is an alist associating symbols, known as ``state globals'' or ``state global variables'', with values. But no such alist actually exists in the implementation. Instead, ACL2 provides utilities for reading state globals — see @ and see f-get-global — and utilities for writing them — see assign and see f-put-global. The following log shows how they work; further explanation follows below.
ACL2 !>(assign my-var (+ 3 4)) 7 ACL2 !>(@ my-var) 7 ACL2 !>(f-put-global 'my-var (+ 1 5) state) <state> ACL2 !>(f-get-global 'my-var state) 6 ACL2 !>
Note that the first result is indented by one space. This is ACL2's way to indicate that the assign expression returned an ``error triple'' and that no error was signaled. We discuss error triples in more detail below; also see error-triple.
As illustrated above, the output signatures of the utilities for assigning
to state globals differ from each other as follows: f-put-global
returns
ACL2 !>:trans1 (@ my-var) (F-GET-GLOBAL 'MY-VAR STATE) ACL2 !>
State globals are useful for conveying persistent state information.
Consider for example the utility set-inhibit-output-lst. The form
A particularly useful state global is
You may wish to modify state globals within a book, but this can be
slightly problematic because only legal event forms (see embedded-event-form) may go into books. Fortunately there is a
workaround using
A REMARK ON GUARDS
For a function definition (see defun), if
We can illustrate this point by modifying the example above as follows, to
read the value of state global
(defun foo (state) (declare (xargs :stobjs state)) (f-get-global 'gag-mode state))
If you try this in a fresh ACL2 session, the proof will fail with the
following key checkpoint, which says that the state global
(IMPLIES (STATE-P1 STATE) (ASSOC-EQUAL 'GAG-MODE (NTH 2 STATE)))
How can we deal with this proof failure? One way is simply to ignore the
issue by defining the function in
(defun foo (state) (declare (xargs :stobjs state :mode :program)) (f-get-global 'gag-mode state))
Perhaps a better way is to strengthen the guard to assert that the indicated state global is bound, as follows.
(defun foo (state) (declare (xargs :guard (boundp-global 'gag-mode state) :stobjs state)) (f-get-global 'gag-mode state))
Also see guard-miscellany for discussion of guard generation from
xargs fields of declare forms, specifically, for keywords
ERRORS AND ERROR TRIPLES
When evaluation returns three values, where the first two are ordinary
objects and the third is the ACL2 state, the result may be called an ``error
triple''. (Whether it is treated as an error triple depends on the
programmer.) Error triples are often denoted
Even ACL2 users who are not programmers encounter error triples, because
these are the values returned by evaluation of ACL2 events. Consider
the following log, where the only user input is the
ACL2 !>(defun foo (x) x) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (EQUAL (FOO X) X). Summary Form: ( DEFUN FOO ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>
All output above results from explicit calls of output functions, except
for the next-to-last line, which contains
ACL2 !>:u
0:x(EXIT-BOOT-STRAP-MODE)
ACL2 !>(set-ld-post-eval-print t state)
(NIL T <state>)
ACL2 !>(defun foo (x) x)
Since FOO is non-recursive, its admission is trivial. We observe that
the type of FOO is described by the theorem (EQUAL (FOO X) X).
Summary
Form: ( DEFUN FOO ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(NIL FOO <state>)
ACL2 !>
The way error triples are printed by
It is so common to produce an error triple whose first (error flag)
component is
We turn now to the topic of errors. The macro er ``causes'' an
error, but there are really two quite different kinds of errors: ``soft'' and
``hard'' errors. We use the term ``soft error'' to refer to a form that
returns an error triple
Note that the function abort!, which you can invoke by typing
ACL2 !>(thm (equal (abort!) nil)) Q.E.D. Summary Form: ( THM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION ABORT!)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>(equal (abort!) nil) Abort to ACL2 top-level ... ACL2 !>
(What actually happens with a hard error, including non-default cases, is a
bit subtle; most readers will probably want to skip this paragraph. The
read-eval-print loop implemented by ld is implemented by a call of the
ACL2 evaluator function,
The most common way to signal errors is the macro er, which prints
a formatted error message and returns a soft or hard error as specified by the
call. Note however that soft errors are signaled using
Since the output signatures of soft and hard errors are different — hard errors ``return'' a single value while soft errors return a triple — mixing them in an expression requires embedding the hard error form in (an irrelevant) triple, as illustrated below. All branches of the expression must produce an error triple if any branch does.
ACL2 !>(defun chk-find-or-abort (e x state) (declare (xargs :mode :program)) (if (endp x) (value ; Note use of VALUE! (er hard 'chk-find-or-abort "Did not find ~x0!" e)) (if (not (integerp (car x))) (er soft 'chk-find-or-abort "Non-integer, ~x0, in list!" (car x)) (if (eql (car x) e) (value x) (chk-find-or-abort e (cdr x) state))))) Summary Form: ( DEFUN CHK-FIND-OR-ABORT ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CHK-FIND-OR-ABORT ACL2 !>(chk-find-or-abort 3 '(1 2 3 4 5) state) (3 4 5) ACL2 !>(chk-find-or-abort 3 '(1 A 3 4 5) state) ACL2 Error in CHK-FIND-OR-ABORT: Non-integer, A, in list! ACL2 !>(chk-find-or-abort 3 '(1 2 4 5) state) HARD ACL2 ERROR in CHK-FIND-OR-ABORT: Did not find 3! ... ACL2 !>
See er for further discussion of errors. For some other individual topics related to errors see assert$, see break-on-error, see error1, see hard-error, see illegal, and see ld-error-triples.
In the next section we discuss soft errors further, in the context of programming.
SEQUENTIAL PROGRAMMING
This section describes handy ways to modify state in steps, using macros
that implement a sequence of let or mv-let bindings. For
example, suppose you want to assign the values 1 and 2 to two state globals
(let ((state (f-put-global 'one-var 1 state))) (let ((state (f-put-global 'two-var 2 state))) state))
It is so common to bind state successively in such a manner that ACL2 provides a macro, pprogn, for this purpose. Thus, an equivalent solution to the problem above is
(pprogn (f-put-global 'one-var 1 state) (f-put-global 'two-var 2 state) state)
or, more simply, as follows.
(pprogn (f-put-global 'one-var 1 state) (f-put-global 'two-var 2 state))
See pprogn. Note that the last form is allowed to return multiple
values; the only requirement on the last form is that its value include
It is also common to update the state using a sequence of forms such that
each returns an error triple, where the intention is for evaluation to
short-circuit immediately if a soft error is encountered. Suppose
(mv-let (erp val state) <expr1> (cond (erp (mv erp val state)) (t <expr2>)))
But ACL2 provides a handy macro, er-progn, for this purpose. The following code is equivalent to the code just above.
(er-progn <expr1> <expr2>)
See er-progn for more details. Note that unlike pprogn, the return signature for the last expression must be the same as that of the others: an error triple.
Let's consider how to use
(pprogn (f1 x state) (er-progn (g1 x state) (pprogn (f2 x state) (g2 x state))))
Finally, consider the events progn and progn!.
These have similar behavior to that of er-progn. However, progn and progn! may only be used in event contexts, for example at
the top level or immediately underneath a call of encapsulate or
progn, while er-progn has no such restriction. So when
writing code, use
BINDING VARIABLES USING ERROR TRIPLES
In this section we discuss the macro
The macro
(er-let* ((x1 (f1 state)) (x2 (f2 x1 state))) (value (cons x1 x2)))
The code just above is essentially equivalent to writing the following.
(mv-let (erp x1 state) (f1 state) (cond (erp (mv erp x1 state)) (t (mv-let (erp x2 state) (f2 x1 state) (cond (erp (mv erp x2 state)) (t (value (cons x1 x2))))))))
As suggested by the example above,
Of course, soft errors can be ``caught'' by using mv-let instead of
BINDING STATE GLOBAL VARIABLES
In this section we introduce a utility, state-global-let*, that is
an analogue of
(state-global-let* ((inhibit-output-lst (add-to-set-eq 'summary (@ inhibit-output-lst)))) (thm (equal x x)))
This form binds state global variable
See state-global-let* for more complete documentation.
INPUT AND OUTPUT
In ACL2, most input and output involves the ACL2 state. See io.
TIMINGS
For how to obtain the time elapsed since the start of the ACL2 session, see read-run-time.
For a utility for saving times into the ACL2 state and for printing those
saved times, see the community book
To time an evaluation (though this really isn't about state), see time$.
ENVIRONMENT AND SYSTEM
Next, we mention briefly some ways in which ACL2 interacts with its environment using the ACL2 state.
For how to read and write environment variables, see getenv$ and see setenv$.
For how to run a command in the host operating system, see sys-call, sys-call+, and sys-call*.
REMARKS ON EVENTS AND LD
In general, undefined or surprising behavior may occur when using ACL2 events or calling ld in your programs. In some cases ACL2 enforces restrictions against these uses. We strongly discourage using ld in programs, as it has been designed to be called only at the top level of a read-eval-print loop. However, you may wish to read or write ld specials in your programs; see ld.
There is also a restriction on contexts in which make-event may be called: it may only be called in a context where an event is expected, such as the top level, in a book, or as an argument of encapsulate or progn. The reason is that ACL2 does very subtle and careful tracking of make-event expansions; and it is only able to do this in event contexts, where it is able to carry out such tracking accurately.
ADVANCED TOPICS
ACL2 provides the function
For a function that provides the true absolute filename, with soft links resolved, see canonical-pathname.
For a function that returns a checksum on the characters in a channel, see checksum.
To obtain a random number, see random$.
If you are programming in raw-mode (see set-raw-mode) or in raw
Lisp, use the variable
We invite suggestions for additional advanced topics.