Internal Note #157 Computational Logic, Inc. October 17, 1989 ** Draft ** A User's Manual for RCL ** DRAFT ** Matt Kaufmann [This work was supported in part at Computational Logic, Inc., by the Defense Advanced Research Projects Agency, ARPA Orders 6082 and 9151. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc., the Defense Advanced Research Projects Agency or the U.S. Government.] Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . 1 2. DEFUN-RCL . . . . . . . . . . . . . . . . . . . . . . 1 3. DEFMACRO-RCL . . . . . . . . . . . . . . . . . . . . 3 4. DO-RCL . . . . . . . . . . . . . . . . . . . . . . . 4 5. TAGBODY . . . . . . . . . . . . . . . . . . . . . . . 5 6. PROCLAIM-RCL . . . . . . . . . . . . . . . . . . . . 6 6.1. SPECIAL proclamations . . . . . . . . . . . . . . 6 6.2. FORCE-AUXILIARY-FUNCTIONS proclamations . . . . . 6 6.3. INHIBIT-AUXILIARY-LEMMAS proclamations . . . . . 6 6.4. POSTPROCESS-DEFNS proclamations . . . . . . . . . 7 7. DECLARE . . . . . . . . . . . . . . . . . . . . . . . 8 7.1. HINTS declarations . . . . . . . . . . . . . . . 9 7.2. FUNCTIONS declarations . . . . . . . . . . . . . 9 7.3. EVENTS declarations . . . . . . . . . . . . . . . 9 7.4. POSTPROCESS declarations . . . . . . . . . . . . 9 8. GLOBAL SWITCHES AND UTILITIES . . . . . . . . . . . . 10 8.1. The switch *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* 10 8.2. The switch *PRINT-SIMPLIFICATION-INFO-FLG* . . . 10 8.3. The switch *INSTRUMENT-FLG* . . . . . . . . . . . 11 8.4. The utility UBT-RCL . . . . . . . . . . . . . . . 11 8.5. The utility RCL-STATUS . . . . . . . . . . . . . 11 9. THE ALGORITHM . . . . . . . . . . . . . . . . . . . . 11 9.1. Creating the initial DEFNs . . . . . . . . . . . 11 9.2. Errors: The ERR function . . . . . . . . . . . . 12 9.3. Simplification of RCL state data structures . . . 13 9.4. Mutual recursion analysis . . . . . . . . . . . . 13 9.5. Trimming definitions . . . . . . . . . . . . . . 13 9.6. Eliminating superfluous parameters . . . . . . . 14 9.7. Recursion elimination . . . . . . . . . . . . . . 14 1. Introduction This note is an update and extension of CLI Internal Note 110, [1]. That note gives an introduction to an earlier version of the Rose Common Lisp (RCL) system, which is a verification system for a subset of Common Lisp in the following sense. The syntax of the RCL language is a subset of the syntax of Common Lisp (as defined by the Common Lisp manual [2]). The semantics of the RCL language is consistent with the description in [2]. Soon there will be a technical report [3] that gives a more rigorous account of the soundness of the RCL system. Actually, a by-product of the approach in this note is a rather thorough (if informal) account of semantic issues. Nevertheless, this note is simply an attempt to document carefully how to use the RCL system in its current form. A quick summary of the semantics of our system is that it allows one to verify partial correctness of programs in the usual sense, i.e. one proves properties that hold of programs when they terminate in other than an error state. The prerequisites for using this system are a working knowledge of the Boyer-Moore theorem prover [4] and a little knowledge of Common Lisp [2]. There are three basic ``commands'' of Common Lisp that are supported in RCL: DEFUN-RCL, DEFMACRO-RCL, and PROCLAIM-RCL (for proclaiming of special variables and other global state settings). It is also permitted to submit several DEFUN-RCL and DEFMACRO-RCL forms by using the command DO-RCL. The next three sections document DEFUN-RCL and DEFMACRO-RCL and their generalization DO-RCL. After that comes a discussion of how the system handles TAGBODY forms. This is followed by sections that describe the general PROCLAIM and DECLARE mechanisms, as well as the various global switches and utilities that are available to the user. We conclude with a summary of the algorithm that we use, concentrating especially on the simplifications (optimizations) that are performed. First though, let us point out that all this is built on top of the Boyer-Moore Theorem Prover [5, 4], also known as NQTHM, and in fact is actually built on top of PC-NQTHM [6, 7], an interactive ``proof-checker'' enhancement of NQTHM. There have been a few modifications in the NQTHM database structure to support RCL, but these shouldn't really be visible to the user. However, one is not allowed to use NOTE-LIB inside RCL to read in a library made under NQTHM (or PC-NQTHM) without RCL loaded, nor is one allowed to use NOTE-LIB inside NQTHM (or PC-NQTHM) to read in a library made under RCL.(implementation detail: we ensure this by creating a different THEOREM-PROVER-LIBRARY-VERSION for RCL) However, it's important to note that RCL is started up with a library called startup loaded in, and hence the BOOT-STRAP command should not be invoked.(We will probably explicitly disallow BOOT-STRAP in future versions.) The startup library has been built on top of libraries for bags, natural numbers, integers, and vectors (really, lists with vector-type operations), as documented in [8] and recently updated by Bill Bevier and Matt Wilding. We ignore system issues here, except to say that at CLInc, one may start up this system by giving the shell command rcl. Perhaps the most important modification of the NQTHM implementation is that the definition of a legal name has been altered. More precisely, the definition(of NQTHM's Lisp function LEGAL-CHAR-CODE-SEQ, actually) has been altered so that lower-case characters are now legal, and there are no special restrictions on the first character of a symbol (other than the restrictions on all the characters) except for one small one: if the first character is `*' then the second character may not be any of the characters `0' through `9'.(This is to avoid, at the very least, name conflicts with the executable counterparts of NQTHM functions. These functions all are of the form *1*. This restriction also guarantees that *!*QUOTE is not an evg, which is important in order for the DEFMACRO-RCL macros to expand as expected.) Actually, we also allow one additional non-alphanumeric character in our symbols, namely, the period (.). However, when a symbol appears in RCL code it is not allowed to start with a period. We reserve such symbols for system use, in particular .RCL-FLG, .MUTUAL-FLG, and .PLISTS (as described in the sections that follow). REMARK. The convention in this note is that all input is in lower case. All list expressions in the output are in upper case. ACKNOWLEDGEMENTS I'd like to thank my colleagues at Computational Logic, Inc., for pleasant and useful interactions. In particular, Larry Smith provided lots of useful feedback during the development of the current version of this system, and Larry Akers, Bob Boyer, and J Moore also were extremely helpful on a number of occasions. 2. DEFUN-RCL Syntax: (defun-rcl {decl} {form}*) Here, the syntactic restrictions on are the same as those for NQTHM function names, but modified as described at the end of the preceding section. For the discussion of DEFUN-RCL in this section we'll ignore the issue of declarations (denoted {decl} in the display above), returning to that in Section 7.(In the current implementation we only allow at most one DECLARE form per definition, which may however have many individual declarations; see Section 7. However, we expect to remove this restriction in a future implementation.) The result of executing this form is the creation of an NQTHM DEFN event with name *CL-. (In fact there can be more then one event, as will be explained in Sections 5 and 7. But in the simplest cases, where the system defaults are used and there are no DECLARE forms or TAGBODY forms, a single NQTHM DEFN event is created.) Moreover, as we will explain below, the DEFN has at least one extra formal parameter, .RCL-FLG. For example, if the user submits the command >(defun-rcl app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y)) then the system responds by creating and executing an NQTHM DEFN event: Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-APP (.RCL-FLG X Y) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) (*CL-APP T (CDR X) Y)) Y) F)) Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-APP is accepted under the principle of definition. Note that: (OR (OR (FALSEP (*CL-APP .RCL-FLG X Y)) (LISTP (*CL-APP .RCL-FLG X Y))) (EQUAL (*CL-APP .RCL-FLG X Y) Y)) is a theorem. [ 4.1 0.1 0.1 ] *CL-APP T > Recall that we call APP the corresponding NQTHM function for APP. Let's observe that the system can easily prove (prove-lemma *cl-app-append (rewrite) (equal (*cl-app t x y) (append x y))) Here then, briefly, is a description of the correspondence between this DEFUN-RCL and this DEFN; again, we refer the reader to [3] for a more rigorous explanation. In the example above, the Common Lisp definition of APP has two formal parameters, X and Y. The corresponding DEFN event defines *CL-APP to have three formal parameters: .RCL-FLG, X, and Y.(.RCL-FLG was called *SPECIAL-NAME* in [1]) In fact, .RCL-FLG will be the first formal parameter in any such *CL- function definition. The idea is that for any values x0 and y0, (*CL-APP T x0 y0) equals the value returned by the evaluation of (APP X Y) in a Lisp environment in which X and Y are bound respectively to x0 and y0. In the example above, T is the only value of .RCL-FLG that is of interest. However we can illustrate other values of .RCL-FLG in the following example. Notice that the NQTHM function *CL-TEST has not only the extra formal parameter .RCL-FLG and the formal X from the definition of TEST, but also has the extra formal parameter *UVW*. In general, all special variables whose values that are relevant to the execution of an RCL function show up as extra formals to the corresponding NQTHM function. Also, all extra formals besides .RCL-FLG occur after the original formal parameters in the list of formals, and are ordered alphabetically. Here then is the example; explanation follows. >(defun-rcl test (x) (if (consp x) (and (equal (car x) 3) (progn (setq *uvw* (cdr x)) t)) (throw 'badtest x))) Used the following non-boot-strap lemmas and functions in the simplification process: *CL-AND. (DEFN *CL-TEST (.RCL-FLG X *UVW*) (CASE .RCL-FLG (*1*TRUE (IF (LISTP X) (IF (EQUAL (CAR X) 3) 'T NIL) X)) (*1*FALSE (IF (LISTP X) F '(THROW BADTEST))) (*UVW* (IF (LISTP X) (IF (EQUAL (CAR X) 3) (CDR X) *UVW*) *UVW*)) (OTHERWISE F))) [ 0.3 0.0 0.0 ] *CL-TEST T > For readers not too familiar with the CASE syntax modification for Boyer-Moore logic, here is the body of the above DEFN written in traditional user syntax. (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (IF (EQUAL (CAR X) 3) 'T NIL) X) (IF (EQUAL .RCL-FLG F) (IF (LISTP X) F '(THROW BADTEST)) (IF (EQUAL .RCL-FLG '*UVW*) (IF (LISTP X) (IF (EQUAL (CAR X) 3) (CDR X) *UVW*) *UVW*) F))) Let's consider what this DEFN event says about *CL-TEST for each value of the input parameter .RCL-FLG. The case that .RCL-FLG is T is analogous to the previous example. It says that the value of the Lisp form (TEST X) for any particular X is (IF (LISTP X) (IF (EQUAL (CAR X) 3) 'T NIL) X). This is just as one would expect from looking at the definition of TEST, though perhaps the case where (LISTP X) is false is worth a comment. In this case the Lisp evaluation ends with evaluation of the form (THROW 'BADTEST X), and we simply adopt the convention that the value of a THROW is simply the value that was thrown (in this case, the value of X). (This and other seemingly vague verbiage can be made precise by defining an interpreter for RCL within the Boyer-Moore logic. In fact we've done just that, though that work is not yet polished.) This observation leads naturally to the next case of .RCL-FLG, namely where it equals F. In that case the value of *CL-TEST is the value of the signal present after executing the Lisp form (TEST X). We are thus led to the notion of a signal, which is an NQTHM term that represents the ``error condition'' part of the Lisp state. Normally this term is F, which denotes a ``normal'' state -- but when an exception is raised by THROW, CATCH, or even GO (in a TAGBODY, cf. Section 5), the signal is no longer F. In this case, the signal is F unless X is not a CONS pair (i.e. a LISTP), in which case the signal '(THROW BADTEST) arises from the THROW. The next case for .RCL-FLG in the above example is where .RCL-FLG is the special variable '*UVW*. Incidentally, although it's not shown here, there needs to be a preceding event (PROCLAIM-RCL '(SPECIAL *UVW*)) in order for this DEFUN-RCL form not to cause an error (see Subsection 6.1). At any rate, in this case of .RCL-FLG, the value of (TEST X) is intended to be the value of *UVW*. Inspection of that case in the DEFN event will show that the expected result is obtained, namely, *UVW* is unchanged except in the case that (LISTP X) and (EQUAL (CAR X) 3) hold, in which case *UVW* is set to (CDR X). Notice that *UVW* is an extra formal parameter of *CL-TEST, i.e. is a formal parameter of *CL-TEST which was not a formal parameter of TEST. Finally, in all remaining cases the value F is returned. Notice that this means that we can specify that a given special variable v is not changed by any terminating call of a function FOO, by saying the following (where x1 ... xn are the formals of *CL-FOO other than .RCL-FLG): (*) (OR (EQUAL (*CL-FOO 'v x1 ... xn) v) (EQUAL (*CL-FOO 'v x1 ... xn) F)) Let's see why (*) characterizes the property that the value of v is never changed by an execution of a call of FOO. If v is not a variable that is among the ``variables set'' of FOO, i.e. if 'v is not one of the cases of .RCL-FLG, then *CL-FOO returns F (by definition of *CL-FOO), and we're done. So suppose that v is one of the ``variables set'' of FOO, i.e. 'v is one of the cases of .RCL-FLG. For any terminating call of FOO, our spec is that (*CL-FOO 'v ...) returns the value of v after that call. Since this value can never be F (since (FALSE) is not a Common Lisp value), (*) above is equivalent to the statement that the value of v after running FOO is unchanged. We have described briefly how a DEFUN-RCL form produces a DEFN event. However, an additional effect recorded by the system is to record five properties of the function being defined: its VARIABLES-READ, VARIABLES-SET, RCL-STATE-VARS-READ, RCL-STATE-VARS-SET, and ERROR-SIGNALS.(In the implementation, these are actually properties stored on the property list of *CL-.) These properties indicate the interaction of the given function with the Lisp state. So in the TEST example above, we have the following entries on the property list of *CL-TEST: VARIABLES-READ (*UVW*) VARIABLES-SET (*UVW*) RCL-STATE-VARS-READ NIL RCL-STATE-VARS-SET NIL ERROR-SIGNALS ((THROW BADTEST)) This information is used when another function is defined using TEST. Consider the following example. (defun-rcl newtest (x) (let ((*uvw* *uvw*)) (setq *temp* nil) (test (cons x x)))) This yields the following DEFN event. Notice that *UVW* is among the special variables read (in fact the VARIABLES-READ property of *CL-NEWTEST is simply the one-element list (*UVW*)), because of the call to TEST. Also notice that *UVW* is not among the VARIABLES-SET because of the protection of *UVW* afforded by the LET in the definition of NEWTEST. Here the only special variable set is *TEMP*. (DEFN *CL-NEWTEST (.RCL-FLG X *UVW*) (CASE .RCL-FLG (*1*TRUE (*CL-TEST T (CONS X X) *UVW*)) (*1*FALSE (*CL-TEST F (CONS X X) *UVW*)) (*TEMP* NIL) (OTHERWISE F))) Next let us observe that we have taken care in our treatment of the Lisp function CATCH. So for example, the system is able to deduce that the CATCH in the following example catches all possible signals, so that the resulting signal is F: >(defun-rcl catch-newtest (x) (catch 'badtest (newtest x))) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-CATCH-NEWTEST (.RCL-FLG X *UVW*) (CASE .RCL-FLG (*1*TRUE (*CL-NEWTEST T X *UVW*)) (*TEMP* (*CL-NEWTEST '*TEMP* X *UVW*)) (OTHERWISE F))) [ 0.2 0.0 0.0 ] *CL-CATCH-NEWTEST T Later (Subsection 9.1) we will see how to coax the simplifier into producing a syntactically simpler value for the case *TEMP* above. We conclude this section with a brief discussion of state variables. At this time there is only one state variable, .PLISTS. which represents the property lists in the Lisp state as an association list, associating symbols with property-value association lists. For example, if a Lisp state has only two symbols with properties, X and Y, and if the property list of X is (FOO 3 BAR 4) and of Y is (BLOB 5), then .PLISTS is the list ((X (FOO 3) (BAR 4)) (Y (BLOB 5))). The following example, which follows a suggestion of Bob Boyer, illustrates the system's handling of property lists. In each case we'll give the input in lower-case and the resulting NQTHM DEFN event in upper-case. Here *PUTPROP and *GETPROP are defined in the RCL "GROUND-ZERO" (boot-strap) theory. For completeness, their definitions appear at the end of this section; they correspond quite closely to Lisp's traditional PUTPROP and GET functions. (defun-rcl putprops (symbols mark prop) ;; Puts the value MARK on the PROP property of each symbol in the list SYMBOLS (if (consp symbols) (progn (putprop (car symbols) mark prop) (putprops (cdr symbols) mark prop)) nil)) ;; Notice in the recursive call below that the actual parameter in .PLISTS's position ;; is the result of having done a PUTPROP of PROP on the MARK property of ;; the first element of SYMBOLS. (DEFN *CL-PUTPROPS (.RCL-FLG SYMBOLS MARK PROP .PLISTS) (CASE .RCL-FLG (*1*TRUE NIL) (.PLISTS (IF (LISTP SYMBOLS) (*CL-PUTPROPS '.PLISTS (CDR SYMBOLS) MARK PROP (*PUTPROP .PLISTS (CAR SYMBOLS) MARK PROP)) .PLISTS)) (OTHERWISE F))) (defun-rcl checkmarks (symbols prop) ;; Returns the list of symbols in the list SYMBOLS that have a non-nil PROP property (if (consp symbols) (if (get (car symbols) prop) (cons (car symbols) (checkmarks (cdr symbols) prop)) (checkmarks (cdr symbols) prop)) nil)) (DEFN *CL-CHECKMARKS (.RCL-FLG SYMBOLS PROP .PLISTS) (IF (EQUAL .RCL-FLG T) (IF (LISTP SYMBOLS) (IF (EQUAL (*GETPROP .PLISTS (CAR SYMBOLS) PROP NIL) NIL) (*CL-CHECKMARKS T (CDR SYMBOLS) PROP .PLISTS) (CONS (CAR SYMBOLS) (*CL-CHECKMARKS T (CDR SYMBOLS) PROP .PLISTS))) NIL) F)) (defun-rcl int (x y) ;; Returns the intersection of the lists X and Y of symbols by first ;; initializing the INT property of each symbol in the list X with NIL, then ;; putting T on the INT property of each symbol in the list Y, and finally ;; returning those symbols in the list X that have a non-NIL INT property. (putprops x nil 'int) (putprops y 't 'int) (checkmarks x 'int)) (DEFN *CL-INT (.RCL-FLG X Y .PLISTS) (CASE .RCL-FLG (*1*TRUE (*CL-CHECKMARKS T X 'INT (*CL-PUTPROPS '.PLISTS Y 'T 'INT (*CL-PUTPROPS '.PLISTS X NIL 'INT .PLISTS)))) (.PLISTS (*CL-PUTPROPS '.PLISTS Y 'T 'INT (*CL-PUTPROPS '.PLISTS X NIL 'INT .PLISTS))) (OTHERWISE F))) In fact, after giving a standard recursive definition of INTERSECT in NQTHM and proving three lemmas, the following lemma may be proved: (prove-lemma *cl-int-is-intersect (rewrite) (equal (*cl-int t x y plists) (intersect x y))) For reference, here are the two built-in function definitions promised above, together with a definition of PUT-ASSOC needed for the definition of *PUTPROP. (*getprop plists symbol prop default) = (let ((pair (assoc prop (cdr (assoc symbol plists))))) (if pair (cdr pair) default)) (put-assoc key val alist) = ;; Adds (key . val) at the end if key is not already a key of alist (if (listp alist) (if (equal key (caar alist)) (cons (cons key val) (cdr alist)) (cons (car alist) (put-assoc key val (cdr alist)))) (list (cons key val))) (*putprop plists symbol value prop) = (put-assoc symbol (put-assoc prop value (cdr (assoc symbol plists))) plists) 3. DEFMACRO-RCL Syntax: (defmacro-rcl {decl}* {form}*) The primary syntactic difference between such a form and a DEFUN-RCL form is in the allowable ``shape'' of the formal parameters. That is, the syntax for allows any CONS structure built from legal symbols (``legal'' in the sense described at the end of Section 1), including simply a single atom. Here are some examples of legal DEFMACRO-RCL forms and the DEFN forms they produce. (defmacro-rcl lazy-car (x) (if (and (consp x) (equal (car x) 'cons)) (car (cdr x)) `(car ,x))) (defmacro-rcl and x ;; from the startup file (and-fn x)) (defmacro-rcl prog (bindings . body) ;; from the startup file `(block nil (let ,bindings (tagbody ,@body)))) The DEFN forms produced by DEFMACRO-RCL tend to be quite ugly, but fortunately it should rarely be necessary for a user to look at them. The important thing about these DEFN forms (if indeed anything is particularly important about them, fro the user's point of view!) is that they always take two formal parameters: .RCL-FLG (of course) and a parameter that is intended to represent an entire call of the macro (including the macro itself, which is the CAR of such a form). Here, for example, is the DEFN event produced for the LAZY-CAR example above. (DEFN *CL-LAZY-CAR (.RCL-FLG LAZY-CAR-WHOLE) (CASE .RCL-FLG (*1*TRUE (IF (LISTP (CDR LAZY-CAR-WHOLE)) (IF (EQUAL (CDDR LAZY-CAR-WHOLE) NIL) (IF (LISTP (CADR LAZY-CAR-WHOLE)) (IF (EQUAL (CAADR LAZY-CAR-WHOLE) 'CONS) (*CL-CAR<> (CDADR LAZY-CAR-WHOLE)) (LIST 'CAR (CADR LAZY-CAR-WHOLE))) (LIST 'CAR (CADR LAZY-CAR-WHOLE))) '(MACROEXPAND-ERROR (TOO MANY ARGUMENTS))) '(MACROEXPAND-ERROR (NOT ENOUGH ARGUMENTS)))) (*1*FALSE (IF (LISTP (CDR LAZY-CAR-WHOLE)) (IF (EQUAL (CDDR LAZY-CAR-WHOLE) NIL) F '(ERROR)) '(ERROR))) (OTHERWISE F))) The way macros work in RCL is intended to be essentially the same as how they are specified to work in Common Lisp. That is, once a DEFMACRO-RCL, say of a function FOO, has been accepted, future DEFMACRO-RCL and DEFUN-RCL definitions will macroexpand calls of FOO: the body of any future definition is traversed (outside-in) as it is analyzed, and whenever a call of FOO is encountered, FOO is run on its argument list (which is bound to the formals of FOO as indicated by the structured defmacro-lambda-list).[More precisely, *CL-FOO is run on T together with the list of arguments (QUOTE x) as x ranges over the arguments of FOO.] Of course, in the implementation this means that the executable counterpart of *CL-FOO is run with its .RCL-FLG parameter being T (T representing value, cf. Section 2.) At this point the alert reader may have a couple of concerns. One concern is: what if FOO depends on some values of special variables or state variables? What values do we use for those when we are executing FOO? At this time we don't carry around a notion of the global Lisp state, so we simply disallow DEFMACRO-RCLs that read any special variables or state variables. We also disallow DEFMACRO-RCLs that SET any special variables or state variables, since there's no mechanism for reflecting that setting. Finally, any time that an RCL macro (say, FOO) is to be executed, the system first calls the executable counterpart of *CL-FOO with .RCL-FLG set to FALSE, to help to ensure that a real compilation of that Lisp definition would not cause an error.(More genuine certainty will be obtained when we implement total correctness checking. For now, we only wish to claim that when a DEFMACRO doesn't cause an error or fail to terminate, then its meaning is reflected in the corresponding DEFMACRO-RCL.) Finally, we should clarify a potential point of confusion. Recall the correspondence between Lisp functions defined by DEFUN-RCL and NQTHM DEFN functions discussed in the preceding section. For DEFMACRO-RCL functions, there is a similar correspondence -- similar, at least, if one thinks of a macro in terms of the function that it defines, a function which takes code and returns new code. Here are some examples that illustrate *CL-LAZY-CAR, where LAZY-CAR was defined above using DEFMACRO-RCL: >(r-loop) Abbreviated Output Mode: On Type ? for help. *(*cl-lazy-car t '(lazy-car x)) '(CAR X) *(*cl-lazy-car t '(lazy-car (cons x y))) 'X *(*cl-lazy-car f '(lazy-car (cons x y))) F *(*cl-lazy-car t '(lazy-car x y)) '(MACROEXPAND-ERROR (TOO MANY ARGUMENTS)) *(*cl-lazy-car f '(lazy-car x y)) '(ERROR) To summarize this point: the *CL- function defined by DEFN to ``correspond'' to a DEFMACRO-RCL is intended to represent what is called in Common Lisp the expansion function for the macro, i.e. the function returned by the Lisp function MACRO-FUNCTION, and not the result of evaluating the resulting form. One more example should illustrate this point. (*cl-lazy-car t '(lazy-car (cons (cdr '(1 2)) 7))) = '(CDR '(1 2)) Notice that the right-hand side above is not '(2), even though (using simplification with rewrite rules) it is the case that (defun-rcl lazy-car-test () (lazy-car (cons (cdr '(1 2)) 7))) produces (DEFN *CL-LAZY-CAR-TEST (.RCL-FLG) (IF (EQUAL .RCL-FLG T) '(2) F)) Perhaps we should mention one subtlety. There are perhaps two notions of ``recursive macro'' that one might imagine, but only one of them (the reasonable one) is allowed here. Here is an example of an acceptable ``recursive macro'' (one which takes repeated CDRs at definition time, when possible): (defmacro-rcl lazy-cdr* (x) (if (and (consp x) (equal (car x) 'cons)) (list 'lazy-cdr* (car (cddr x))) (list 'cdr x))) So for example, we have the following sample use of LAZY-CDR*. Notice that the form (SETQ X 8) is not relevant but would have been very relevant if LAZY-CDR* were an ordinary function that evaluates all its arguments. (defun-rcl foo (x) (cons 3 (lazy-cdr* (cons (setq x 7) (cons (setq x 8) x))))) (DEFN *CL-FOO (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (CONS 3 (*CL-CDR<> X)) F)) However, it is an error to actually call a macro before the process of defining that macro (i.e. the execution of the DEFMACRO-RCL or DO-RCL in which it is defined) is entirely complete. That kind of recursion seems a sufficiently strange thing to do that it seems difficult to think of a reasonable example of how to violate this requirement with recursion. An unreasonable example might be (defmacro-rcl boo (x) (if (consp x) (boo (cdr x)) 3)). 4. DO-RCL First we need a definition. Let's say that one DEFN form depends on another if the body of the first contains a call of the function defined by the other. If one has a sequence of DEFN forms then this notion induces a binary relation on those forms, which we will call the dependency relation. There is always a smallest transitive-reflexive relation(i.e. preorder) R* generated by a binary relation R on a set, namely x R* y iff there is a sequence x = x R x R ... R x = y. Consider the 0 1 n equivalence relation E on the field of R which is defined as follows: x E y iff (x R* y and y R* x). In the case where R is the dependency relation on a set of definitions, we will call the equivalence classes of E the dependency classes. We have seen how to use DEFUN-RCL and DEFMACRO-RCL. But what do we do when our definitions may be mutually recursive? In this case we may use DO-RCL. If the definitions turn out not to be mutually recursive after all, then DO-RCL could have been avoided in favor of submitting the definitions one after the other (in the proper order). However, if there is mutual recursion then one extra function is created for each dependency class (see paragraph above) of size greater than 1. That function has as its formal parameters the union of the formal parameters of the definitions in that dependency class together with one extra formal parameter, .MUTUAL-FLG (possibly suffixed by a number to make it a new parameter). The auxiliary functions will have names of the form =n where is the first argument of DO-RCL and n is a number (chosen by the system so that the resulting name will be new).(More on mutual recursion in NQTHM may be found in [9]. Though there are some minor differences in detail between the implementation described there and the one described here, the principles are the same and the pace is more leisurely there.) Here is an example. Notice that MUT-1 and MUT-2 are mutually recursive, as are MUT-3 and MUT-4. (do-rcl mutts (defun-rcl mut-1 (x) (if (consp x) (cons (car x) (mut-2 (cdr x))) nil)) (defun-rcl mut-2 (x) (if (consp x) (cons (car x) (mut-1 (cdr x))) nil)) (defun-rcl mut-3 (x) (if (consp x) (cons (car x) (mut-4 (cdr x))) nil)) (defun-rcl mut-4 (x) (if (consp x) (cons (car x) (mut-3 (cdr x))) nil)) ) The system is able to deduce the dependency graph, and it creates the following DEFN events. Notice that *CL-MUT-1 and *CL-MUT-2 are in the same dependency class, as are *CL-MUT-3 and *CL-MUT-4. MUTTS=0 is created for the first pair of functions, where its parameter .MUTUAL-FLG determines whether the value of MUTTS=0 represents the value of *CL-MUT-2 or *CL-MUT-1, according to whether .MUTUAL-FLG is '*CL-MUT-2 or not. (Similarly for MUTTS=1, *CL-MUT-4, and *CL-MUT-3.) (DEFN MUTTS=0 (.MUTUAL-FLG .RCL-FLG X) (COND ((EQUAL .MUTUAL-FLG '*CL-MUT-2) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) (MUTTS=0 '*CL-MUT-1 T (CDR X))) NIL) F)) ((EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) (MUTTS=0 '*CL-MUT-2 T (CDR X))) NIL)) (T F))) (DEFN *CL-MUT-2 (.RCL-FLG X) (MUTTS=0 '*CL-MUT-2 .RCL-FLG X)) (DEFN *CL-MUT-1 (.RCL-FLG X) (MUTTS=0 '*CL-MUT-1 .RCL-FLG X)) (DEFN MUTTS=1 (.MUTUAL-FLG .RCL-FLG X) (COND ((EQUAL .MUTUAL-FLG '*CL-MUT-4) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) (MUTTS=1 '*CL-MUT-3 T (CDR X))) NIL) F)) ((EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) (MUTTS=1 '*CL-MUT-4 T (CDR X))) NIL)) (T F))) (DEFN *CL-MUT-4 (.RCL-FLG X) (MUTTS=1 '*CL-MUT-4 .RCL-FLG X)) (DEFN *CL-MUT-3 (.RCL-FLG X) (MUTTS=1 '*CL-MUT-3 .RCL-FLG X)) If there are DECLARE forms then those forms are all gathered together into a single set of DECLARE forms; see Section 7 for details. Finally, we note that for convenience we have arranged things so that inside DO-RCL, one may use DEFUN or DEFMACRO in place of DEFUN-RCL or DEFMACRO-RCL without any change in functionality whatsoever. 5. TAGBODY In general, additional *CL- functions may be created by DEFUN-RCL or DEFMACRO-RCL to reflect iteration. We will call these tagbody functions because the iteration form we support is TAGBODY. (Many readers will prefer to use the PROG macro, whose definition may be found in Section 3.) The idea is that each call of TAGBODY is replaced by a new Lisp function of one argument, that argument representing a tag giving the entry point in that TAGBODY code. If the first form in the tagbody is not a tag, i.e. is not an integer or a symbol, then the tag TAGBODY-START (suffixed by a number to make it a new tag, if necessary) is inserted as the first argument of the TAGBODY form; this tag is then the one which the ``tagbody function'' is initially called. More precisely, the system implicitly defines a Lisp function using DEFUN-RCL which we'll call a tagbody function. Its name is created by suffixing -TAGBODY-0 to the name of the function in which a tagbody occurs (at least for the first such tagbody that the system encounters; later ones are then the result of suffixing -TAGBODY-1, -TAGBODY-2, etc. to the main function name). It has one formal parameter, TAG.(Actually, as usual with such things, TAG is suffixed by a numeral if necessary in order to avoid name clashes, this time with the lexical and special variables in the given context.) This function is called initially with its argument equaling the topmost tag in the tagbody. Then the translation process creates an NQTHM DEFN named by prefixing *CL- to the name of this tagbody function the NQTHM function. However, let us note that this DEFN may be optimized by the system in various ways; for example the formals .RCL-FLG and TAG may be dropped. (More on such optimizations may be found in Section 9.) The important thing is that the final definition, which corresponds to the original DEFUN-RCL function (e.g., *CL-LASTCDR corresponds to LASTCDR in the example below) correctly models the behavior of that NQTHM function. Let us look at a simple example. The RETURN-FROM form reflects our adherence to the specification of DEFUN in Common Lisp that there is an implicit BLOCK around the function body, where the tag of that implicit BLOCK form equals the name of the function being defined. >(defun-rcl lastcdr (x) (tagbody loop (if (consp x) (setq x (cdr x)) (return-from lastcdr x)) (go loop))) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-LASTCDR-TAGBODY-0 (X) (IF (LISTP X) (*CL-LASTCDR-TAGBODY-0 (CDR X)) X)) Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-LASTCDR-TAGBODY-0 is accepted under the principle of definition. [ 0.1 0.1 0.1 ] *CL-LASTCDR-TAGBODY-0 (DEFN *CL-LASTCDR (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (*CL-LASTCDR-TAGBODY-0 X) F)) [ 0.1 0.0 0.0 ] *CL-LASTCDR T > Just as in the case of the main function (i.e. the NQTHM function that corresponds to the one defined by DEFUN-RCL), the NQTHM function that corresponds to a tagbody function may have extra formal parameters for the special (and state) variables that it needs (reads). Here is another example. Recall from Sectio 3 that a PROG macroexpands into a TAGBODY; more on this below. >(defun-rcl rev1 (x) (prog (acc) loop (when (not (consp x)) (return acc)) (setq acc (cons (car x) acc)) (setq x (cdr x)) (go loop))) Used the following non-boot-strap lemmas and functions in the simplification process: *CL-NOT-REWRITE, *CL-NOT<>-REWRITE, *CL-RETURN, *CL-WHEN, and *CL-PROG. (DEFN *CL-REV1-TAGBODY-0 (ACC X) (IF (LISTP X) (*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC) (CDR X)) ACC)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-REV1-TAGBODY-0 is accepted under the definitional principle. From the definition we can conclude that: (OR (LISTP (*CL-REV1-TAGBODY-0 ACC X)) (EQUAL (*CL-REV1-TAGBODY-0 ACC X) ACC)) is a theorem. [ 0.1 0.1 0.1 ] *CL-REV1-TAGBODY-0 (DEFN *CL-REV1 (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (*CL-REV1-TAGBODY-0 NIL X) F)) Note that: (OR (FALSEP (*CL-REV1 .RCL-FLG X)) (LITATOM (*CL-REV1 .RCL-FLG X)) (LISTP (*CL-REV1 .RCL-FLG X))) is a theorem. [ 0.1 0.0 0.0 ] *CL-REV1 T As mentioned above, notice that PROG is provided in the RCL system, just as it is in Common Lisp. For example: >(r-loop) Abbreviated Output Mode: On Type ? for help. *(*cl-prog t '(prog (acc) loop (when (not (consp x)) (return acc)) (setq acc (cons (car x) acc)) (setq x (cdr x)) (go loop))) '(BLOCK NIL (LET (ACC) (TAGBODY LOOP (WHEN (NOT (CONSP X)) (RETURN ACC)) (SETQ ACC (CONS (CAR X) ACC)) (SETQ X (CDR X)) (GO LOOP)))) * The important thing about this example, anyhow, is that ACC is treated like a special variable from the point of view of the TAGBODY form, as is easily seen from the macroexpanded form (BLOCK NIL (LET (ACC) (TAGBODY ...))) above. This fact shows up in the inclusion of ACC as an extra formal parameter in *CL-REV1-TAGBODY-0. Interestingly, the body of this function corresponds not to the value of the TAGBODY form but rather to the value of ACC. We'll come back to this example in Section 9. For now, suffice it to say that the original body of *CL-REV1-TAGBODY-0 (before any simplification) was as follows; but the main function *CL-REV1 only calls this function with .RCL-FLG set to 'ACC, so the other branches of the CASE were discarded by the system. The unsimplified body of *CL-REV1-TAGBODY-0 is actually as follows. (CASE .RCL-FLG (*1*TRUE (IF (LISTP X) (*CL-REV1-TAGBODY-0 T 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC)) (*1*FALSE (IF (LISTP X) (*CL-REV1-TAGBODY-0 F 'LOOP (CONS (CAR X) ACC) (CDR X)) '(RETURN-FROM ()))) (ACC (IF (LISTP X) (*CL-REV1-TAGBODY-0 'ACC 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC)) (X (IF (LISTP X) (*CL-REV1-TAGBODY-0 'X 'LOOP (CONS (CAR X) ACC) (CDR X)) X)) (OTHERWISE F)) 6. PROCLAIM-RCL Syntax: (proclaim-rcl (quote (kind . rest)) {event-name}) Here kind is one of SPECIAL, FORCE-AUXILIARY-FUNCTIONS, INHIBIT-AUXILIARY-LEMMAS, or POSTPROCESS-DEFNS. (In general, the list of such legal kinds is kept in the Lisp variable *LEGAL-RCL-PROCLAMATION-TYPES*.) Notice that PROCLAIM-RCL is a new kind of event (unlike DEFUN-RCL and DEFMACRO-RCL, which create DEFN events but aren't themselves events). Hence it is subject to the usual undoing mechanism, e.g. using the NQTHM command UBT.(However, we do not attempt to track dependencies on PROCLAIM-RCL events. In particular, if a DEFUN-RCL form uses a special variable and the proclaiming of the variable is undone by UNDO-NAME, then the database will be in a state that is not re-creatable without using UNDO-NAME. This situation is analogous to the situation with DISABLE and ENABLE events in NQTHM.) Also notice that some of the PROCLAIM-RCL proclamations also make sense in a local setting; see Section 7. 6.1 SPECIAL proclamations The event (PROCLAIM-RCL '(SPECIAL )) declares the variable to be special in the usual Lisp sense, i.e. to have the property that it may be referenced in functions without being passed explicitly. The following example should perhaps suffice. >(defun-rcl fff (x) (setq *zzz* x) 3) Error: ERROR SIGNALLED BY RCL FUNCTION.... The variable *ZZZ* is neither lexical nor special in (SETQ *ZZZ* X) Error signalled by EVAL. Broken at DO-RCL-FN. Type :H for Help. >>:q Top level. >(proclaim-rcl '(special *zzz*)) [ 0.0 0.0 0.0 ] DEFVAR-*ZZZ* >(defun-rcl fff (x) (setq *zzz* x) 3) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-FFF (.RCL-FLG X) (CASE .RCL-FLG (*1*TRUE 3) (*ZZZ* X) (OTHERWISE F))) Recall that the event name for PROCLAIM-RCL is an optional second argument. For SPECIAL proclamations we have a particular way of assigning the default: (PROCLAIM-RCL '(SPECIAL )) generates a PROCLAIM-RCL event named DEFVAR-. The same effect could be obtained with (PROCLAIM-RCL '(SPECIAL ) DEFVAR-), but if a different name is desired, a different optional argument could be supplied, as in: >(proclaim-rcl '(special *abc*) does-this-make-my-point?) [ 0.0 0.0 0.0 ] DOES-THIS-MAKE-MY-POINT? > 6.2 FORCE-AUXILIARY-FUNCTIONS proclamations An auxiliary function is a function defined by an NQTHM DEFN event that was created in response to DEFUN-RCL, DEFMACRO-RCL, or DO-RCL, but is not the NQTHM function corresponding to any function defined explicitly by DEFUN-RCL or DEFMACRO-RCL. The extra functions created by mutual recursion and by tagbody forms are examples of auxiliary functions, but in this subsection we will be concerned with another type of auxiliary function, namely one that corresponds to the value, signal, or value of a special or state variable after a call of a Lisp function. Let us call these sub-functions. By ``Lisp function'' here we mean any name defined by DEFUN-RCL or DEFMACRO-RCL, including those DEFUN-RCL forms created behind-the-scenes for tagbody functions (cf. Section 5). The event (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS T)) causes auxiliary functions to be created for each *CL- function arising from a DEFUN-RCL or DEFMACRO-RCL definition (including functions arising from TAGBODY forms; see Section 5): one for the value of the function, one for the signal corresponding to the function, and one for each special variable and state variable(i.e., .PLISTS) potentially set by the function. The auxiliary function names are obtained from the main *CL- function name by suffixing `<>' for the value, `<>signal' for the signal, and `' for a special variable or state variable v. Here is an example. (defun-rcl sweep1 (x) (if (consp x) (progn (sweep1 (cdr x)) (sweep1 (car x)) nil) (setq ans (cons x ans)))) This definition of SWEEP1 generates DEFN events *CL-SWEEP1<> and *CL-SWEEP1, for the value of a function call and of the special variable ANS after executing a call (respectively). (DEFN *CL-SWEEP1<> (X ANS) (IF (LISTP X) NIL (CONS X ANS))) (DEFN *CL-SWEEP1 (X ANS) (IF (LISTP X) (*CL-SWEEP1 (CAR X) (*CL-SWEEP1 (CDR X) ANS)) (CONS X ANS))) (DEFN *CL-SWEEP1 (.RCL-FLG X ANS) (CASE .RCL-FLG (*1*TRUE (*CL-SWEEP1<> X ANS)) (ANS (*CL-SWEEP1 X ANS)) (OTHERWISE F))) Notice that *CL-SWEEP1<>SIGNAL was not created. In fact, when the system can determine that the signal is identically F, it will not create an auxiliary function for the signal, preferring instead to use F directly as the value of the signal (as part of the "OTHERWISE" case). Similarly, (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS NIL)) turns off this feature. The default is NIL, i.e. these auxiliary functions are not created until the command (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS T)) is given. (Of course, (PROCLAIM-RCL '(FORCE-AUXILIARY-FUNCTIONS NIL)) would then turn this feature off again.) These events are assigned names by default: FORCE-AUXILIARY-FUNCTIONS-ON and FORCE-AUXILIARY- FUNCTIONS-OFF (possibly with numeric suffixes, in order to create new names for the events). However, as with all PROCLAIM-RCL events the user is welcome to provide the name of the event as an optional second argument, e.g. (PROCLAIM-RCL '(FORCE-AUXILIARY- FUNCTIONS NIL) PROCLAIM-TEST). It is an error to (FORCE-AUXILIARY-FUNCTIONS T) when auxiliary functions are already forced or to (FORCE-AUXILIARY-FUNCTIONS NIL) when they are already non-forced. 6.3 INHIBIT-AUXILIARY-LEMMAS proclamations The event (PROCLAIM-RCL '(INHIBIT-AUXILIARY-LEMMAS T)) causes auxiliary lemmas to be created and proved, as described below; (PROCLAIM-RCL '(INHIBIT-AUXILIARY-LEMMAS NIL)) turns off this feature. The default is NIL, i.e. auxiliary lemmas are not inhibited; they will be created until (PROCLAIM-RCL '(INHIBIT- AUXILIARY-LEMMAS T)) is executed. Notice that if there are no auxiliary functions created then there will be no auxiliary lemmas. The naming conventions for the resulting event are the same as for FORCE-AUXILIARY-FUNCTIONS, except of course that the defaults have a prefix of INHIBIT-AUXILIARY-LEMMAS rather than of FORCE-AUXILIARY-FUNCTIONS. One auxiliary lemma is created for each auxiliary sub-function that is created by the mechanism of the preceding subsection, i.e. that corresponds to the value, signal, or value of a special or state variable after a call of a function defined by DEFUN-RCL or DEFMACRO-RCL (including tagbody functions). All auxiliary lemmas are run at the end of whatever other events are created by DEFUN-RCL, DEFMACRO-RCL, or DO-RCL. Each such lemma is of the following form, where (say) *cl-foo_suffix is the name of the sub-function, *cl-foo is the function from which that sub-function was derived, and flag refers to T, F, or v, according to whether the sub-function corresponds to the value, the signal, or the variable v (respectively). (prove-lemma *cl-foo_suffix-rewrite (rewrite) (equal (*cl-foo flag ...args...) (*cl-foo_suffix ...args...))) Consider the example of SWEEP1 described in the preceding subsection. In that example, two auxiliary functions were created. The following lemmas would subsequently be created as well, assuming that auxiliary lemmas were not inhibited (which, once again, is the default). (PROVE-LEMMA *CL-SWEEP1<>-REWRITE (REWRITE) (EQUAL (*CL-SWEEP1 T X ANS) (*CL-SWEEP1<> X ANS))) (PROVE-LEMMA *CL-SWEEP1-REWRITE (REWRITE) (EQUAL (*CL-SWEEP1 'ANS X ANS) (*CL-SWEEP1 X ANS))) To summarize, then, suppose that auxiliary lemmas are not inhibited. (Again, this is the default.) Then it is the case that at the end of the sequence of events that would otherwise be executed, one lemma is created for each sub-function. Each such lemma instructs the rewriter to replace various function calls with calls of corresponding sub-functions in future simplifications and proofs. 6.4 POSTPROCESS-DEFNS proclamations The event (PROCLAIM-RCL '(POSTPROCESS-DEFNS NIL)) turns off a feature that we call definition postprocessing. It turns out that among the several kinds of simplifications that we do, there is a kind of recursion elimination, done with a function REPLACE-WITH-CONSTANTS-IN-DEFN.(Who cares, you may ask, what the function is called? You probably only care if you have set *INSTRUMENT-FLG* to T; see Section 8.) Now we cannot prove that this optimization is sound in general(in fact we doubt that it is, but have yet to produce an example) except under the condition that the DEFN in question has already been accepted. However, this optimization can be a useful one (an example will follow below), so the default is that this optimization is always attempted. If some simplification does indeed occur, then the definition is undone (automatically by the system), the simplified definition is simplified a final time, and finally the new definition is submitted. Here is a simple example. The function REV-LINEAR1 is one that is presumably used only for its side-effect to the special variable ANS (which has presumably been PROCLAIMed special already by a previous PROCLAIM-RCL event). The idea is that the system can deduce that the value of this function is always NIL. >(DEFUN-RCL REV-LINEAR1 (X) (IF (CONSP X) (PROGN (SETQ ANS (CONS (CAR X) ANS)) (REV-LINEAR1 (CDR X))) NIL)) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-REV-LINEAR1 (.RCL-FLG X ANS) (CASE .RCL-FLG (*1*TRUE (IF (LISTP X) (*CL-REV-LINEAR1 T (CDR X) (CONS (CAR X) ANS)) NIL)) (ANS (IF (LISTP X) (*CL-REV-LINEAR1 'ANS (CDR X) (CONS (CAR X) ANS)) ANS)) (OTHERWISE F))) Linear arithmetic and the lemma CDR-LESSP can be used to establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-REV-LINEAR1 is accepted under the definitional principle. Observe that: (OR (OR (FALSEP (*CL-REV-LINEAR1 .RCL-FLG X ANS)) (LITATOM (*CL-REV-LINEAR1 .RCL-FLG X ANS)) (LISTP (*CL-REV-LINEAR1 .RCL-FLG X ANS))) (EQUAL (*CL-REV-LINEAR1 .RCL-FLG X ANS) ANS)) is a theorem. [ 0.2 0.2 0.1 ] [[[[[ Replacing definition of *CL-REV-LINEAR1 with a simpler one: ]]]]] (DEFN *CL-REV-LINEAR1 (.RCL-FLG X ANS) (CASE .RCL-FLG (*1*TRUE NIL) (ANS (IF (LISTP X) (*CL-REV-LINEAR1 'ANS (CDR X) (CONS (CAR X) ANS)) ANS)) (OTHERWISE F))) Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-REV-LINEAR1 is accepted under the principle of definition. Note that: (OR (OR (FALSEP (*CL-REV-LINEAR1 .RCL-FLG X ANS)) (LITATOM (*CL-REV-LINEAR1 .RCL-FLG X ANS)) (LISTP (*CL-REV-LINEAR1 .RCL-FLG X ANS))) (EQUAL (*CL-REV-LINEAR1 .RCL-FLG X ANS) ANS)) is a theorem. [ 0.1 0.1 0.1 ] *CL-REV-LINEAR1 T As we already mentioned above, the default is that this feature is on, and (PROCLAIM-RCL '(POSTPROCESS-DEFNS NIL)) turns it off. This feature can then be turned back on again with (PROCLAIM-RCL '(POSTPROCESS-DEFNS T)). There are actually two other legal settings that we expect to be used only rarely. (PROCLAIM-RCL '(POSTPROCESS-DEFNS COMPLETE)) instructs the system to attempt to simplify every definition(using essentially the simplifier of PC-NQTHM, [6]), whether or not the simplification done by REPLACE-WITH-CONSTANTS-IN-DEFN does anything. We would expect that this kind of simplification is rarely going to do any good by itself (in fact, see the example at the end of this subsection), but we allow this COMPLETE setting anyhow in case someone finds a use for it. The final legal setting is CONSTANTS, i.e. the event form (PROCLAIM-RCL '(POSTPROCESS-DEFNS CONSTANTS)) is allowed. This is just like the setting of T, except that no further simplification is attempted after the recursion elimination. The only use we expect for this setting is when a user dislikes the forms produced by that further simplification but still wants the recursion elimination provided by REPLACE-WITH-CONSTANTS-IN-DEFN. As with all PROCLAIM events, an optional second argument names the event. The default event name is POSTPROCESS-, where is NIL, T, COMPLETE, or CONSTANTS according to which of these is supplied in the PROCLAIM-RCL event form. If such a name is not new, then a numeral is suffixed. Finally, here is an example showing how simplification can do more harm than good, at least aesthetically. >(defun-rcl bad (x) (if (equal x 3) (throw 'foo 7) nil)) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-BAD (.RCL-FLG X) (CASE .RCL-FLG (*1*TRUE (IF (EQUAL X 3) 7 NIL)) (*1*FALSE (IF (EQUAL X 3) '(THROW FOO) F)) (OTHERWISE F))) Observe that: (OR (FALSEP (*CL-BAD .RCL-FLG X)) (NUMBERP (*CL-BAD .RCL-FLG X)) (LITATOM (*CL-BAD .RCL-FLG X)) (LISTP (*CL-BAD .RCL-FLG X))) is a theorem. [ 0.2 0.0 0.0 ] [[[[[ Replacing definition of *CL-BAD with a simpler one: ]]]]] (DEFN *CL-BAD (.RCL-FLG X) (COND ((EQUAL .RCL-FLG T) (IF (EQUAL X 3) 7 NIL)) (.RCL-FLG F) ((EQUAL X 3) '(THROW FOO)) (T F))) Observe that: (OR (FALSEP (*CL-BAD .RCL-FLG X)) (NUMBERP (*CL-BAD .RCL-FLG X)) (LITATOM (*CL-BAD .RCL-FLG X)) (LISTP (*CL-BAD .RCL-FLG X))) is a theorem. [ 0.1 0.0 0.1 ] *CL-BAD T Another example of definition postprocessing may be found in Subsection 7.4. 7. DECLARE Recall from Section 2 that an optional DECLARE form is allowed immediately after the formal parameters of a definition and before its body. In this section we describe the shapes that the DECLARE forms may take as well as the effects that they have. The general syntax is: (declare (kind (event ...) (event ...)) 1 1,1 1,k 1 ... (kind (event ...) (event ...))) n n,1 n,k n Each kind must be distinct from the others and must be one of i HINTS, FUNCTIONS, EVENTS, or POSTPROCESS(i.e. one of those in the Lisp variable *DECLARATIONS-LIST*). Events within the scope of the same kind should be distinct, i.e. if j N j then event 1 2 i,j 1 N event , or else an error is caused. Each event is i,j i,j 2 intended to be the name of an event that is run in the course of carrying out the DEFUN-RCL, DEFMACRO-RCL, or DO-RCL in question; a warning is issued when this is not the case. Such DECLARE forms are also allowed when the definitions are inside DO-RCL; in that case, they are merged together and used together for each definition in that DO-RCL form. The merged DECLARE form is obtained by appending all declarations of each kind into a single declaration of that kind. The restrictions and warnings discussed in the previous paragraph then apply to this single merged declaration. Here is an example with some comments. It provides a pretty thorough summary, but we give more details on each kind of declaration in the subsections that follow. >(defun-rcl fff (x) (declare ;; Create a sub-function *CL-FFF<> for the value from a call of FFF and ;; a sub-function *CL-FFF for the value of ANS after that call (functions (*cl-fff t ans)) ;; Prove the silly lemma SAMPLE just after running the event *CL-FFF (events (*cl-fff (prove-lemma sample nil (equal x x)))) ;; Append the hints-list (((LESSP (LENGTH X)))) to the back of the event *CL-FFF<> ;; and append the hints-list (((LESSP (COUNT ANS)))) to the back of the event *CL-FFF (hints (*cl-fff<> ((lessp (length x)))) (*cl-fff ((lessp (count x)))))) ;; end of declarations (cond ((consp x) (setq xxx (1- xxx)) (setq ans (1+ ans)) (fff (cdr x))) (t x))) Used the following non-boot-strap lemmas and functions in the simplification process: *CL-COND. ;; The following is created because of the presence of T in the hint (functions (*cl-fff t ans)), ;; and the hint ((LESSP (LENGTH X))) is a result of the HINTS declaration. ;; This function represents the value returned by a call of FFF. (DEFN *CL-FFF<> (X) (IF (LISTP X) (*CL-FFF<> (CDR X)) X) ((LESSP (LENGTH X)))) Linear arithmetic, the lemmas EQUAL-LENGTH-0 and SUB1-ADD1, and the definitions of LESSP and LENGTH can be used to establish that the measure (LENGTH X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-FFF<> is accepted under the principle of definition. [ 0.1 0.5 0.0 ] *CL-FFF<> ;; The following is created because of the presence of ANS in the hint ;; (functions (*cl-fff t ans)), and the hint ((LESSP (COUNT X))) ;; is a result of the HINTS declaration. ;; This function represents the value of the special variable ANS after a call of FFF. (DEFN *CL-FFF (X ANS) (IF (LISTP X) (*CL-FFF (CDR X) (IPLUS ANS 1)) ANS) ((LESSP (COUNT X)))) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-FFF is accepted under the principle of definition. Note that: (OR (OR (NUMBERP (*CL-FFF X ANS)) (NEGATIVEP (*CL-FFF X ANS))) (EQUAL (*CL-FFF X ANS) ANS)) is a theorem. [ 4.3 0.1 0.1 ] *CL-FFF (DEFN *CL-FFF (.RCL-FLG X ANS XXX) (CASE .RCL-FLG (*1*TRUE (*CL-FFF<> X)) ;; Notice that CL-FFF was not created since XXX was not specified ;; in the FUNCTIONS declaration. (XXX (IF (LISTP X) (*CL-FFF 'XXX (CDR X) (IPLUS ANS 1) (IDIFFERENCE XXX 1)) XXX)) (ANS (*CL-FFF X ANS)) (OTHERWISE F))) Linear arithmetic and the lemma CDR-LESSP can be used to establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-FFF is accepted under the definitional principle. [ 0.2 0.1 0.1 ] *CL-FFF ;; The following event was created just after *CL-FFF because of the events declaration. (PROVE-LEMMA SAMPLE NIL (EQUAL X X)) This formula simplifies, obviously, to: T. Q.E.D. [ 0.0 0.1 0.0 ] SAMPLE ;; The final two lemmas were created because we had the default setting for auxiliary ;; lemmas not being inhibited. (PROVE-LEMMA *CL-FFF<>-REWRITE (REWRITE) (EQUAL (*CL-FFF T X ANS XXX) (*CL-FFF<> X))) This formula simplifies, opening up the definitions of EQUAL and *CL-FFF, to: T. Q.E.D. [ 0.0 0.1 0.0 ] *CL-FFF<>-REWRITE (PROVE-LEMMA *CL-FFF-REWRITE (REWRITE) (EQUAL (*CL-FFF 'ANS X ANS XXX) (*CL-FFF X ANS))) This conjecture simplifies, expanding EQUAL and *CL-FFF, to: T. Q.E.D. [ 0.0 0.2 0.0 ] *CL-FFF-REWRITE T > It is important to note that in the absence of DECLARE forms, the global state, as set by PROCLAIM-RCL and reported by RCL-STATUS (see Subsection 8.5), is used. So for example, if there had been no FUNCTIONS declaration, the same results as above would be obtained if the defaults were modified by (PROCLAIM-RCL (FORCE-AUXILIARY-FUNCTIONS T)), except that a function *CL-FFF would also have been created, together with a corresponding rewrite rule. 7.1 HINTS declarations The example above showed a sample HINTS declaration: (hints (*cl-fff<> ((lessp (length x)))) (*cl-fff ((lessp (count x))))) As this example suggests, the syntax for HINTS declarations is (HINTS (event hints hints ...) 1 1,1 1,2 ... (event hints hints ...)) n n,1 n,2 Each hints is appended to the end of the event named event i,j i before that event is run. Typically there is only one hint per event, and one can think of the hint as the optional ``hints'' argument to the event. 7.2 FUNCTIONS declarations The syntax for this form of declaration is (FUNCTIONS (f x ... x ) 1 1,1 1,n 1 ... (f x ... x ))) k k,1 k,n k where each f is a distinct name of an NQTHM function that one i expects to be created by the DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form that is being processed. The distinctness requirement is enforced, but if the only ``error'' is that function names are given that turn out not to name functions that become defined, then the execution proceeds happily and only a warning (not an error) is issued. In the presence of such a declaration in a DEFUN-RCL or DEFMACRO-RCL form, the global situation for FORCE-AUXILIARY- FUNCTIONS (see Subsection 6.2) for the function in question is ignored. Such a declaration instructs the system that for each of the functions f , auxiliary functions will be created i according to the following rules. If x is T, then f <> will i,j i be created to represent the value of f , in the sense described i in Section 6 above. If x is F then f <>signal will be created i,j i to represent the signal of f , also in the sense described in i Section 6 above, while if x is a special variable or state i,j variable v then f will similarly be created to represent the i value of v after a call of f . Note however that just as with i the proclamation (FORCE-AUXILIARY-FUNCTIONS T), an auxiliary function for the signal, for a special variable, or for a state variable will only be created when it ``makes sense'' to do so. For the signal, this means that if the system can see that the signal is always F then it will not bother to create such a function. For a special variable or state variable, the system will not bother to create such a function when it can deduce that a call of the function does not alter the value of that variable. For example, the declaration (declare (functions (*cl-sweep1 ans))) instructs the system that regardless of the global state, the system should create a sub-function *CL-SWEEP1 of *CL-SWEEP1 if it cannot determine that ANS is unchanged by every call of SWEEP1; and, it should not create any other sub-functions auxiliary to SWEEP1. More generally, x is also allowed instead to be a pair (v i,j name), where v is as above (i.e. something that we have already allowed to be x ) and name is the name that we wish to give the i,j auxiliary function (which should be a new name). So for example, the declaration (declare (functions (*cl-sweep1 t (ans foo)))) would result in a the creations of functions just as in the SWEEP1 example above, except that the sub-function corresponding to ANS would be called FOO instead of *CL-SWEEP1. 7.3 EVENTS declarations The syntax for EVENTS declarations is (EVENTS (event x ... x ) 1 1,1 1,n 1 ... (event x ... x )) k k,1 k,n k where each x is an event of type PROVE-LEMMA, DEFN, ADD-AXIOM, i,j CONSTRAIN, DCL, FUNCTIONALLY-INSTANTIATE, PROCLAIM-RCL, ENABLE, DISABLE, or TOGGLE(Implementation note: the list of event types is stored in the Lisp variable *ALL-EVENT-TYPES*.). In the presence of such a hint, it is the case that immediately after completion of event (where 1 L i L k), the events in the list i (x ... x ) are run in sequence. i,1 i,n i 7.4 POSTPROCESS declarations The syntax for POSTPROCESS declarations is (postprocess (f status ) 1 1 ... (f status )) k k where each status is T, NIL, COMPLETE, or CONSTANTS. Such a i declaration has the effect that for each name f that is the name i of a DEFN event, definition postprocessing will have status status for that definition, in the sense of Subsection 6.4. i Here is an example. Because of the postprocess declaration below, the body of the auxiliary function *CL-BBB<> is simplified to a constant but the auxiliary function *CL-BBB is not, even though it could be. >(defun-rcl bbb (x) (declare (functions (*cl-bbb t ans)) (postprocess (*cl-bbb<> t) (*cl-bbb nil))) (if (consp x) (bbb (cdr x)) (progn (setq ans 3) 4))) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-BBB<> (X) (IF (LISTP X) (*CL-BBB<> (CDR X)) 4)) Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-BBB<> is accepted under the definitional principle. Note that (NUMBERP (*CL-BBB<> X)) is a theorem. [ 0.1 0.1 0.1 ] [[[[[ Replacing definition of *CL-BBB<> with a simpler one: ]]]]] (DEFN *CL-BBB<> (X) 4) WARNING: X is in the arglist but not in the body of the definition of *CL-BBB<>. Observe that (NUMBERP (*CL-BBB<> X)) is a theorem. [ 0.1 0.0 0.0 ] *CL-BBB<> (DEFN *CL-BBB (X) (IF (LISTP X) (*CL-BBB (CDR X)) 3)) Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-BBB is accepted under the definitional principle. Note that (NUMBERP (*CL-BBB X)) is a theorem. [ 0.1 0.1 0.1 ] *CL-BBB (DEFN *CL-BBB (.RCL-FLG X ANS) (CASE .RCL-FLG (*1*TRUE (*CL-BBB<> X)) (ANS (*CL-BBB X)) (OTHERWISE F))) WARNING: ANS is in the arglist but not in the body of the definition of *CL-BBB. From the definition we can conclude that: (OR (FALSEP (*CL-BBB .RCL-FLG X ANS)) (NUMBERP (*CL-BBB .RCL-FLG X ANS))) is a theorem. [ 0.1 0.0 0.1 ] *CL-BBB 8. GLOBAL SWITCHES AND UTILITIES Recall that the global state may be examined by submitting the command (RCL-STATUS), which reports the settings induced by PROCLAIM-RCL events (cf. Section 6) as well as the settings of certain user-settable Lisp variables. Those variables -- *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG*, *PRINT-SIMPLIFICATION- INFO-FLG*, and *INSTRUMENT-FLG* -- are described in this section. The settings of these variables have no effect on the database; in particular, they have no effect on the libraries created by a PROVEALL. This is why we have chosen not to implement these switches using the PROCLAIM-RCL mechanism. Nevertheless, they can be helpful to the user while he is interacting with the system. The utilities UBT-RCL and RCL-STATUS are also described in this section. 8.1 The switch *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* Default: T The default setting ensures that the system automatically unwinds the database state when an error occurs in the middle of a DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form. That is, if such a form does not run to completion successfully (this includes the possibility that there is some event created by the form that fails), then all events that have been created by this form are undone so that the database (as reflected by the Lisp variable CHRONOLOGY) is the same as the database in place at the time the form was submitted. If one wishes to leave the events in place up to the failed event, one may (SETQ *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* NIL). This feature can be useful if, for example, a DEFN fails to be accepted and one wants to explore the problem in the context of the auxiliary functions that were accepted before the problem function. 8.2 The switch *PRINT-SIMPLIFICATION-INFO-FLG* Default: T This flag is the cause of the simplification message printed just before the printing of each DEFN event that arises from an RCL definition. That message is suppressed when *PRINT- SIMPLIFICATION-INFO-FLG* is NIL. However, when this flag is not NIL, the system tells the user which lemmas may have been used in the simplification process(Using the PC-NQTHM rewriter). In general, lemmas that are part of the ``boot-strap''(to be precise, that are defined in the Lisp global variable BOOT-STRAP-INSTRS, which is modified from NQTHM by the RCL source file boot.lisp) are not mentioned here; however, in the special case where *PRINT-SIMPLIFICATION-INFO-FLG* is BOOT, the system prints these out as well. Here is an example. >*print-simplification-info-flg* T >(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil)) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-FOO (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) 3) NIL) F)) Observe that: (OR (FALSEP (*CL-FOO .RCL-FLG X)) (LITATOM (*CL-FOO .RCL-FLG X)) (LISTP (*CL-FOO .RCL-FLG X))) is a theorem. [ 0.2 0.0 0.0 ] *CL-FOO T >(ubt) *CL-FOO >(setq *print-simplification-info-flg* nil) NIL >(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil)) (DEFN *CL-FOO (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) 3) NIL) F)) Observe that: (OR (FALSEP (*CL-FOO .RCL-FLG X)) (LITATOM (*CL-FOO .RCL-FLG X)) (LISTP (*CL-FOO .RCL-FLG X))) is a theorem. [ 0.1 0.0 0.1 ] *CL-FOO T >(ubt) *CL-FOO >(setq *print-simplification-info-flg* 'boot) BOOT >(defun-rcl foo (x) (if (consp x) (cons (car x) 3) nil)) Used the following lemmas and functions in the simplification process: *CL-CONS<>-REWRITE, NOT, *CL-CAR<>-IS-CAR, NON-NILP-*CL-CONSP<>, and NON-NILP-EXPANDER. (DEFN *CL-FOO (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (IF (LISTP X) (CONS (CAR X) 3) NIL) F)) Observe that: (OR (FALSEP (*CL-FOO .RCL-FLG X)) (LITATOM (*CL-FOO .RCL-FLG X)) (LISTP (*CL-FOO .RCL-FLG X))) is a theorem. [ 0.1 0.0 0.0 ] *CL-FOO T > 8.3 The switch *INSTRUMENT-FLG* Default: NIL When *INSTRUMENT-FLG* is non-NIL, information is printed to the screen whenever any of the simplification routines discussed in Section 9 have an effect. The messages are perhaps a bit obscure, but we expect them to be of interest mainly to people who are already quite familiar with these routines, say by having read [3]. If output is being directed to a file by PROVEALL, then this information is written to the file with extension ``.err''. In the special case that *INSTRUMENT-FLG* is FILE-ONLY, this information will only be printed when during a PROVEALL.(More precisely, it will only be printed when ERR-FILE is not NIL.) Finally, *INSTRUMENT-FLG* is also allowed to be a list of zero or more of the six routines discussed in Section 9: ELIMINATE- EXCESS-VARIABLES-SET, DROP-EXCESS-FORMALS, OPEN-FORWARD- REFERENCES, RCL-TRIM-DEFNS-WITH-RESTRICTIONS, ELIMINATE- SUPERFLUOUS-PARAMETERS, and REPLACE-WITH-CONSTANTS-IN-DEFN. 8.4 The utility UBT-RCL Before explaining this utility in detail, let us explain simply what we expect to be the most common usage: (UBT-RCL T) instructs the system to undo at least one event, back through the start of the most recent event sequence created by DEFUN-RCL, DEFMACRO-RCL, or DO-RCL. In fact, (UBT-RCL T) is an anomalous case, being equivalent to (UBT-RCL 0 T). Other than this anomalous case, the general syntax for UBT-RCL is as follows: details are given below. (UBT-RCL &OPTIONAL n flag) where n is a non-negative integer or an event name (just as for the nqthm utility UBT) and a non-NIL flag argument means, roughly, ``undo further if necessary back to the start of a DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form.'' Here is a more careful description. Recall that the NQTHM utility UBT takes an optional argument (default: 0) and pops that many events off the (history) chronology if the argument is a positive integer, and otherwise, assuming that the argument is the name of an event, undoes all events up to and including the given named event. UBT-RCL is similar, but is intended to make it possible to consider all events caused by a single DEFUN-RCL, DEFMACRO-RCL, or DO-RCL as a single event for the purpose of undoing. In fact it works exactly as does UBT, with the following additional action. If the earliest event undone is the corresponding NQTHM function for some Lisp function defined by the user with DEFUN-RCL or DEFMACRO-RCL (possibly inside DO-RCL), or if the optional second argument is supplied (and is not NIL), then the system undoes events back up to (and not including) the most recent ``starting point''. By a ``starting point'' we mean an event immediately before a sequence of one or more events arising from a DEFUN-RCL, DEFMACRO-RCL, or DO-RCL form. 8.5 The utility RCL-STATUS The command RCL-STATUS (actually, a Lisp function of no arguments) is rather self-explanatory. Here is an example. >(rcl-status) List of current RCL special variables: (*TEMP* *UVW*) ... Current value of *UNWIND-PROTECT-IN-RUN-RCL-EVENTS-FLG* is NIL. ... Current value of *PRINT-SIMPLIFICATION-INFO-FLG* is T. ... Current value of *INSTRUMENT-FLG* is T. ... Definition postprocessing status: T. ... Auxiliary functions forced? NO. ... Auxiliary lemmas inhibited? NO. NIL > 9. THE ALGORITHM This final section gives an informal introduction to our translation algorithm, especially to the various optimizations/simplifications that are performed. A rigorous account will appear in [3]. 9.1 Creating the initial DEFNs The basic algorithm, loosely stated, is a symbolic execution of code. That is, the body of a Lisp definition is traversed, and as this takes place, the resulting Lisp state is maintained at every point of the execution. Let us call these representations of Lisp state RCL-state data structures. Each RCL-state structure has four components(actually 5, but the fifth one is for the code itself, and we choose not to explain that here). One component is the ``binding stack'', which associates values with variables (both lexical and special). One component is for the ``state variables''; currently the only state variable is .PLISTS, which represents the property lists as an association list associating symbols with lists of pairs of the form (CONS property value). One component represents the ``signal'', which is normally F (false), representing absence of a condition, but which becomes ('THROW ) when a THROW form is encountered whose first argument evaluates to , and rather similarly for RETURN-FROM, GO, and ERR, which is an RCL approximation to the Common Lisp function ERROR (see the next subsection). The final component is for the value of the form. The values of each variable in the binding stack, as well as .PLISTS, the signal, and the value, are all terms in the NQTHM logic. The initial assumption is that no function depends on or sets the (global) value of any special variable (or .PLISTS), nor does any function cause any signal other than F. After the function (or functions, if one has multiple definitions, as is generally the case with DO-RCL) is thus processed, an account is taken of which additional variables might be read or set after all, and the process is repeated. Each time the process is repeated, any new variables that are discovered to be potentially set or read are thus noted, and variables already noted as set or read are never un-noted, so since these variable sets are finite, the monotone nature of this procedure guarantees termination. The result of this stage is essentially an association of NQTHM function names with their formals (including .RCL-FLG and perhaps extra formals from special and state variables) and RCL-state data structures.(Implementation note: this stage is represented by the Lisp function DEFUN-RCL=RESULT-LIST.) There can actually be quite a bit of simplification done even at this initial stage, since the PC-NQTHM simplifier is used throughout this stage. Consider the following example from Section 2. (The definition of the RCL function TEST had already been processed at that point.) >(defun-rcl newtest (x) (let ((*uvw* *uvw*)) (setq *temp* nil) (test (cons x x)))) Used no non-boot-strap lemmas or functions in the simplification process. (DEFN *CL-NEWTEST (.RCL-FLG X *UVW*) (CASE .RCL-FLG (*1*TRUE (*CL-TEST T (CONS X X) *UVW*)) (*1*FALSE (*CL-TEST F (CONS X X) *UVW*)) (*TEMP* NIL) (OTHERWISE F))) [ 0.2 0.0 0.0 ] *CL-NEWTEST T > Suppose that we wanted the value of the signal to be printed out explicitly, rather than by way of reference to *CL-TEST. Then one could prove the following rewrite rule before submitting the (DEFUN-RCL NEWTEST ...) form. (prove-lemma *cl-test-f-rewrite (rewrite) (equal (*cl-test f x *uvw*) (if (listp x) f '(throw badtest)))) The DEFN event below differs from the one above in that it has used the above rewrite rule to replace the *1*FALSE branch of the CASE with (IF (LISTP (CONS X X)) F '(THROW BADTEST)), which in turn simplifies to F. In fact, no explicit case for the signal is even constructed at all in the DEFN event below, and in fact the ERROR-SIGNALS property of *CL-NEWTEST is NIL. >(defun-rcl newtest (x) (let ((*uvw* *uvw*)) (setq *temp* nil) (test (cons x x)))) Used the following non-boot-strap lemmas and functions in the simplification process: *CL-TEST-F-REWRITE. (DEFN *CL-NEWTEST (.RCL-FLG X *UVW*) (CASE .RCL-FLG (*1*TRUE (*CL-TEST T (CONS X X) *UVW*)) (*TEMP* NIL) (OTHERWISE F))) [ 0.2 0.0 0.0 ] *CL-NEWTEST T > Obviously this example is contrived, but it does serve to illustrate two points. First, rewrite rules are used in the translation of RCL definitions. Second, functions are not automatically expanded in the simplification process; the call of (*CL-TEST F X *UVW*) in the *1*FALSE case above did not open up until we proved a rewrite rule to tell it to do so. One final rather subtle fact: such rules generally need to be proved ahead of time, i.e. they cannot be done by way of EVENTS declarations (cf. Subsection 7.3). This is because simplification with rewrite rules is only done before the processing of any events is begun. (There is one unusual exception, namely, simplification with rewrite rules may be done by definition postprocessing, cf. Subsections 6.4 and 7.4. But this is rather rare.) 9.2 Errors: The ERR function Before we go on to describe the next step in the translation algorithm, let us discuss one useful subtlety in our notion of signal. Recall that we are only claiming a partial correctness semantics, in the sense that functions defined by DEFUN-RCL are represented by NQTHM functions that correspond only on those inputs, and for those Lisp states, where evaluation terminates and in fact terminates in other than an error. For the purposes of this notion, ``error'' includes only those Lisp states where the signal is (ERROR). This semantics turns out to be quite convenient, as illustrated by the example in the appendix. Roughly speaking, for any call of a Lisp function that is not among the ones currently being translated to NQTHM, we ``cheat'' by assuming that that call cannot cause signal of (ERROR), and we have heuristics to take advantage of that assumption. For any call of a Lisp function that is among the ones currently being translated to NQTHM, no such special treatment is afforded. Hence, one may use the RCL function ERR to sometimes signal an error so that the current function can be accepted, and yet not pay the price of a case split on the error signal when later functions call this one. Here is a rather involved, but very illustrative example, of this treatment of ERR. Here we use ERR indirectly by way of the macro ASSERT, which is included in the startup library: (defmacro-rcl assert (form) `(or ,form (err '(assertion failed for ,form)))) For readers not comfortable with backquote, here is the same definition expressed without backquote. (defmacro-rcl assert (form) (list 'or form (list 'err (list 'quote (list 'assertion 'failed 'for form))))) Here then is a transcript of a successful PROVEALL which runs directly on top of the startup library and illustrates the use of ASSERT (in the (DEFUN-RCL FACT ...) form below). ^L (ENABLE IPLUS-NUMBERP) [ 0.0 0.0 0.0 ] IPLUS-NUMBERP-ON ^L (ENABLE IDIFFERENCE-NUMBERP) [ 0.0 0.0 0.0 ] IDIFFERENCE-NUMBERP-ON ^L (ENABLE IQUOTIENT-NUMBERP) [ 0.0 0.0 0.0 ] IQUOTIENT-NUMBERP-ON ^L (ENABLE ILESSP-NUMBERP) [ 0.0 0.0 0.0 ] ILESSP-NUMBERP-ON ^L (ENABLE IZEROP-NUMBERP) [ 0.0 0.0 0.0 ] IZEROP-NUMBERP-ON ^L (ENABLE NUMBERP-IS-INTEGERP) [ 0.0 0.0 0.0 ] NUMBERP-IS-INTEGERP-ON ^L (PROVE-LEMMA LESSP-0-NUMBERP (REWRITE) (IMPLIES (LESSP 0 X) (NUMBERP X))) WARNING: LESSP-0-NUMBERP will slow down the theorem-prover because it will cause backward chaining on every instance of a primitive type expression. This simplifies, unfolding LESSP, to: T. Q.E.D. [ 0.1 0.0 0.0 ] LESSP-0-NUMBERP ^L (PROVE-LEMMA ILESSP-0-LESSP (REWRITE) (IMPLIES (NUMBERP X) (EQUAL (ILESSP X Y) (LESSP X Y))) ((ENABLE ILESSP))) <<<..... short proof omitted .....>>> Q.E.D. [ 0.1 0.7 0.0 ] ILESSP-0-LESSP ^L (DEFUN-RCL FACT (N) (PROG ((ACC 1)) LOOP (ASSERT (AND (< 0 ACC) (< 0 N))) (WHEN (EQUAL N 1) (RETURN ACC)) (SETQ ACC (* N ACC)) (SETQ N (1- N)) (GO LOOP))) Used the following non-boot-strap lemmas and functions in the simplification process: NUMBERP-IS-INTEGERP, ITIMES-NUMBERP, LESSP-0-NUMBERP, *CL-RETURN, *CL-WHEN, ILESSP-0-LESSP, NON-NILP-*CL-<<>, *CL-AND, *CL-OR, *CL-ASSERT, and *CL-PROG. (DEFN *CL-FACT-TAGBODY-0 (.RCL-FLG ACC N) (COND ((EQUAL .RCL-FLG T) (IF (LESSP 0 ACC) (IF (LESSP 0 N) (IF (EQUAL N 1) ACC (*CL-FACT-TAGBODY-0 T (TIMES N ACC) (IDIFFERENCE N 1))) '(ASSERTION FAILED FOR (AND (< 0 ACC) (< 0 N)))) '(ASSERTION FAILED FOR (AND (< 0 ACC) (< 0 N))))) ((LESSP 0 ACC) (IF (LESSP 0 N) (IF (EQUAL N 1) '(RETURN-FROM NIL) (*CL-FACT-TAGBODY-0 F (TIMES N ACC) (IDIFFERENCE N 1))) '(ERROR))) (T '(ERROR)))) Linear arithmetic, the lemmas COUNT-NUMBERP, IDIFFERENCE-NUMBERP, and DIFFERENCE-ADD1-ARG2, and the definitions of DIFFERENCE, LESSP, and EQUAL establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-FACT-TAGBODY-0 is accepted under the definitional principle. Observe that: (OR (OR (NUMBERP (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N)) (LISTP (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N))) (EQUAL (*CL-FACT-TAGBODY-0 .RCL-FLG ACC N) ACC)) is a theorem. [ 0.4 3.2 0.1 ] *CL-FACT-TAGBODY-0 (DEFN *CL-FACT (.RCL-FLG N) (CASE .RCL-FLG (*1*TRUE (*CL-FACT-TAGBODY-0 T 1 N)) (*1*FALSE (IF (EQUAL (*CL-FACT-TAGBODY-0 F 1 N) '(RETURN-FROM NIL)) F (*CL-FACT-TAGBODY-0 F 1 N))) (OTHERWISE F))) Note that: (OR (FALSEP (*CL-FACT .RCL-FLG N)) (NUMBERP (*CL-FACT .RCL-FLG N)) (LISTP (*CL-FACT .RCL-FLG N))) is a theorem. [ 0.2 0.0 0.0 ] *CL-FACT T ^L (DEFN FACTORIAL (N) (IF (ZEROP N) 1 (TIMES N (FACTORIAL (SUB1 N))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, FACTORIAL is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (FACTORIAL N)) is a theorem. [ 0.1 0.8 0.1 ] FACTORIAL ^L (PROVE-LEMMA FACT-FACTORIAL (REWRITE) (IMPLIES (AND (NOT (ZEROP N)) (NOT (ZEROP ACC))) (EQUAL (*CL-FACT-TAGBODY-0 T ACC N) (TIMES ACC (FACTORIAL N))))) <<<..... proof omitted .....>>> Q.E.D. [ 0.1 20.8 0.6 ] FACT-FACTORIAL ^L (PROVE-LEMMA FACT-FACTORIAL-MAIN (REWRITE) (IMPLIES (NOT (ZEROP N)) (EQUAL (*CL-FACT T N) (FACTORIAL N)))) WARNING: Note that the rewrite rule FACT-FACTORIAL-MAIN will be stored so as to apply only to terms with the nonrecursive function symbol *CL-FACT. <<<..... short proof omitted .....>>> Q.E.D. [ 0.1 1.3 0.0 ] FACT-FACTORIAL-MAIN 9.3 Simplification of RCL state data structures At this stage we take the association of names to RCL-state structures and repeatedly perform three kinds of optimizations, in sequence, until there is no further change.(Implementation note: the iterative repeating of these three optimizations is performed by the Lisp function SIMPLIFY-DEFUN-RCL=RESULT-LIST.) OPEN-FORWARD-REFERENCES takes functions that were introduced for TAGBODY forms and opens up recursive calls for values of .RCL-FLG and the TAG that are ``safe''. Here we say the a pair (representing .RCL-FLG and the TAG) is safe if in the branch of the body of the function corresponding to .RCL-FLG = x and TAG = y, all the recursive calls of the function have TAG parameters that occur strictly below y in the TAGBODY code. DROP-EXCESS-FORMALS eliminates formal parameters that are no longer needed for a function because they do not appear in its associated RCL-state data structure. ELIMINATE-EXCESS-VARIABLES-SET adjusts the RCL-state data structure corresponding to a function, by noting special and state variables that are unchanged (even though the implementation conservatively ``guessed'' that they might be changed) by execution of the function. 9.4 Mutual recursion analysis Now that each function is associated with an appropriate RCL-state structure, the association of RCL-state data structures with names is used to create tentative DEFN events: the variables-read are used to extend the formal parameter lists of the original function(s); .RCL-FLG is added as a formal parameter; and the body is a CASE statement on .RCL-FLG with one case for the value, one case for the signal (if the system hasn't deduced that it's always F), and one case for each variable set. Then the mutual recursion analysis is done to create and order the dependency classes, in the sense described in Section 4.(Implementation note: the function RCL-MUTUAL-DEFNS actually performs this stage and the last, as well as the process of turning RCL-state structures into DEFN events.) 9.5 Trimming definitions Suppose now that we have a sequence of definitions, one of which corresponds to our original DEFUN-RCL or DEFMACRO-RCL form (or, more than one in the case that a DO-RCL form with more than one definition was submitted), and the rest of which we have called auxiliary. In fact, then, it should be permissible to modify the auxiliary function definitions, as long as this has no effect on the main functions. That is the idea behind what we call ``trimming definitions''(Implementation note: this stage is performed by the function RCL-TRIM-DEFNS-WITH-RESTRICTIONS.). Here is an example that illustrates this process. The point here is that the main function, *CL-REV1, only calls the function *CL-REV1-TAGBODY-0 once, with the first two arguments in that call being '*1*TRUE (i.e. T) and 'LOOP. It turns out that if we modify the definition of *CL-REV1-TAGBODY-0 to be ``restricted'' to the branch of its definition in which its first two arguments have those values, then the resulting definition is ``equivalent'' to the original, from the point of view of *CL-REV1. We have set *INSTRUMENT-FLG* to the one-element list (RCL-TRIM-DEFNS-WITH-RESTRICTIONS) (cf. preceding footnote) in order to track this optimization. Sorry about the mess: please read '*1*TRUE as T and '*1*FALSE as F. >(defun-rcl rev1 (x) (prog (acc) loop (when (not (consp x)) (return acc)) (setq acc (cons (car x) acc)) (setq x (cdr x)) (go loop))) ******************** RCL-TRIM-DEFNS-WITH-RESTRICTIONS ........................................ ((*CL-REV1-TAGBODY-0 (.RCL-FLG TAG ACC X) (IF (EQUAL .RCL-FLG '*1*TRUE) (IF (LISTP X) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC) (IF (EQUAL .RCL-FLG '*1*FALSE) (IF (LISTP X) (*CL-REV1-TAGBODY-0 '*1*FALSE 'LOOP (CONS (CAR X) ACC) (CDR X)) '(RETURN-FROM NIL)) (IF (EQUAL .RCL-FLG 'ACC) (IF (LISTP X) (*CL-REV1-TAGBODY-0 'ACC 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC) (IF (EQUAL .RCL-FLG 'X) (IF (LISTP X) (*CL-REV1-TAGBODY-0 'X 'LOOP (CONS (CAR X) ACC) (CDR X)) X) '*1*FALSE))))) (*CL-REV1 (.RCL-FLG X) (IF (EQUAL .RCL-FLG '*1*TRUE) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP 'NIL X) '*1*FALSE))) ........................................ ((*CL-REV1-TAGBODY-0 (.RCL-FLG TAG ACC X) (IF (LISTP X) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC)) (*CL-REV1 (.RCL-FLG X) (IF (EQUAL .RCL-FLG '*1*TRUE) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP 'NIL X) '*1*FALSE))) ******************** Used the following non-boot-strap lemmas and functions in the simplification process: *CL-NOT-REWRITE, *CL-NOT<>-REWRITE, *CL-RETURN, *CL-WHEN, and *CL-PROG. (DEFN *CL-REV1-TAGBODY-0 (ACC X) (IF (LISTP X) (*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC) (CDR X)) ACC)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, *CL-REV1-TAGBODY-0 is accepted under the definitional principle. From the definition we can conclude that: (OR (LISTP (*CL-REV1-TAGBODY-0 ACC X)) (EQUAL (*CL-REV1-TAGBODY-0 ACC X) ACC)) is a theorem. [ 0.1 0.1 0.1 ] *CL-REV1-TAGBODY-0 (DEFN *CL-REV1 (.RCL-FLG X) (IF (EQUAL .RCL-FLG T) (*CL-REV1-TAGBODY-0 NIL X) F)) Note that: (OR (FALSEP (*CL-REV1 .RCL-FLG X)) (LITATOM (*CL-REV1 .RCL-FLG X)) (LISTP (*CL-REV1 .RCL-FLG X))) is a theorem. [ 0.1 0.0 0.0 ] *CL-REV1 T > 9.6 Eliminating superfluous parameters The system is now ready to try once again to eliminate extra formal parameters. However, while DROP-EXCESS-FORMALS (discussed above in Subsection 9.3) is performed on RCL-state data structures, the function ELIMINATE-SUPERFLUOUS-PARAMETERS is applied to tentative DEFN events. Also, if analysis shows some formal parameters to be irrelevant to the value of the function, then at this stage we are even willing to drop .RCL-FLG and the original formal parameters of the DEFUN if they are among the superfluous formals, as long as the function in question is not one of the original functions defined by the user. So for example, if we had set *INSTRUMENT-FLG* to T, we would have seen the following additional output immediately after the output for RCL-TRIM-DEFNS-WITH-RESTRICTIONS (and before the DEFN of *CL-REV1-TAGBODY-0) in the preceding subsection's example. ******************** ELIMINATE-SUPERFLUOUS-PARAMETERS: (CALLED DROP-EXCESS-FORMALS-TERM ON CHANGED-FORMALS-ALIST OF ((*CL-REV1-TAGBODY-0 (ACC X) (.RCL-FLG TAG ACC X))) AND NAME *CL-REV1-TAGBODY-0 AND ORIGINAL FORMALS (.RCL-FLG TAG ACC X)) ........................................ ;; Previous body of *CL-REV1-TAGBODY-0 (IF (LISTP X) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP (CONS (CAR X) ACC) (CDR X)) ACC) ........................................ ;; Revised body of *CL-REV1-TAGBODY-0 (IF (LISTP X) (*CL-REV1-TAGBODY-0 (CONS (CAR X) ACC) (CDR X)) ACC) ******************** ;; The following output corresponds to the definition of *CL-REV1. ******************** ELIMINATE-SUPERFLUOUS-PARAMETERS: (CALLED DROP-EXCESS-FORMALS-TERM ON CHANGED-FORMALS-ALIST OF ((*CL-REV1-TAGBODY-0 (ACC X) (.RCL-FLG TAG ACC X))) AND NAME *CL-REV1 AND ORIGINAL FORMALS (.RCL-FLG X)) ........................................ ;; Previous body of *CL-REV1 (IF (EQUAL .RCL-FLG '*1*TRUE) (*CL-REV1-TAGBODY-0 '*1*TRUE 'LOOP 'NIL X) '*1*FALSE) ........................................ ;; Revised body of *CL-REV1 (IF (EQUAL .RCL-FLG '*1*TRUE) (*CL-REV1-TAGBODY-0 'NIL X) '*1*FALSE) ******************** 9.7 Recursion elimination The final major simplification is recursion elimination in certain circumstances. This is exactly the optimization that was called ``definition postprocessing'' in Subsections 6.4 and 7.4. As we mentioned before, unlike the other optimizations, we only trust the soundness of this one if the definition in question is already acceptable before the optimization. The rough idea is that if one has a branch of a definition such that the ``only way out'' is with a fixed constant value, then one can replace that branch by that constant.(Implementation note: this function is called REPLACE-WITH-CONSTANTS-IN-DEFN.) See Subsection 6.4 for an example. REFERENCES 1. M. Kaufmann, ``A Verification System for a Subset of Common Lisp'', Internal Note 110, Computational Logic, Inc., January 1989. 2. Guy L. Steele Jr., Common LISP: The Language, Digital Press, 1984. 3. M. Kaufmann, ``Rose Common Lisp: A Lisp Verification System'', Technical Report, Computational Logic, Inc., to appear. 4. R. S. Boyer and J S. Moore, A Computational Logic Handbook, Academic Press, Boston, 1988. 5. R. S. Boyer and J S. Moore, A Computational Logic, Academic Press, New York, 1979. 6. M. Kaufmann, ``A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover'', Technical Report 19, Computational Logic, Inc., May 1988. 7. M. Kaufmann, ``Addition of Free Variables to an Interactive Enhancement of the Boyer-Moore Theorem Prover'', Tech. report 42, Computational Logic, Inc., 1717 West Sixth Street, Suite 290 Austin, TX 78703, 1989. 8. W. Bevier, ``A Library for Hardware Verification'', Internal Note 57, Computational Logic, Inc., June 1988. 9. M. Kaufmann, ``A mutual recursion and dependency analysis tool for NQTHM'', Internal Note 99, Computational Logic, Inc., November 1988.