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: CDAAAR, Next: CDAADR, Prev: CASE-MATCH, Up: PROGRAMMING CDAAAR cdr of the caaar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDAADR, Next: CDAAR, Prev: CDAAAR, Up: PROGRAMMING CDAADR cdr of the caadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDAAR, Next: CDADAR, Prev: CDAADR, Up: PROGRAMMING CDAAR cdr of the caar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDADAR, Next: CDADDR, Prev: CDAAR, Up: PROGRAMMING CDADAR cdr of the cadar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDADDR, Next: CDADR, Prev: CDADAR, Up: PROGRAMMING CDADDR cdr of the caddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDADR, Next: CDAR, Prev: CDADDR, Up: PROGRAMMING CDADR cdr of the cadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDAR, Next: CDDAAR, Prev: CDADR, Up: PROGRAMMING CDAR cdr of the car See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDAAR, Next: CDDADR, Prev: CDAR, Up: PROGRAMMING CDDAAR cdr of the cdaar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDADR, Next: CDDAR, Prev: CDDAAR, Up: PROGRAMMING CDDADR cdr of the cdadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDAR, Next: CDDDAR, Prev: CDDADR, Up: PROGRAMMING CDDAR cdr of the cdar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDDAR, Next: CDDDDR, Prev: CDDAR, Up: PROGRAMMING CDDDAR cdr of the cddar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDDDR, Next: CDDDR, Prev: CDDDAR, Up: PROGRAMMING CDDDDR cdr of the cdddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDDR, Next: CDDR, Prev: CDDDDR, Up: PROGRAMMING CDDDR cdr of the cddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDDR, Next: CDR, Prev: CDDDR, Up: PROGRAMMING CDDR cdr of the cdr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CDR, Next: CEILING, Prev: CDDR, Up: PROGRAMMING CDR returns the second element of a cons pair, else nil Basic axiom: (equal (cdr x) (cond ((consp x) (cdr x)) (t nil))) Guard: (or (consp x) (equal x nil)) Notice that in the ACL2 logic, cdr returns nil for every atom.  File: acl2-doc-lemacs.info, Node: CEILING, Next: CHAR, Prev: CDR, Up: PROGRAMMING CEILING division returning an integer by truncating toward positive infinity Example Forms: ACL2 !>(ceiling 14 3) 5 ACL2 !>(ceiling -14 3) -4 ACL2 !>(ceiling 14 -3) -4 ACL2 !>(ceiling -14 -3) 5 ACL2 !>(ceiling -15 -3) 5 (Ceiling i j) is the result of taking the quotient of i and j and returning the smallest integer that is at least as great as that quotient. For example, the quotient of -14 by 3 is -4 2/3, and the smallest integer at least that great is -4. The guard for (ceiling i j) requires that i and j are rational numbers and j is non-zero. Ceiling is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR, Next: CHAR-CODE, Prev: CEILING, Up: PROGRAMMING CHAR the nth element (zero-based) of a string (Char s n) is the nth element of s, zero-based. If n is greater than or equal to the length of s, then char returns nil. (Char s n) has a guard that n is a non-negative integer and s is a stringp. Char is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR-CODE, Next: CHAR-DOWNCASE, Prev: CHAR, Up: PROGRAMMING CHAR-CODE the numeric code for a given character Basic axiom: (equal (char-code x) (if (characterp x) (char-code x) 0)) Guard for (char-code x): (characterp x) This function maps all non-characters to 0.  File: acl2-doc-lemacs.info, Node: CHAR-DOWNCASE, Next: CHAR-EQUAL, Prev: CHAR-CODE, Up: PROGRAMMING CHAR-DOWNCASE turn upper-case characters into lower-case characters (Char-downcase x) is equal to #A when x is #a, #B when x is #b, ..., and #Z when x is #z, and is x for any other character. The guard for char-downcase requires its argument to be a character. Char-downcase is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR-EQUAL, Next: CHAR-UPCASE, Prev: CHAR-DOWNCASE, Up: PROGRAMMING CHAR-EQUAL character equality without regard to case For characters x and y, (char-equal x y) is true if and only if x and y are the same except perhaps for their case. The guard on char-equal requires that its arguments are both characters. Char-equal is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR-UPCASE, Next: CHAR<, Prev: CHAR-EQUAL, Up: PROGRAMMING CHAR-UPCASE turn lower-case characters into upper-case characters (Char-upcase x) is equal to #A when x is #a, #B when x is #b, ..., and #Z when x is #z, and is x for any other character. The guard for char-upcase requires its argument to be a character. Char-upcase is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR<, Next: CHAR<=, Prev: CHAR-UPCASE, Up: PROGRAMMING CHAR< less-than test for characters (char< x y) is true if and only if the character code of x is less than that of y. *Note CHAR-CODE::. The guard for char< specifies that its arguments are characters. Char< is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR<=, Next: CHAR>, Prev: CHAR<, Up: PROGRAMMING CHAR<= less-than-or-equal test for characters (char<= x y) is true if and only if the character code of x is less than or equal to that of y. *Note CHAR-CODE::. The guard for char<= specifies that its arguments are characters. Char<= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR>, Next: CHAR>=, Prev: CHAR<=, Up: PROGRAMMING CHAR> greater-than test for characters (char> x y) is true if and only if the character code of x is greater than that of y. *Note CHAR-CODE::. The guard for char> specifies that its arguments are characters. Char> is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHAR>=, Next: CHARACTER-LISTP, Prev: CHAR>, Up: PROGRAMMING CHAR>= greater-than-or-equal test for characters (char>= x y) is true if and only if the character code of x is greater than or equal to that of y. *Note CHAR-CODE::. The guard for char>= specifies that its arguments are characters. Char>= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CHARACTER-LISTP, Next: CHARACTERP, Prev: CHAR>=, Up: PROGRAMMING CHARACTER-LISTP recognizer for a true list of characters The predicate character-listp tests whether its argument is a true list of characters.  File: acl2-doc-lemacs.info, Node: CHARACTERP, Next: CHARACTERS, Prev: CHARACTER-LISTP, Up: PROGRAMMING CHARACTERP recognizer for characters (characterp x) is true if and only if x is a character.  File: acl2-doc-lemacs.info, Node: CHARACTERS, Next: CODE-CHAR, Prev: CHARACTERP, Up: PROGRAMMING CHARACTERS characters in ACL2 ACL2 accepts 256 distinct characters, which are the characters obtained by applying the function code-char to each integer from 0 to 255. Among these, Common Lisp designates certain ones as *standard characters*, namely those of the form (code-char n) where n is from 33 to 126, together with #\Newline and #\Space. The actual standard characters may be viewed by evaluating the defconst *standard-chars*. To be more precise, Common Lisp does not specify the precise relationship between code-char and the standard characters. However, we check that the underlying Common Lisp implementation uses a particular relationship that extends the usual ASCII coding of characters. We also check that Space, Tab, Newline, Page, and Rubout correspond to characters with respective char-codes 32, 9, 10, 12, and 127. Code-char has an inverse, char-code. Thus, when char-code is applied to an ACL2 character, c, it returns a number n between 0 and 255 inclusive such that (code-char n) = c. The preceding paragraph implies that there is only one ACL2 character with a given character code. CLTL allows for "attributes" for characters, which could allow distinct characters with the same code, but ACL2 does not allow this. *The Character Reader* ACL2 support the `#\' notation for characters provided by Common Lisp, with some restrictions. First of all, for every character c, the notation #\c may be used to denote the character object c. That is, the user may type in this notation and ACL2 will read it as denoting the character object c. In this case, the character immediately following c must be one of the following "terminating characters": a Tab, a Newline, a Page character, a space, or one of the characters: " ' ( ) ; ` , Other than the notation above, ACL2 accepts alternate notation for five characters. #\Space #\Tab #\Newline #\Page #\Rubout Again, in each of these cases the next character must be from among the set of "terminating characters" described in the single-character case. Our implementation is consistent with IS0-8859, even though we don't provide #\ syntax for entering characters other than that described above. Finally, we note that it is our intention that any object printed by ACL2's top-level-loop may be read back into ACL2. Please notify the implementors if you find a counterexample to this claim.  File: acl2-doc-lemacs.info, Node: CODE-CHAR, Next: COERCE, Prev: CHARACTERS, Up: PROGRAMMING CODE-CHAR the character corresponding to a given numeric code Basic axiom: (equal (code-char x) (if (and (integerp x) (>= x 0) (< x 256)) (code-char x) (code-char 0))) Guard for (code-char x): (and (integerp x) (>= x 0) (< x 256)) ACL2 supports 8-bit characters. Inputs not between 0 and 255 are treated as 0.  File: acl2-doc-lemacs.info, Node: COERCE, Next: COMPILATION, Prev: CODE-CHAR, Up: PROGRAMMING COERCE coerce a character list to a string and a string to a list Basic axiom: (equal (coerce x y) (cond ((equal y 'list) (if (stringp x) (coerce x 'list) nil)) (t (coerce (make-character-list x) 'string)))) Guard for (coerce x y): (if (equal y 'list) (stringp x) (if (equal y 'string) (character-listp x) nil))  File: acl2-doc-lemacs.info, Node: COMPILATION, Next: COMPLEX, Prev: COERCE, Up: PROGRAMMING COMPILATION compiling ACL2 functions Example: ACL2 !>:comp app ACL2 !>:set-compile-fns t *Note COMP:: and *Note SET-COMPILE-FNS::.  File: acl2-doc-lemacs.info, Node: COMPLEX, Next: COMPLEX-RATIONALP, Prev: COMPILATION, Up: PROGRAMMING COMPLEX create an ACL2 number Examples: (complex x 3) ; x + 3i, where i is the principal square root of -1 (complex x y) ; x + yi (complex x 0) ; same as x, for rational numbers x The function complex takes two rational number arguments and returns an ACL2 number. This number will be of type (complex rational) [as defined in the Common Lisp language], except that if the second argument is zero, then complex returns its first argument. The function complex-rationalp is a recognizer for complex rational numbers, i.e. for ACL2 numbers that are not rational numbers. The reader macro #C (which is the same as #c) provides a convenient way for typing in complex numbers. For explicit rational numbers x and y, #C(x y) is read to the same value as (complex x y). The functions realpart and imagpart return the real and imaginary parts (respectively) of a complex (possibly rational) number. So for example, (realpart #C(3 4)) = 3, (imagpart #C(3 4)) = 4, (realpart 3/4) = 3/4, and (imagpart 3/4) = 0. A basic axiom that shows what complex returns on arguments violating its guard (which says that both arguments are rational numbers) is the following. (equal (complex x y) (complex (if (rationalp x) x 0) (if (rationalp y) y 0)))  File: acl2-doc-lemacs.info, Node: COMPLEX-RATIONALP, Next: CONCATENATE, Prev: COMPLEX, Up: PROGRAMMING COMPLEX-RATIONALP recognizes complex rational numbers Examples: (complex-rationalp 3) ; nil, as 3 is rational, not complex rational (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 (complex-rationalp t) ; nil (complex-rationalp #c(3 1)) ; t, as #c(3 1) is the complex number 3 + i *Note COMPLEX:: for more about complex rationals in ACL2.  File: acl2-doc-lemacs.info, Node: CONCATENATE, Next: COND, Prev: COMPLEX-RATIONALP, Up: PROGRAMMING CONCATENATE concatenate lists or strings together Examples: (concatenate 'string "ab" "cd" "ef") ; equals "abcdef" (concatenate 'string "ab") ; equals "ab" (concatenate 'list '(a b) '(c d) '(e f)) ; equals '(a b c d e f) (concatenate 'list) ; equals nil General Form: (concatenate result-type x1 x2 ... xn) where n >= 0 and either: result-type is 'string and each xi is a string; or result-type is 'list and each xi is a true list. Concatenate simply concatenates its arguments to form the result string or list. Also *Note APPEND:: and *Note STRING-APPEND::, though concatenate is probably preferable to string-append for efficiency. Note: We do *not* try to comply with the Lisp language's insistence that concatenate copies its arguments. Not only are we in an applicative setting, where this issue shouldn't matter for the logic, but also we do not actually modify the underlying lisp implementation of concatenate; we merely provide a definition for it. Concatenate is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: COND, Next: CONJUGATE, Prev: CONCATENATE, Up: PROGRAMMING COND conditional based on if-then-else Cond is the construct for IF, THEN, ELSE IF, ... The test is against nil. The argument list for cond is a list of "clauses", each of which is a list. In ACL2, clauses must have length 1 or 2. Cond is a Common Lisp macro. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CONJUGATE, Next: CONS, Prev: COND, Up: PROGRAMMING CONJUGATE complex number conjugate Conjugate takes an ACL2 number as an argument, and returns its complex conjugate (i.e., the result of negating its imaginary part.). Conjugate is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: CONS, Next: CONSP, Prev: CONJUGATE, Up: PROGRAMMING CONS pair and list constructor (cons x y) is a pair whose first component is x and second component is y. If y is a list, then (cons x y) is a list that has an addtional element x on the front.  File: acl2-doc-lemacs.info, Node: CONSP, Next: DECLARE, Prev: CONS, Up: PROGRAMMING CONSP recognizer for cons pairs (consp x) is true if and only if x is a cons pair.  File: acl2-doc-lemacs.info, Node: DECLARE, Next: DENOMINATOR, Prev: CONSP, Up: PROGRAMMING DECLARE declarations Examples: (declare (ignore x y z)) (declare (ignore x y z) (type integer i j k) (type (satisfies integerp) m1 m2)) (declare (xargs :guard (and (integerp i) (<= 0 i)) :guard-hints (("Goal" :use (:instance lemma3 (x (+ i j))))))) General Form: (declare d1 ... dn) where, in ACL2, each di is of one of the following forms: (ignore v1 ... vn) -- where each vi is a variable introduced in the immediately superior lexical environment. (type type-spec v1 ... vn) -- where each vi is a variable introduced in the immediately superior lexical environment and type-spec is a type specifier (as described in the documentation for type-spec). (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's and their respective vali's are described in the documentation for xargs. Declarations in ACL2 may occur only where dcl occurs below: (DEFUN name args doc-string dcl ... dcl body) (DEFMACRO name args doc-string dcl ... dcl body) (LET ((v1 t1) ...) dcl ... dcl body) (MV-LET (v1 ...) term dcl ... dcl body) Of course, if a form macroexpands into one of these (as let* expands into nested lets and our er-let* expands into nested mv-lets) then declarations are permitted as handled by the macros involved. Declare is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: DENOMINATOR, Next: DIGIT-CHAR-P, Prev: DECLARE, Up: PROGRAMMING DENOMINATOR divisor of a ratio in lowest terms Basic axiom: (equal (denominator x) (if (rationalp x) (denominator x) 1)) Guard for (denominator x): (rationalp x)  File: acl2-doc-lemacs.info, Node: DIGIT-CHAR-P, Next: DIGIT-TO-CHAR, Prev: DENOMINATOR, Up: PROGRAMMING DIGIT-CHAR-P the number, if any, corresponding to a given character (digit-char-p ch) is the integer corresponding to the character ch in base 10. For example, (digit-char-p #\3) is equal to the integer 3. More generally, an optional second argument specifies the radix (default 10, as indicated above). The guard for digit-char-p (more precisely, for the function our-digit-char-p that calls of this macro expand to) requires its second argument to be an integer between 2 and 36, inclusive, and its first argument to be a character. Digit-char-p is a Common Lisp function, though it is implemented in the ACL2 logic as an ACL2 macro. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: DIGIT-TO-CHAR, Next: EIGHTH, Prev: DIGIT-CHAR-P, Up: PROGRAMMING DIGIT-TO-CHAR map a digit to a character Example: ACL2 !>(digit-to-char 8) #\8 For an integer n from 0 to 9, (digit-to-char n) is the character corresponding to n in decimal notation. The guard for digit-to-char requires its argument to be an integer between 0 and 9, inclusive.  File: acl2-doc-lemacs.info, Node: EIGHTH, Next: ENDP, Prev: DIGIT-TO-CHAR, Up: PROGRAMMING EIGHTH eighth member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: ENDP, Next: EQ, Prev: EIGHTH, Up: PROGRAMMING ENDP recognizer for empty lists In the ACL2 logic, (endp x) is the same as (atom x). *Note ATOM::. Unlike atom, the guard for endp requires that x is a cons pair or is nil. Thus, endp is typically used as a termination test for functions that recur on a true-listp argument. *Note GUARD:: for general information about guards. Endp is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: EQ, Next: EQL, Prev: ENDP, Up: PROGRAMMING EQ equality of symbols Eq is the function for determining whether two objects are identical (i.e., have the exact same store address in the current von Neumann implementation of Common Lisp). It is the same as equal in the ACL2 logic. Eq is a Common Lisp function. In order to ensure conformance with Common Lisp, the ACL2 guard on eq requires at least one of the arguments to eq to be a symbol. Common Lisp guarantees that if x is a symbol, then x is eq to y if and only if x is equal to y. Thus, the ACL2 user should think of eq as nothing besides a fast means for checking equal when one argument is known to be a symbol. In particular, it is possible that an eq test will not even require the cost of a function call but will be as fast as a single machine instruction.  File: acl2-doc-lemacs.info, Node: EQL, Next: EQLABLE-ALISTP, Prev: EQ, Up: PROGRAMMING EQL test equality (of two numbers, symbols, or characters) (eql x y) is logically equivalent to (equal x y). Unlike equal, eql has a guard requiring at least one of its arguments to be a number, a symbol, or a character. Generally, eql is executed more efficiently than equal. For a discussion of the various ways to test against 0, *Note ZERO-TEST-IDIOMS::. Eql is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: EQLABLE-ALISTP, Next: EQLABLE-LISTP, Prev: EQL, Up: PROGRAMMING EQLABLE-ALISTP recognizer for a true list of pairs whose cars are suitable for eql The predicate eqlable-alistp tests whether its argument is a true-listp of consp objects whose cars all satisfy eqlablep.  File: acl2-doc-lemacs.info, Node: EQLABLE-LISTP, Next: EQLABLEP, Prev: EQLABLE-ALISTP, Up: PROGRAMMING EQLABLE-LISTP recognizer for a true list of objects each suitable for eql The predicate eqlable-listp tests whether its argument is a true-listp of objects satisfying eqlablep.  File: acl2-doc-lemacs.info, Node: EQLABLEP, Next: EQUAL, Prev: EQLABLE-LISTP, Up: PROGRAMMING EQLABLEP the guard for the function eql The predicate eqlablep tests whether its argument is suitable for eql, at least one of whose arguments must satisfy this predicate in Common Lisp. (Eqlablep x) is true if and only if its argument is a number, a symbol, or a character.  File: acl2-doc-lemacs.info, Node: EQUAL, Next: ER-PROGN, Prev: EQLABLEP, Up: PROGRAMMING EQUAL true equality (equal x y) is equal to t or nil, according to whether or not x and y are the same value. For a discussion of the various idioms for testing against 0, *Note ZERO-TEST-IDIOMS::.  File: acl2-doc-lemacs.info, Node: ER-PROGN, Next: EVENP, Prev: EQUAL, Up: PROGRAMMING ER-PROGN perform a sequence of state-changing "error triples" Example: (er-progn (check-good-foo-p (f-get-global 'my-foo state) state) (value (* (f-get-global 'my-foo state) (f-get-global 'bar state)))) This sequencing primitive is only useful when programming with state, something that very few users will probably want to do. *Note STATE::. Er-progn is used much the way that progn is used in Common Lisp, except that it expects each form within it to evaluate to an "error triple" of the form (mv erp val state). The first such form, if any, that evaluates to such a triple where erp is not nil yields the error triple returned by the er-progn. If there is no such form, then the last form returns the value of the er-progn form. We intend to write more about this topic, especially if there are requests to do so.  File: acl2-doc-lemacs.info, Node: EVENP, Next: EXPLODE-NONNEGATIVE-INTEGER, Prev: ER-PROGN, Up: PROGRAMMING EVENP test whether an integer is even (evenp x) is true if and only if the integer x is even. Actually, in the ACL2 logic (evenp x) is defined to be true when x/2 is an integer. The guard for evenp requires its argument to be an integer. Evenp is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: EXPLODE-NONNEGATIVE-INTEGER, Next: EXPT, Prev: EVENP, Up: PROGRAMMING EXPLODE-NONNEGATIVE-INTEGER the list of characters in the decimal form of a number Example: ACL2 !>(explode-nonnegative-integer 325 nil) (#3 #2 #5) For a non-negative integer n, (explode-nonnegative-integer n nil) is the list of characters in the decimal representation of n. The guard for explode-nonnegative-integer requires the first argument to be a nonnegative integer.  File: acl2-doc-lemacs.info, Node: EXPT, Next: FIFTH, Prev: EXPLODE-NONNEGATIVE-INTEGER, Up: PROGRAMMING EXPT exponential function (Expt r i) is the result of raising the number r to the integer power i. The guard for (expt r i) is that r is a number and i is an integer, and furthermore, if r is 0 then i is nonnegative. When the type requirements of the guard aren't met, (expt r i) first coerces r to a number and i to an integer. Expt is a Common Lisp function. See any Common Lisp documentation for more information. Note that r can be a complex number; this is consistent with Common lisp.  File: acl2-doc-lemacs.info, Node: FIFTH, Next: FIRST, Prev: EXPT, Up: PROGRAMMING FIFTH fifth member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: FIRST, Next: FIX, Prev: FIFTH, Up: PROGRAMMING FIRST first member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: FIX, Next: FIX-TRUE-LIST, Prev: FIRST, Up: PROGRAMMING FIX coerce to a number Fix simply returns any numeric argument unchanged, returning 0 on a non-numeric argument. Also *Note NFIX::, *Note IFIX::, and *Note RFIX:: for analogous functions that coerce to a natural number, an integer, and a rational number, respectively. Fix has a guard of t.  File: acl2-doc-lemacs.info, Node: FIX-TRUE-LIST, Next: FLOOR, Prev: FIX, Up: PROGRAMMING FIX-TRUE-LIST coerce to a true list Fix-true-list is the identity function on true-listp objects. It converts every list to a true list by dropping the final cdr, and it converts every atom to nil.  File: acl2-doc-lemacs.info, Node: FLOOR, Next: FMS, Prev: FIX-TRUE-LIST, Up: PROGRAMMING FLOOR division returning an integer by truncating toward negative infinity Example Forms: ACL2 !>(floor 14 3) 4 ACL2 !>(floor -14 3) -5 ACL2 !>(floor 14 -3) -5 ACL2 !>(floor -14 -3) 4 ACL2 !>(floor -15 -3) 5 (Floor i j) returns the result of taking the quotient of i and j and returning the greatest integer not exceeding that quotient. For example, the quotient of -14 by 3 is -4 2/3, and the largest integer not exceeding that rational number is -5. The guard for (floor i j) requires that i and j are rational numbers and j is non-zero. Floor is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: FMS, Next: FMT, Prev: FLOOR, Up: PROGRAMMING FMS :(str alist co-channel state evisc) => state *Note FMT:: for further explanation. The tilde-directives are ~xx pretty print vx (maybe after printing a newline) ~yx pretty print vx starting in current column; end with newline ~Xxy like ~xx but use vy as the evisceration tuple ~Yxy like ~yx but use vy as the evisceration tuple ~px pretty print term (maybe with infix) vx (maybe after printing a newline) ~qx pretty print term (maybe with infix) vx starting in current column; end with newline ~Pxy like ~px but use vy as the evisceration tuple ~Qxy like ~qx but use vy as the evisceration tuple ~@x if vx is a string, "str", recursively format "str" if vx is ("str" . a), recursively format "str" under a+ ~#x~[...~/...~/ ... ~/...~] cases on vx ^ ^ ... ^ if 0<=vx<=k, choose vxth alternative 0 1 ... k if vx is a list of length 1, case 0; else 1 ~*x iterator: vx must be of the form ("str0" "str1" "str2" "str3" lst . a); if lst is initially empty, format "str0" under a+; otherwise, bind #\* successively to the elements of lst and then recursively format "stri" under a+, where i=1 if there is one element left to process, i=2 if there are two left, and i=3 otherwise. ~&x print elements of vx with ~x, separated by commas and a final "and" ~vx print elements of vx with ~x, separated by commas and a final "or" ~nx if vx is a small positive integer, print it as a word, e.g., seven; if vx is a singleton containing a small positive integer, print the corresponding ordinal as a word, e.g., seventh ~Nx like ~nx but the word is capitalized, e.g., Seven or Seventh ~tx tab out to column vx; newline first if at or past column vx ~cx vx is (n . w), print integer n right justified in field of width w ~fx print object vx flat over as many lines as necessary ~Fx same as ~f, except that subsequent lines are indented to start one character to the right of the first character printed ~sx if vx is a symbol, print vx, breaking on hyphens; if vx is a string, print the characters in it, breaking on hyphens ~ tilde space: print a space ~_x print vx spaces ~ tilde newline: skip following whitespace ~% output a newline ~| output a newline unless already on left margin ~~ print a tilde ~- if close to rightmargin, output a hyphen and newline; else skip this char  File: acl2-doc-lemacs.info, Node: FMT, Next: FMT1, Prev: FMS, Up: PROGRAMMING FMT formatted printing ACL2 provides the functions fmt, fmt1, and fms as substitutes for Common Lisp's format function. All three print a given string under an alist pairing character objects with values, interpreting certain "tilde-directives" in the string. Channel must be a character output channel (e.g., *standard-co*). General Forms: result (fms string alist channel state evisc-tuple) ; state (fmt string alist channel state evisc-tuple) ; (mv col state) (fmt1 string alist column channel state evisc-tuple) ; (mv col state) Fms and fmt print an initial newline to put channel in column 0; Fmt1 requires the current column as input. Columns are numbered from 0. The current column is the column into which the next character will be printed. (Thus, the current column number is also the number of characters printed since the last newline.) The col returned by fmt and fmt1 is the current column at the conclusion of the formatting. Evisc-tuple must be either nil (meaning no abbreviations are used when objects are printed) or an "evisceration tuple" such as that returned by (default-evisc-tuple state). We list the tilde-directives below. The notation is explained after the chart. ~xx pretty print vx (maybe after printing a newline) ~yx pretty print vx starting in current column; end with newline ~Xxy like ~xx but use vy as the evisceration tuple ~Yxy like ~yx but use vy as the evisceration tuple ~px pretty print term (maybe with infix) vx (maybe after printing a newline) ~qx pretty print term (maybe with infix) vx starting in current column; end with newline ~Pxy like ~px but use vy as the evisceration tuple ~Qxy like ~qx but use vy as the evisceration tuple ~@x if vx is a string, "str", recursively format "str" if vx is ("str" . a), recursively format "str" under a+ ~#x~[...~/...~/ ... ~/...~] cases on vx ^ ^ ... ^ if 0<=vx<=k, choose vxth alternative 0 1 ... k if vx is a list of length 1, case 0; else 1 ~*x iterator: vx must be of the form ("str0" "str1" "str2" "str3" lst . a); if lst is initially empty, format "str0" under a+; otherwise, bind #\* successively to the elements of lst and then recursively format "stri" under a+, where i=1 if there is one element left to process, i=2 if there are two left, and i=3 otherwise. ~&x print elements of vx with ~x, separated by commas and a final "and" ~vx print elements of vx with ~x, separated by commas and a final "or" ~nx if vx is a small positive integer, print it as a word, e.g., seven; if vx is a singleton containing a small positive integer, print the corresponding ordinal as a word, e.g., seventh ~Nx like ~nx but the word is capitalized, e.g., Seven or Seventh ~tx tab out to column vx; newline first if at or past column vx ~cx vx is (n . w), print integer n right justified in field of width w ~fx print object vx flat over as many lines as necessary ~Fx same as ~f, except that subsequent lines are indented to start one character to the right of the first character printed ~sx if vx is a symbol, print vx, breaking on hyphens; if vx is a string, print the characters in it, breaking on hyphens ~ tilde space: print a space ~_x print vx spaces ~ tilde newline: skip following whitespace ~% output a newline ~| output a newline unless already on left margin ~~ print a tilde ~- if close to rightmargin, output a hyphen and newline; else skip this char If x is a character, then vx is the value of #\x under the current alist. When we say "format str under a+" we mean recursively process the given string under an alist obtained by appending a to the current alist. ACL2's formatting functions print to the indicated channel, keeping track of which column they are in. Fmt1 can be used if the caller knows which column the channel is in (i.e., how many characters have been printed since the last newline). Otherwise, fmt or fms must be used, both of which output a newline so as to establish the column position at 0. Unlike Common Lisp's format routine, fmt and its relatives break the output into lines so as to try to avoid printing past column 77. That number is built-into the definitions of ACL2's formatting functions. Line breaks are automatically inserted as necessary in place of spaces and after hyphens in the text being printed. The formatting functions scan the string from left to right, printing each successive character unless it is a tilde (~). Upon encountering tildes the formatters take action determined by the character or characters immediately following the tilde. The typical tilde-directive is a group of three successive characters from the string being printed. For example, ~x0 is a 3 character tilde-directive. The first character in a tilde-directive is always the tilde character itself. The next character is called the "command" character. The character after that is usually taken as the name of a "format variable" that is bound in the alist under which the string is being printed. Format variables are, by necessity, characters. The objects actually printed by a tilde-directive are the objects obtained by looking up the command's format variables in the alist. Typical format variable names are 0, 1, 2, ..., 9, a, b, c, etc., and if a tilde-directive uses the format variable 0, as in ~x0, then the character #\0 must be bound in the alist. Some tilde commands take no arguments and others take more than one, so some directives are of length two and others are longer. It should be noted that this use of characters in the string to denote arguments is another break from Common Lisp's format routine. In Common Lisp, the directives refer implicitly to the "next item to be printed." But in ACL2 the directives name each item explicitly with our format variables. The following text contains examples that can be evaluated. To make this process easier, we use a macro which is defined as part of ACL2 just for this documentation. The macro is named fmx and it takes up to eleven arguments, the first of which is a format string, str, and the others of which are taken as the values of format variables. The variables used are #\0 through #\9. The macro constructs an appropriate alist, a, and then evaluates (fmt str a *standard-co* state nil). Thus, (fmx "Here is v0, ~x0, and here is v1, ~x1." (cons 'value 0) (cons 'value 1)) is just an abbreviation for (fmt "Here is v0, ~x0, and here is v1, ~x1." (list (cons #\0 (cons 'value 0)) (cons #\1 (cons 'value 1))) *standard-co* state nil) which returns (mv 53 state) after printing the line Here is v0, (VALUE . 0), and here is v1, (VALUE . 1). We now devote special attention to three of the tilde-directives whose use is non-obvious. *The Case Statement* ~#x is essentially a "case statement" in the language of fmt. The proper form of the statement is ~#x~[case-0~/case-1~/ ... ~/case-k~], where each of the case-i is a format string. In the most common use, the variable x has an integer value, vx, between 0 and k, inclusive. The effect of formatting the directive is to format case-vx. For example (fmx "Go ~#0~[North~/East~/South~/West~].~%" 1) will print "Go East." followed by a newline and will return (mv 0 state), while if you change the 1 above to 3 (the maximum legal value), it will print "Go West." In order to make it easier to print such phrases as "there are seven cases" requiring agreement between subject and verb based on the number of elements of a list, the case statement allows its variable to take a list as its value and selects case-0 if the list has length 1 and case-1 otherwise. (let ((cases '(a b c))) (fmx "There ~#0~[is ~n1 case~/are ~n1 cases~]." cases (length cases))) will print "There are three cases." but if you change the '(a b c) above simply to '(a) it will print "There is one case." and if you change it to nil it will print "There are zero cases." *Indirection* Roughly speaking, ~@ will act as though the value of its argument is a format string and splice it into the current string at the current position. It is often used when the phrase to be printed must be computed. For example, (let ((ev 'DEFUN)) (fmx "~x0 is an event~@1." 'foo (if (member-eq ev '(defun defstub encapsulate)) " that may introduce a function symbol" ""))) will print "foo is an event that may introduce a function symbol," but if the value of ev is changed from 'defun to 'defthm, it prints "foo is an event." The ~@ directive "splices" in the computed phrase (which might be empty). Of course, this particular example could be done with the case statement ~#1~[~/ that may introduce a function symbol~] where the value of #\1 is appropriately computed to be 0 or 1. If the argument to ~@ is a pair, it is taken to be a format string consed onto an alist, i.e., ("str" . a), and the alist, a, is used to extend the current one before "str" is recursively processed. This feature of fmt can be used to pass around "phrases" that contain computed contextual information in a. The most typical use is as "error messages." For example, suppose you are writing a function which does not have access to state and so cannot print an error message. It may nevertheless be necessary for it to signal an error to its caller, say by returning two results, the first of which is interpreted as an error message if non-nil. Our convention is to use a ~@ pair to represent such messages. For example, the error value might be produced by the code: (cons "Error: The instruction ~x0 is illegal when the stack is ~x1.~%" (list (cons #\0 (current-instruction st)) (cons #\1 (i-stack st)))) If the current-instruction and i-stack (whatever they are) are '(popi 3) and '(a b) when the cons above is evaluated, then it produces '("Error: The instruction ~x0 is illegal when the stack is ~x1.~%" (#\0 POPI 3) (#\1 A B)) and if this pair is made the value of the fmt variable 0, then ~@0 will print Error: The instruction (POPI 3) is illegal when the stack is (A B). For example, evaluate (let ((pair '("Error: The instruction ~x0 is illegal when the stack is ~x1.~%" (#\0 POPI 3) (#\1 A B)))) (fmx "~@0" pair)). Thus, even though the function that produced the "error" could not print it, it could specify exactly what error message and data are to be printed. This example raises another issue. Sometimes it is desirable to break lines in your format strings so as to make your source code more attractive. That is the purpose of the tilde-newline directive. The following code produces exactly the same output as described above. (let ((pair '("Error: The instruction ~x0 ~ is illegal when the stack is ~ ~x1.~%" (#\0 POPI 3) (#\1 A B)))) (fmx "~@0" pair)). Finally, observe that when ~@0 extends the current alist, alist, with the one, a, in its argument, the bindings from a are added to the front of alist, overriding the current values of any shared variables. This insures that the variable values seen by the recursively processed string, "str", are those from a, but if "str" uses variables not bound in a, their values are as specified in the original alist. Intuitively, variables bound in a are local to the processing of ("str" . a) but "str" may use "global variables." The example above illustrates this because when the ~@0 is processed, #\0 is bound to the error message pair. But when the ~x0 in the error string is processed, #\0 is bound to the illegal instruction. *Iteration* The ~* directive is used to process each element of a list. For example, (let ((lst '(a b c d e f g h))) ; a true-list whose elements we exhibit (fmx "~*0" `("Whoa!" ; what to print if there's nothing to print "~x*!" ; how to print the last element "~x* and " ; how to print the 2nd to last element "~x*, " ; how to print all other elements ,lst))) ; the list of elements to print will print "A, B, C, D, E, F, G and H!". Try this example with other true list values of lst, such as '(a b), '(a), and nil. The tilde-directives ~&0 and ~v0, which take a true list argument and display its elements separated by commas and a final "and" or "or," are implemented in terms of the more general ~*. The ~* directive allows the 5-tuple to specify in its final cdr an alist with which to extend the current one before processing the individual elements. We often use ~* to print a series of phrases, separated by suitable punctuation, whitespace and noise words. In such use, the ~* handles the separation of the phrases and each phrase is generally printed by ~@. Here is a complex example. In the let*, below, we bind phrases to a list of ~@ pairs and then we create a ~* 5-tuple to print out the conjunction of the phrases with a parenthetical "finally!" if the series is longer than 3. (let* ((phrases (list (list "simplifying with the replacement rules ~&0" (cons #\0 '(rewrite-rule1 rewrite-rule2 rewrite-rule3))) (list "destructor elimination using ~x0" (cons #\0 'elim-rule)) (list "generalizing the terms ~&0" (cons #\0 '((rev x) (app u v)))) (list "inducting on ~x0" (cons #\0 'I)))) (5-tuple (list "magic" ; no phrases "~@*" ; last phrase "~@*, and~#f~[~/ (finally!)~] " ; second to last phrase "~@*, " ; other phrases phrases ; the phrases themselves (cons #\f (if (>(length phrases) 3) 1 0))))) ;print "finally"? (fmx "We did it by ~*0." 5-tuple)) This let* prints We did it by simplifying with the replacement rules REWRITE-RULE1, REWRITE-RULE2 and REWRITE-RULE3, destructor elimination using ELIM- RULE, generalizing the terms (REV X) and (APP U V), and (finally!) inducting on I. You might wish to try evaluating the let* after removing elements of phrases. Most of the output produced by ACL2 is produced via fmt statements. Thus, inspection of the source code will yield many examples. A complicated example is the code that explains the simplifier's work. See :pc simplify-clause-msg1. An ad hoc example is provided by the function fmt-doc-example, which takes two arguments: an arbitrary true list and state. To see how fmt-doc-example works, :pe fmt-doc-example. (fmt-doc-example '(a b c d e f g h i j k l m n o p) state) will produce the output Here is a true list: (A B C D E F G H I J K L M N O P). It has 16 elements, the third of which is C. We could print each element in square brackets: ([A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [almost there: O], [the end: P]). And if we wished to itemize them into column 15 we could do it like this 0123456789012345 0 (zeroth) A 1 (first) B 2 (second) C 3 (third) D 4 (fourth) E 5 (fifth) F 6 (sixth) G 7 (seventh) H 8 (eighth) I 9 (ninth) J 10 (tenth) K 11 (eleventh) L 12 (twelfth) M 13 (thirteenth) N 14 (14th) O 15 (15th) P End of example. and return (mv 15 state). Finally, we should remind the reader that fmt and its subfunctions, most importantly fmt0, are written entirely in ACL2. We make this comment for two reasons. First, it illustrates the fact that quite low level code can be efficiently written in the language. Second, it means that as a last resort for documentation purposes you can read the source code without changing languages.  File: acl2-doc-lemacs.info, Node: FMT1, Next: FOURTH, Prev: FMT, Up: PROGRAMMING FMT1 :(str alist col co-channel state evisc) => (mv col state) *Note FMT:: for further explanation. The tilde-directives are ~xx pretty print vx (maybe after printing a newline) ~yx pretty print vx starting in current column; end with newline ~Xxy like ~xx but use vy as the evisceration tuple ~Yxy like ~yx but use vy as the evisceration tuple ~px pretty print term (maybe with infix) vx (maybe after printing a newline) ~qx pretty print term (maybe with infix) vx starting in current column; end with newline ~Pxy like ~px but use vy as the evisceration tuple ~Qxy like ~qx but use vy as the evisceration tuple ~@x if vx is a string, "str", recursively format "str" if vx is ("str" . a), recursively format "str" under a+ ~#x~[...~/...~/ ... ~/...~] cases on vx ^ ^ ... ^ if 0<=vx<=k, choose vxth alternative 0 1 ... k if vx is a list of length 1, case 0; else 1 ~*x iterator: vx must be of the form ("str0" "str1" "str2" "str3" lst . a); if lst is initially empty, format "str0" under a+; otherwise, bind #\* successively to the elements of lst and then recursively format "stri" under a+, where i=1 if there is one element left to process, i=2 if there are two left, and i=3 otherwise. ~&x print elements of vx with ~x, separated by commas and a final "and" ~vx print elements of vx with ~x, separated by commas and a final "or" ~nx if vx is a small positive integer, print it as a word, e.g., seven; if vx is a singleton containing a small positive integer, print the corresponding ordinal as a word, e.g., seventh ~Nx like ~nx but the word is capitalized, e.g., Seven or Seventh ~tx tab out to column vx; newline first if at or past column vx ~cx vx is (n . w), print integer n right justified in field of width w ~fx print object vx flat over as many lines as necessary ~Fx same as ~f, except that subsequent lines are indented to start one character to the right of the first character printed ~sx if vx is a symbol, print vx, breaking on hyphens; if vx is a string, print the characters in it, breaking on hyphens ~ tilde space: print a space ~_x print vx spaces ~ tilde newline: skip following whitespace ~% output a newline ~| output a newline unless already on left margin ~~ print a tilde ~- if close to rightmargin, output a hyphen and newline; else skip this char  File: acl2-doc-lemacs.info, Node: FOURTH, Next: IDENTITY, Prev: FMT1, Up: PROGRAMMING FOURTH fourth member of the list See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: IDENTITY, Next: IF, Prev: FOURTH, Up: PROGRAMMING IDENTITY the identity function (Identity x) equals x; what else can we say? Identity is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: IF, Next: IFF, Prev: IDENTITY, Up: PROGRAMMING IF if-then-else function (if x y z) is equal to y if x is any value other than nil, and is equal to z if x is nil. Only one of y, z is evaluated when (if x y z) is evaluated. If has a guard of t. If is part of Common Lisp. See any Common Lisp documentation for more information.