Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-lemacs.info, Node: PROGN, Next: PROOFS-CO, Prev: PPROGN, Up: PROGRAMMING PROGN see the documentation for er-progn ACL2 does not allow the use of progn in definitions. Instead, a function er-progn can be used for sequencing state-oriented operations; *Note ER-PROGN:: and *Note STATE::. Progn is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: PROOFS-CO, Next: PROPER-CONSP, Prev: PROGN, Up: PROGRAMMING PROOFS-CO the proofs character output channel Proofs-co is an ld special (*Note LD::). The accessor is (proofs-co state) and the updater is (set-proofs-co val state). Proofs-co must be an open character output channel. It is to this channel that defun, defthm, and the other event commands print their commentary. "Proofs-co" stands for "proofs character output." The initial value of proofs-co is the same as the value of *standard-co* (*Note *STANDARD-CO*::).  File: acl2-doc-lemacs.info, Node: PROPER-CONSP, Next: PUT-ASSOC-EQ, Prev: PROOFS-CO, Up: PROGRAMMING PROPER-CONSP recognizer for proper (null-terminated) non-empty lists Proper-consp is the function that checks whether its argument is a non-empty list that ends in nil. Also *Note TRUE-LISTP::.  File: acl2-doc-lemacs.info, Node: PUT-ASSOC-EQ, Next: PUT-ASSOC-EQUAL, Prev: PROPER-CONSP, Up: PROGRAMMING PUT-ASSOC-EQ modify an association list by associating a value with a key (Put-assoc-eq name val alist) returns an alist that is the same as the list alist, except that the first pair in alist with a car of name is replaced by (cons name val), if there is one. If there is no such pair, then (cons name val) is added at the end. The guard of (put-assoc-eq name val alist) requires that alist is an alistp, and moreover, either name is a symbol or alist is a symbol-alistp.  File: acl2-doc-lemacs.info, Node: PUT-ASSOC-EQUAL, Next: RASSOC, Prev: PUT-ASSOC-EQ, Up: PROGRAMMING PUT-ASSOC-EQUAL modify an association list by associating a value with a key (Put-assoc-equal name val alist) returns an alist that is the same as the list alist, except that the first pair in alist with a car of name is replaced by (cons name val), if there is one. If there is no such pair, then (cons name val) is added at the end. The guard of (put-assoc-equal name val alist) requires that alist is an alistp.  File: acl2-doc-lemacs.info, Node: RASSOC, Next: RATIONAL-LISTP, Prev: PUT-ASSOC-EQUAL, Up: PROGRAMMING RASSOC look up value in association list, using eql as test (Rassoc x alist) is similar to (assoc x alist), the difference being that it looks for the first pair in the given alist whose cdr, rather than car, is eql to x. *Note ASSOC::. The guard of rassoc requires its second argument to be an alist, and in addition, that either its first argument is eqlablep or else all second components of pairs belonging to the second argument are eqlablep. *Note EQLABLEP::. Rassoc is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: RATIONAL-LISTP, Next: RATIONALP, Prev: RASSOC, Up: PROGRAMMING RATIONAL-LISTP recognizer for a true list of rational numbers The predicate rational-listp tests whether its argument is a true list of rational numbers.  File: acl2-doc-lemacs.info, Node: RATIONALP, Next: REALPART, Prev: RATIONAL-LISTP, Up: PROGRAMMING RATIONALP recognizer for whole numbers (rationalp x) is true if and only if x is an rational number.  File: acl2-doc-lemacs.info, Node: REALPART, Next: REDEFINING-PROGRAMS, Prev: RATIONALP, Up: PROGRAMMING REALPART real part of a complex number Basic axiom: (equal (realpart x) (if (acl2-numberp x) (realpart x) 0)) Guard for (realpart x): (acl2-numberp x)  File: acl2-doc-lemacs.info, Node: REDEFINING-PROGRAMS, Next: REM, Prev: REALPART, Up: PROGRAMMING REDEFINING-PROGRAMS an explanation of why we restrict redefinitions ACL2 does not in general allow the redefinition of functions because logical inconsistency can result: previously stored theorems can be rendered invalid if the axioms defining the functions involved are changed. However, to permit prototyping of both :program and :logic mode systems, ACL2 permits redefinition if the user has accepted logical responsibility for the consequences by setting ld-redefinition-action to an appropriate non-nil value. The refusal of ACL2 to support the unrestricted redefinition of :program mode functions may appear somewhat capricious. After all, what are the logical consequences of changing a definition if no axioms are involved? Three important points should be made before we discuss redefinition further. The first is that ACL2 does support redefinition (of both :program and :logic functions) when ld-redefinition-action is non-nil. The second is that a "redefinition" that does not change the mode, formals or body of a function is considered redundant and is permitted even when ld-redefinition-action is nil. We recognize and permit redundant definitions because it is not uncommon for two distinct books to share identical function definitions. When determining whether the body of a function is changed by a proposed redefinition, we actually compare the untranslated versions of the two bodies. *Note TERM::. For example, redundancy is not recognized if the old body is (list a b) and the new body is (cons a (cons b nil)). We use the untranslated bodies because of the difficulty of translating the new body in the presence of the old syntactic information, given the possibility that the redefinition might attempt to change the signature of the function, i.e., the number of formals, the number of results, or the position of STATE in either. The third important point is that a "redefinition" that preserves the formals and body but changes the mode from :program to :logic is permitted even when ld-redefinition-action is nil. That is what verify-termination does. This note addresses the temptation to allow redefiniton of :program functions in situations other than the three described above. Therefore, suppose ld-redefinition-action is nil and consider the cases. Case 1. Suppose the new definition attempts to change the formals or more generally the signature of the function. Accepting such a redefinition would render ill-formed other :program functions which call the redefined function. Subsequent attempts to evaluate those callers could arbitrarily damage the Common Lisp image. Thus, redefinition of :program functions under these circumstances requires the user's active approval, as would be sought with ld-redefinition-action '(:query . :overwrite). Case 2. Suppose the new definition attempts to change the body (even though it preserves the signature). At one time we believed this was acceptable and ACL2 supported the quiet redefinition of :program mode functions in this circumstance. However, because such functions can be used in macros and redundancy checking is based on untranslated bodies, this turns out to be unsound! It is therefore now prohibited. We illustrate such an unsoundness below. Let foo-thm1.lisp be a book with the following contents. (in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm1 (iff (foo x) x) :rule-classes nil) Note that the macro form (p x) translates to (if x t nil). The :program function p1 is used to generate this translation. The function foo is defined so that (foo x) is (p x) and a theorem about foo is proved, namely, that (foo x) is true iff x is true. Now let foo-thm2.lisp be a book with the following contents. (in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil) In this book, the :program function p1 is defined so that (p x) means just the negation of what it meant in the first book, namely, (if x nil t). The function foo is defined identically --- more precisely, the untranslated body of foo is identical in the two books, but because of the difference between the two versions of the the :program function p1 the axioms defining the two foos are different. In the second book we prove the theorem that (foo x) is true iff x is nil. Now consider what would happen if the signature-preserving redefinition of :program functions were permitted and these two books were included. When the second book is included the redefinition of p1 would be permitted since the signature is preserved and p1 is just a :program. But then when the redefinition of foo is processed it would be considered redundant and thus be permitted. The result would be a logic in which it was possible to prove that (foo x) is equivalent to both x and (not x). In particular, the following sequence leads to a proof of nil: (include-book "foo-thm1") (include-book "foo-thm2") (thm nil :hints (("Goal" :use (foo-thm1 foo-thm2)))) It might be possible to loosen the restrictions on the redefinition of :program functions by allowing signature-preserving redefinition of :program functions not involved in macro definitions. Alternatively, we could implement definition redundancy checking based on the translated bodies of functions (though that is quite problematic). Barring those two changes, we believe it is necessary simply to impose the same restrictions on the redefinition of :program mode functions as we do on :logic mode functions.  File: acl2-doc-lemacs.info, Node: REM, Next: REMOVE, Prev: REDEFINING-PROGRAMS, Up: PROGRAMMING REM remainder using truncate ACL2 !>(rem 14 3) 2 ACL2 !>(rem -14 3) -2 ACL2 !>(rem 14 -3) 2 ACL2 !>(rem -14 -3) -2 ACL2 !>(rem -15 -3) 0 ACL2 !> (Rem i j) is that number k that (* j (truncate i j)) added to k equals i. The guard for (rem i j) requires that i and j are rational numbers and j is non-zero. Rem is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: REMOVE, Next: REMOVE-DUPLICATES, Prev: REM, Up: PROGRAMMING REMOVE remove all occurrences, testing using eql (remove x l) is l if x is not a member of l, else is the result of removing all occurrences of x from l. The guard for (remove x l) requires l to be a true list and moreover, either x is eqlablep or all elements of l are eqlablep. Remove is a Common Lisp function. See any Common Lisp documentation for more information. Note that we do not allow keyword arguments (such as test) in ACL2 functions, in particular, in remove.  File: acl2-doc-lemacs.info, Node: REMOVE-DUPLICATES, Next: REMOVE-DUPLICATES-EQUAL, Prev: REMOVE, Up: PROGRAMMING REMOVE-DUPLICATES remove duplicates from a string or (using eql) a list Remove-duplicates returns the result of deleting duplicate elements from the beginning of the given string or true list, i.e., leaving the last element in place. For example, (remove-duplicates '(1 2 3 2 4)) is equal to '(1 3 2 4). The guard for Remove-duplicates requires that its argument is a string or a true-list of eqlablep objects. It uses the function eql to test for equality between elements of its argument. Remove-duplicates is a Common Lisp function. See any Common Lisp documentation for more information. Note that we do not allow keyword arguments (such as test) in ACL2 functions, in particular, in remove-duplicates. But *Note REMOVE-DUPLICATES-EQUAL::, which is similar but uses the function equal to test for duplicate elements.  File: acl2-doc-lemacs.info, Node: REMOVE-DUPLICATES-EQUAL, Next: REST, Prev: REMOVE-DUPLICATES, Up: PROGRAMMING REMOVE-DUPLICATES-EQUAL remove duplicates from a list Remove-duplicates-equal is the same as remove-duplicates, except that its argument must be a true list (not a string), and equal is used to check membership rather than eql. *Note REMOVE-DUPLICATES::. The guard for Remove-duplicates-equal requires that its argument is a true list. Note that unlike remove-duplicates, it does not allow string arguments.  File: acl2-doc-lemacs.info, Node: REST, Next: REVAPPEND, Prev: REMOVE-DUPLICATES-EQUAL, Up: PROGRAMMING REST rest (cdr) of the list In the logic, rest is just a macro for cdr. Rest is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: REVAPPEND, Next: REVERSE, Prev: REST, Up: PROGRAMMING REVAPPEND concatentate the reverse of one list to another (Revappend x y) concatenates the reverse of the list x to y, which is also typically a list. The following theorem characterizes this English description. (equal (revappend x y) (append (reverse x) y)) Hint: This lemma follows immediately from the definition of reverse and the following lemma. (defthm revappend-append (equal (append (revappend x y) z) (revappend x (append y z)))) The guard for (revappend x y) requires that x is a true list. Revappend is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: REVERSE, Next: RFIX, Prev: REVAPPEND, Up: PROGRAMMING REVERSE reverse a list (Reverse x) is the result of reversing the order of the elements of the list x. The guard for reverse requires that its argument is a true list. Reverse is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: RFIX, Next: ROUND, Prev: REVERSE, Up: PROGRAMMING RFIX coerce to a rational number Rfix simply returns any rational number argument unchanged, returning 0 on a non-rational argument. Also *Note NFIX::, *Note IFIX::, and *Note FIX:: for analogous functions that coerce to a natural number, an integer, and a number, respectively. Rfix has a guard of t.  File: acl2-doc-lemacs.info, Node: ROUND, Next: SECOND, Prev: RFIX, Up: PROGRAMMING ROUND division returning an integer by rounding off Example Forms: ACL2 !>(round 14 3) 5 ACL2 !>(round -14 3) -5 ACL2 !>(round 14 -3) -5 ACL2 !>(round -14 -3) 5 ACL2 !>(round 13 3) 4 ACL2 !>(round -13 3) -4 ACL2 !>(round 13 -3) -4 ACL2 !>(round -13 -3) 4 ACL2 !>(round -15 -3) 5 ACL2 !>(round 15 -2) -8 (Round i j) is the result of taking the quotient of i and j and rounding off to the nearest integer. When the quotient is exactly halfway between consecutive integers, it rounds to the even one. The guard for (round i j) requires that i and j are rational numbers and j is non-zero. Round is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: SECOND, Next: SET-DIFFERENCE-EQUAL, Prev: ROUND, Up: PROGRAMMING SECOND second member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: SET-DIFFERENCE-EQUAL, Next: SEVENTH, Prev: SECOND, Up: PROGRAMMING SET-DIFFERENCE-EQUAL elements of one list that are not elements of another (Set-difference l1 l2) equals a list whose members (*Note MEMBER-EQUAL::) contains the members of x that are not members of y. More precisely, the resulting list is the same as one gets by deleting the members of y from x, leaving the remaining elements in the same order as they had in x. The guard for set-difference-equal requires both arguments to be true lists. Essentially, set-difference-equal has the same functionality as the Common Lisp function set-difference, except that it uses the equal function to test membership rather than eql. However, we do not include the function set-difference in ACL2, because the Common Lisp language does not specify the order of the elements in the list that it returns.  File: acl2-doc-lemacs.info, Node: SEVENTH, Next: SIGNUM, Prev: SET-DIFFERENCE-EQUAL, Up: PROGRAMMING SEVENTH seventh member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: SIGNUM, Next: SIXTH, Prev: SEVENTH, Up: PROGRAMMING SIGNUM indicator for positive, negative, or zero (Signum x) is 0 if x is 0, -1 if x is negative, and is 1 otherwise. The guard for signum requires its argument to be rational. Signum is a Common Lisp function. See any Common Lisp documentation for more information. From "Common Lisp the Language" page 206, we see a definition of signum in terms of abs. As explained elsewhere (*Note ABS::), the guard for abs requires its argument to be a rational number; hence, we make the same restriction for signum.  File: acl2-doc-lemacs.info, Node: SIXTH, Next: STANDARD-CHAR-LISTP, Prev: SIGNUM, Up: PROGRAMMING SIXTH sixth member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: STANDARD-CHAR-LISTP, Next: STANDARD-CHAR-P, Prev: SIXTH, Up: PROGRAMMING STANDARD-CHAR-LISTP recognizer for standard characters (standard-char-listp x) is true if and only if x is a null-terminated list all of whose members are standard characters. *Note STANDARD-CHAR-P::. Standard-char-listp has a guard of t.  File: acl2-doc-lemacs.info, Node: STANDARD-CHAR-P, Next: STANDARD-CO, Prev: STANDARD-CHAR-LISTP, Up: PROGRAMMING STANDARD-CHAR-P recognizer for standard characters (Standard-char-p x) is true if and only if x is a "standard" character, i.e., a member of the list *standard-chars*. This list includes #Newline and #Space characters, as well as the usual punctuation and alphanumeric characters. Standard-char-p has a guard requiring its argument to be a character. Standard-char-p is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STANDARD-CO, Next: STANDARD-OI, Prev: STANDARD-CHAR-P, Up: PROGRAMMING STANDARD-CO the character output channel to which ld prints Standard-co is an ld special (*Note LD::). The accessor is (standard-co state) and the updater is (set-standard-co val state). Standard-co must be an open character output channel. It is to this channel that ld prints the prompt, the form to be evaluated, and the results. The event commands such as defun, defthm, etc., which print extensive commentary do not print to standard-co but rather to a different channel, proofs-co, so that you may redirect this commentary while still interacting via standard-co. *Note PROOFS-CO::. "Standard-co" stands for "standard character output." The initial value of standard-co is the same as the value of *standard-co* (*Note *STANDARD-CO*::).  File: acl2-doc-lemacs.info, Node: STANDARD-OI, Next: STRING, Prev: STANDARD-CO, Up: PROGRAMMING STANDARD-OI the standard object input "channel" Standard-oi is an ld special (*Note LD::). The accessor is (standard-oi state) and the updater is (set-standard-oi val state). Standard-oi must be an open object input channel, a true list of objects, or a list of objects whose last cdr is an open object input channel. It is from this source that ld takes the input forms to process. When ld is called, if the value specified for standard-oi is a string or a list of objects whose last cdr is a string, then ld treats the string as a file name and opens an object input channel from that file. The channel opened by ld is closed by ld upon termination. "Standard-oi" stands for "standard object input." The read-eval-print loop in ld reads the objects in standard-oi and treats them as forms to be evaluated. The initial value of standard-oi is the same as the value of *standard-oi* (*Note *STANDARD-OI*::).  File: acl2-doc-lemacs.info, Node: STRING, Next: STRING-ALISTP, Prev: STANDARD-OI, Up: PROGRAMMING STRING coerce to a string (String x) coerces x to a string. If x is already a string, then it is returned unchanged; if x is a symbol, then its symbol-name is returned; and if x is a character, the corresponding one-character string is returned. The guard for string requires its argument to be a string, a symbol, or a character. String is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING-ALISTP, Next: STRING-APPEND, Prev: STRING, Up: PROGRAMMING STRING-ALISTP recognizer for association lists with strings as keys (String-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a string. String-alistp has a guard of t.  File: acl2-doc-lemacs.info, Node: STRING-APPEND, Next: STRING-DOWNCASE, Prev: STRING-ALISTP, Up: PROGRAMMING STRING-APPEND concatenate two strings NOTE: It is probably more efficient to use the Common Lisp function concatenate in place of string-append. That is, (string-append str1 str2) is equal to (concatenate 'string str1 str2). At any rate, string-append takes two arguments, which are both strings (if the guard is to be met), and returns a string obtained concatenating together the characters in the first string followed by those in the second. *Note CONCATENATE::.  File: acl2-doc-lemacs.info, Node: STRING-DOWNCASE, Next: STRING-EQUAL, Prev: STRING-APPEND, Up: PROGRAMMING STRING-DOWNCASE in a given string, turn upper-case characters into lower-case For a string x, (string-downcase x) is the result of applying char-downcase to each character in x. The guard for string-downcase requires its argument to be a string. String-downcase is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING-EQUAL, Next: STRING-LISTP, Prev: STRING-DOWNCASE, Up: PROGRAMMING STRING-EQUAL string equality without regard to case For strings str1 and str2, (string-equal str1 str2) is true if and only str1 and str2 are the same except perhaps for the cases of their characters. The guard on string-equal requires that its arguments are strings. String-equal is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING-LISTP, Next: STRING-UPCASE, Prev: STRING-EQUAL, Up: PROGRAMMING STRING-LISTP recognizer for a true list of strings The predicate string-listp tests whether its argument is a true-listp of strings.  File: acl2-doc-lemacs.info, Node: STRING-UPCASE, Next: STRING<, Prev: STRING-LISTP, Up: PROGRAMMING STRING-UPCASE in a given string, turn lower-case characters into upper-case For a string x, (string-upcase x) is the result of applying char-upcase to each character in x. The guard for string-upcase requires its argument to be a string. String-upcase is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING<, Next: STRING<=, Prev: STRING-UPCASE, Up: PROGRAMMING STRING< less-than test for strings (String< str1 str2) is non-nil if and only if the string str1 precedes the string str2 lexicographically, where character inequalities are tested using char<. When non-nil, (string< str1 str2) is the first position (zero-based) at which the strings differ. Here are some examples. ACL2 !>(string< "abcd" "abu") 2 ACL2 !>(string< "abcd" "Abu") NIL ACL2 !>(string< "abc" "abcde") 3 ACL2 !>(string< "abcde" "abc") NIL The guard for string< specifies that its arguments are strings. String< is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING<=, Next: STRING>, Prev: STRING<, Up: PROGRAMMING STRING<= less-than-or-equal test for strings (String<= str1 str2) is non-nil if and only if the string str1 precedes the string str2 lexicographically or the strings are equal. When non-nil, (string<= str1 str2) is the first position (zero-based) at which the strings differ, if they differ, and otherwise is their common length. *Note STRING<::. The guard for string<= specifies that its arguments are strings. String<= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING>, Next: STRING>=, Prev: STRING<=, Up: PROGRAMMING STRING> greater-than test for strings (String> str1 str2) is non-nil if and only if str2 precedes str1 lexicographically. When non-nil, (string> str1 str2) is the first position (zero-based) at which the strings differ. *Note STRING<::. String> is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRING>=, Next: STRINGP, Prev: STRING>, Up: PROGRAMMING STRING>= less-than-or-equal test for strings (String>= str1 str2) is non-nil if and only if the string str2 precedes the string str1 lexicographically or the strings are equal. When non-nil, (string>= str1 str2) is the first position (zero-based) at which the strings differ, if they differ, and otherwise is their common length. *Note STRING>::. The guard for string>= specifies that its arguments are strings. String>= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: STRINGP, Next: STRIP-CARS, Prev: STRING>=, Up: PROGRAMMING STRINGP recognizer for strings (stringp x) is true if and only if x is a string.  File: acl2-doc-lemacs.info, Node: STRIP-CARS, Next: STRIP-CDRS, Prev: STRINGP, Up: PROGRAMMING STRIP-CARS collect up all first components of pairs in a list (strip-cars x) is the list obtained by walking through the list x and collecting up all first components (cars). (strip-cars x) has a guard of (alistp x).  File: acl2-doc-lemacs.info, Node: STRIP-CDRS, Next: SUBLIS, Prev: STRIP-CARS, Up: PROGRAMMING STRIP-CDRS collect up all second components of pairs in a list (strip-cdrs x) has a guard of (alistp x), and returns the list obtained by walking through the list x and collecting up all second components (cdrs).  File: acl2-doc-lemacs.info, Node: SUBLIS, Next: SUBSEQ, Prev: STRIP-CDRS, Up: PROGRAMMING SUBLIS substitute an alist into a tree (Sublis alist tree) is obtained by replacing every leaf of tree with the result of looking that leaf up in the association list alist. However, a leaf is left unchanged if it is not found as a key in alist. Leaves are lookup up using the function assoc. The guard for (subsetp alist tree) requires (eqlable-alistp alist). This guard ensures that the guard for assoc will be met for each lookup generated by sublis. Sublis is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: SUBSEQ, Next: SUBSETP, Prev: SUBLIS, Up: PROGRAMMING SUBSEQ subsequence of a string or list For any natural numbers start and end, where start <= end <= (length seq), (subseq start end) is the subsequence of seq from index start up to, but not including, index end. End may be nil, which which case it is treated as though it is (length seq), i.e., we obtain the subsequence of seq from index start all the way to the end. The guard for (subseq seq start end) is that seq is a true list or a string, start and end are integers (except, end may be nil, in which case it is treated as (length seq) for ther rest of this discussion), and 0 <= start <= end <= (length seq). Subseq is a Common Lisp function. See any Common Lisp documentation for more information. Note: In Common Lisp the third argument of subseq is optional, but in ACL2 it is required, though it may be nil as explained above.  File: acl2-doc-lemacs.info, Node: SUBSETP, Next: SUBSETP-EQUAL, Prev: SUBSEQ, Up: PROGRAMMING SUBSETP test if every member of one list is a member of the other (Subsetp x y) is true if and only if every member of the list x is a member of the list y. Membership is tested using the function member. Thus, the guard for subsetp requires that its arguments are true lists, and moreover, at least one satisfies eqlable-listp. This guard ensures that the guard for member will be met for each call generated by subsetp. Subsetp is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: SUBSETP-EQUAL, Next: SUBST, Prev: SUBSETP, Up: PROGRAMMING SUBSETP-EQUAL check if all members of one list are members of the other (Subsetp-equal x y) returns t if every member of x is a member of y, where membership is tested using member-equal. The guard for subsetp-equal requires both arguments to be true lists. Subsetp-equal has the same functionality as the Common Lisp function subsetp, except that it uses the equal function to test membership rather than eql.  File: acl2-doc-lemacs.info, Node: SUBST, Next: SYMBOL-<, Prev: SUBSETP-EQUAL, Up: PROGRAMMING SUBST a single substitution into a tree (Subst new old tree) is obtained by substituting new for every occurence of old in the given tree. Equality to old is determined using the function eql. The guard for (subst new old tree) requires (eqlablep old), which ensures that the guard for eql will be met for each comparison generated by subst. Subst is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: SYMBOL-<, Next: SYMBOL-ALISTP, Prev: SUBST, Up: PROGRAMMING SYMBOL-< less-than test for symbols (symbol-< x y) is non-nil if and only if either the symbol-name of the symbol x lexicographially precedes the symbol-name of the symbol y (in the sense of string<) or else the symbol-names are equal and the symbol-package-name of x lexicographically precedes that of y (in the same sense). So for example, (symbol-< 'abcd 'abce) and (symbol-< 'acl2::abcd 'foo::abce) are true. The guard for symbol specifies that its arguments are symbols.  File: acl2-doc-lemacs.info, Node: SYMBOL-ALISTP, Next: SYMBOL-LISTP, Prev: SYMBOL-<, Up: PROGRAMMING SYMBOL-ALISTP recognizer for association lists with symbols as keys (Symbol-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a symbolp.  File: acl2-doc-lemacs.info, Node: SYMBOL-LISTP, Next: SYMBOL-NAME, Prev: SYMBOL-ALISTP, Up: PROGRAMMING SYMBOL-LISTP recognizer for a true list of symbols The predicate symbol-listp tests whether its argument is a true list of symbols.  File: acl2-doc-lemacs.info, Node: SYMBOL-NAME, Next: SYMBOL-PACKAGE-NAME, Prev: SYMBOL-LISTP, Up: PROGRAMMING SYMBOL-NAME the name of a symbol (a string) Basic axiom: (equal (symbol-name x) (if (symbolp x) (symbol-name x) "")) Guard for (symbol-name x): (symbolp x)  File: acl2-doc-lemacs.info, Node: SYMBOL-PACKAGE-NAME, Next: SYMBOLP, Prev: SYMBOL-NAME, Up: PROGRAMMING SYMBOL-PACKAGE-NAME the name of the package of a symbol (a string) Basic axiom: (equal (symbol-package-name x) (if (symbolp x) (symbol-package-name x) "")) Guard for (symbol-package-name x): (symbolp x)  File: acl2-doc-lemacs.info, Node: SYMBOLP, Next: TAKE, Prev: SYMBOL-PACKAGE-NAME, Up: PROGRAMMING SYMBOLP recognizer for symbols (symbolp x) is true if and only if x is a symbol.  File: acl2-doc-lemacs.info, Node: TAKE, Next: TENTH, Prev: SYMBOLP, Up: PROGRAMMING TAKE initial segment of a list For any natural number n not exceeding the length of l, (take n l) collects the first n elements of the list l. The following is a theorem (though it takes some effort, including lemmas, to get ACL2 to prove it): (equal (length (take n l)) (nfix n)) If n is is an integer greater than the length of l, then take pads the list with the appropriate number of nil elements. Thus, the following is also a theorem. (implies (and (integerp n) (true-listp l) (<= (length l) n)) (equal (take n l) (append l (make-list (- n (length l)))))) For related functions, *Note NTHCDR:: and *Note BUTLAST::. The guard for (take n l) is that n is a nonnegative integer and l is a true list.  File: acl2-doc-lemacs.info, Node: TENTH, Next: THE, Prev: TAKE, Up: PROGRAMMING TENTH tenth member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: THE, Next: THIRD, Prev: TENTH, Up: PROGRAMMING THE run-time type check (The typ val) checks that val satisfies the type specification typ (*Note TYPE-SPEC::). An error is caused if the check fails, and otherwise, val is the value of this expression. Here are some examples. (the integer 3) ; returns 3 (the (integer 0 6) 3) ; returns 3 (the (integer 0 6) 7) ; causes an error *Note TYPE-SPEC:: for a discussion of the legal type specifications. The is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: THIRD, Next: TRUE-LIST-LISTP, Prev: THE, Up: PROGRAMMING THIRD third member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: TRUE-LIST-LISTP, Next: TRUE-LISTP, Prev: THIRD, Up: PROGRAMMING TRUE-LIST-LISTP recognizer for true (proper) lists of true lists True-list-listp is the function that checks whether its argument is a list that ends in, or equals, nil, and furthermore, all of its elements have that property. Also *Note TRUE-LISTP::.  File: acl2-doc-lemacs.info, Node: TRUE-LISTP, Next: TRUNCATE, Prev: TRUE-LIST-LISTP, Up: PROGRAMMING TRUE-LISTP recognizer for proper (null-terminated) lists True-listp is the function that checks whether its argument is a list that ends in, or equals, nil.  File: acl2-doc-lemacs.info, Node: TRUNCATE, Next: TYPE-SPEC, Prev: TRUE-LISTP, Up: PROGRAMMING TRUNCATE division returning an integer by truncating toward 0 Example Forms: ACL2 !>(truncate 14 3) 4 ACL2 !>(truncate -14 3) -4 ACL2 !>(truncate 14 -3) -4 ACL2 !>(truncate -14 -3) 4 ACL2 !>(truncate -15 -3) 5 (Truncate i j) is the result of taking the quotient of i and j and dropping the fraction. For example, the quotient of -14 by 3 is -4 2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14 3) of -4. The guard for (truncate i j) requires that i and j are rational numbers and j is non-zero. Truncate is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: TYPE-SPEC, Next: UNARY--, Prev: TRUNCATE, Up: PROGRAMMING TYPE-SPEC type specifiers in declarations Examples: The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec. Other type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127), (RATIONAL 1 *), CHARACTER, and ATOM. The type-specs and their meanings (when applied to the variable x as in (declare (type type-spec x)) are given below. type-spec meaning ATOM (ATOM X) BIT (OR (EQUAL X 1) (EQUAL X 0)) CHARACTER (CHARACTERP X) COMPLEX, (AND (COMPLEX-RATIONALP X) (COMPLEX RATIONAL) (RATIONALP (REALPART X)) (RATIONALP (IMAGPART X))) (COMPLEX type) (AND (COMPLEX-RATIONALP X) (p (REALPART X)) (p (IMAGPART X))) where (p x) is the meaning for type-spec type CONS (CONSP X) INTEGER (INTEGERP X) (INTEGER i j) (AND (INTEGERP X) ; See notes below (<= i X) (<= X j)) (MEMBER x1 ... xn) (MEMBER X '(x1 ... xn)) (MOD i) same as (INTEGER 0 i-1) NIL NIL NULL (EQ X NIL) RATIO (AND (RATIONALP X) (NOT (INTEGERP X))) RATIONAL (RATIONALP X) (RATIONAL i j) (AND (RATIONALP X) ; See notes below (<= i X) (<= X j)) (SATISFIES pred) (pred X) SIGNED-BYTE (INTEGERP X) (SIGNED-BYTE i) same as (INTEGER -2**i-1 (2**i-1)-1) STANDARD-CHAR (STANDARD-CHARP X) STRING (STRINGP X) (STRING max) (AND (STRINGP X) (EQUAL (LENGTH X) max)) SYMBOL (SYMBOLP X) T T UNSIGNED-BYTE same as (INTEGER 0 *) (UNSIGNED-BYTE i) same as (INTEGER 0 (2**i)-1) *Notes:* In general, (integerp i j) means (AND (INTEGERP X) (<= i X) (<= X j)). But if i is the symbol *, the first inequality is omitted. If j is the symbol *, the second inequality is omitted. If instead of being an integer, the second element of the type specification is a list containing an integer, (i), then the first inequality is made strict. An analogous remark holds for the (j) case. The RATIONAL type specifier is similarly generalized.  File: acl2-doc-lemacs.info, Node: UNARY--, Next: UNARY-/, Prev: TYPE-SPEC, Up: PROGRAMMING UNARY-- arithmetic negation function Basic axiom: (equal (unary-- x) (if (acl2-numberp x) (unary-- x) 0)) Guard for (unary-- x): (acl2-numberp x) Notice that like all arithmetic functions, unary-- treats non-numeric inputs as 0. Calls of the macro - on one argument expand to calls of unary--; *Note -::.  File: acl2-doc-lemacs.info, Node: UNARY-/, Next: UNION-EQ, Prev: UNARY--, Up: PROGRAMMING UNARY-/ reciprocal function Basic axiom: (equal (unary-/ x) (if (and (acl2-numberp x) (not (equal x 0))) (unary-/ x) 0)) Guard for (unary-/ x): (and (acl2-numberp x) (not (equal x 0))) Notice that like all arithmetic functions, unary-/ treats non-numeric inputs as 0. Calls of the macro / on one argument expand to calls of unary-/; *Note /::.  File: acl2-doc-lemacs.info, Node: UNION-EQ, Next: UNION-EQUAL, Prev: UNARY-/, Up: PROGRAMMING UNION-EQ union of two lists of symbols (Union-eq x y) equals a list whose members (*Note MEMBER-EQ::) contains the members of x and the members of y. More precisely, the resulting list is the same as one would get by first deleting the members of y from x, and then concatenating the result to the front of y. The guard for union-eq requires both arguments to be true lists, but in fact further requires the first list to contain only symbols, as the function member-eq is used to test membership (with eq). *Note UNION-EQUAL::.  File: acl2-doc-lemacs.info, Node: UNION-EQUAL, Next: UPDATE-NTH, Prev: UNION-EQ, Up: PROGRAMMING UNION-EQUAL union of two lists (Union-equal x y) equals a list whose members (*Note MEMBER-EQUAL::) contains the members of x and the members of y. More precisely, the resulting list is the same as one would get by first deleting the members of y from x, and then concatenating the result to the front of y. The guard for union-equal requires both arguments to be true lists. Essentially, union-equal has the same functionality as the Common Lisp function union, except that it uses the equal function to test membership rather than eql. However, we do not include the function union in ACL2, because the Common Lisp language does not specify the order of the elements in the list that it returns.  File: acl2-doc-lemacs.info, Node: UPDATE-NTH, Next: UPPER-CASE-P, Prev: UNION-EQUAL, Up: PROGRAMMING UPDATE-NTH modify a list by putting the given value at the given position (Update-nth key val l) returns a list that is the same as the list l, except that the value at the 0-based position key (a natural number) is val. If key is an integer at least as large as the length of l, then l will be padded with the appropriate number of nil elements, as illustrated by the following example. ACL2 !>(update-nth 8 'z '(a b c d e)) (A B C D E NIL NIL NIL Z) We have the following theorem. (implies (and (true-listp l) (integerp key) (<= 0 key)) (equal (length (update-nth key val l)) (if (< key (length l)) (length l) (+ 1 key)))) The guard of update-nth requires that its first (position) argument is a natural number and its last (list) argument is a true list.  File: acl2-doc-lemacs.info, Node: UPPER-CASE-P, Next: ZERO-TEST-IDIOMS, Prev: UPDATE-NTH, Up: PROGRAMMING UPPER-CASE-P recognizer for upper case characters (Upper-case-p x) is true if and only if x is an upper case character, i.e., a member of the list #A, #B, ..., #Z. The guard for upper-case-p requires its argument to be a character. Upper-case-p is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: ZERO-TEST-IDIOMS, Next: ZEROP, Prev: UPPER-CASE-P, Up: PROGRAMMING ZERO-TEST-IDIOMS how to test for 0 Below are six commonly used idioms for testing whether x is 0. Zip and zp are the preferred termination tests for recursions down the integers and naturals, respectively. idiom logical guard primary meaning compiled code* (equal x 0)(equal x 0) t (equal x 0) (eql x 0) (equal x 0) t (eql x 0) (zerop x) (equal x 0) x is a number (= x 0) (= x 0) (equal x 0) x is a number (= x 0) (zip x) (equal (ifix x) 0) x is an integer (= x 0) (zp x) (equal (nfix x) 0) x is a natural (= x 0) **Note GUARDS-AND-EVALUATION::, especially the subsection titled "Guards and evaluation V: efficiency issues". Primary code is relevant only if guards are verified. The "compiled code" shown is only suggestive. The first four idioms all have the same logical meaning and differ only with respect to their executability and efficiency. In the absence of compiler optimizing, (= x 0) is probably the most efficient, (equal x 0) is probably the least efficient, and (eql x 0) is in between. However, an optimizing compiler could always choose to compile (equal x 0) as (eql x 0) and, in situations where x is known at compile-time to be numeric, (eql x 0) as (= x 0). So efficiency considerations must, of course, be made in the context of the host compiler. Note also that (zerop x) and (= x 0) are indistinguishable. They have the same meaning and the same guard, and can reasonably be expected to generate equally efficient code. Note that (zip x) and (zp x) do not have the same logical meanings as the others or each other. They are not simple tests for equality to 0. They each coerce x into a restricted domain, zip to the integers and zp to the natural numbers, choosing 0 for x when x is outside the domain. Thus, 1/2, #c(1 3), and 'abc, for example, are all "recognized" as zero by both zip and zp. But zip reports that -1 is different from 0 while zp reports that -1 "is" 0. More precisely, (zip -1) is nil while (zp -1) is t. Note that the last four idioms all have guards that restrict their Common Lisp executability. If these last four are used in situations in which guards are to be verified, then proof obligations are incurred as the price of using them. If guard verification is not involved in your project, then the first four can be thought of as synonymous. Zip and zp are not provided by Common Lisp but are ACL2-specific functions. Why does ACL2 provide these functions? The answer has to do with the admission of recursively defined functions and efficiency. Zp is provided as the zero-test in situations where the controlling formal parameter is understood to be a natural number. Zip is analogously provided for the integer case. We illustrate below. Here is an admissible definition of factorial (defun fact (n) (if (zp n) 1 (* n (fact (1- n))))) Observe the classic recursion scheme: a test against 0 and recursion by 1-. Note however that the test against 0 is expressed with the zp idiom. Note also the absence of a guard making explicit our intention that n is a natural number. This definition of factorial is readily admitted because when (zp n) is false (i.e., nil) then n is a natural number other than 0 and so (1- n) is less than n. The base case, where (zp n) is true, handles all the "unexpected" inputs, such as arise with (fact -1) and (fact 'abc). When calls of fact are evaluated, (zp n) checks (integerp n) and (> n 0). Guard verification is unsuccessful for this definition of fact because zp requires its argument to be a natural number and there is no guard on fact, above. Thus the primary raw lisp for fact is inaccessible and only the :logic definition (which does runtime "type" checking) is used in computation. In summary, this definition of factorial is easily admitted and easily manipulated by the prover but is not executed as efficiently as it could be. Runtime efficiency can be improved by adding a guard to the definition. (defun fact (n) (declare (xargs :guard (and (integerp n) (>= n 0)))) (if (zp n) 1 (* n (fact (1- n))))) This guarded definition has the same termination conditions as before -- termination is not sensitive to the guard. But the guards can be verified. This makes the primary raw lisp definition accessible during execution. In that definition, the (zp n) above is compiled as (= n 0), because n will always be a natural number when the primary code is executed. Thus, by adding a guard and verifying it, the elegant and easily used definition of factorial is also efficiently executed on natural numbers. Now let us consider an alternative definition of factorial in which (= n 0) is used in place of (zp n). (defun fact (n) (if (= n 0) 1 (* n (fact (1- n))))) This definition does not terminate. For example (fact -1) gives rise to a call of (fact -2), etc. Hence, this alternative is inadmissible. A plausible response is the addition of a guard restricting n to the naturals: (defun fact (n) (declare (xargs :guard (and (integerp n) (>= n 0)))) (if (= n 0) 1 (* n (fact (1- n))))) But because the termination argument is not sensitive to the guard, it is still impossible to admit this definition. To influence the termination argument one must change the conditions tested. Adding a runtime test that n is a natural number would suffice and allow both admission and guard verification. But such a test would slow down the execution of the compiled function. The use of (zp n) as the test avoids this dilemma. Zp provides the logical equivalent of a runtime test that n is a natural number but the execution efficiency of a direct = comparison with 0, at the expense of a guard conjecture to prove. In addition, if guard verification and most-efficient execution are not needed, then the use of (zp n) allows the admission of the function without a guard or other extraneous verbiage. While general rules are made to be broken, it is probably a good idea to get into the habit of using (zp n) as your terminating "0 test" idiom when recursing down the natural numbers. It provides the logical power of testing that n is a non-0 natural number and allows efficient execution. We now turn to the analogous function, zip. Zip is the preferred 0-test idiom when recursing through the integers toward 0. Zip considers any non-integer to be 0 and otherwise just recognizes 0. A typical use of zip is in the definition of integer-length, shown below. (ACL2 can actually accept this definition, but only after appropriate lemmas have been proved.) (defun integer-length (i) (declare (xargs :guard (integerp i))) (if (zip i) 0 (if (= i -1) 0 (+ 1 (integer-length (floor i 2)))))) Observe that the function recurses by (floor i 2). Hence, calling the function on 25 causes calls on 12, 6, 3, 1, and 0, while calling it on -25 generates calls on -13, -7, -4, -2, and -1. By making (zip i) the first test, we terminate the recursion immediately on non-integers. The guard, if present, can be verified and allows the primary raw lisp definition to check (= i 0) as the first terminating condition (because the primary code is executed only on integers).  File: acl2-doc-lemacs.info, Node: ZEROP, Next: ZIP, Prev: ZERO-TEST-IDIOMS, Up: PROGRAMMING ZEROP test an acl2-number against 0 (zerop x) is t if x is 0 and is nil otherwise. Thus, it is logically equivalent to (equal x 0). (Zerop x) has a guard requiring x to be numeric and can be expected to execute more efficiently than (equal x 0) in properly guarded compiled code. In recursions down the natural numbers, (zp x) is preferred over (zerop x) because the former coerces x to a natural and allows the termination proof. In recursions through the integers, (zip x) is preferred. *Note ZERO-TEST-IDIOMS::. Zerop is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: ZIP, Next: ZP, Prev: ZEROP, Up: PROGRAMMING ZIP testing an "integer" against 0 (Zip i) is logically equivalent to (equal (ifix i) 0) and is the preferred termination test for recursion through the integers. (Zip i) returns t if i is 0 or not an integer; it returns nil otherwise. Thus, i (zp i) 3 nil 0 t -2 nil 5/2 t #c(1 3) t 'abc t (Zip i) has a guard requiring i to be an integer. For a discussion of the various idioms for testing against 0, *Note ZERO-TEST-IDIOMS::. Zip is typically used as the termination test in recursions through the integers. It has the advantage of "coercing" its argument to an integer and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows zip to be compiled as a direct =-comparision with 0.