Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.8 Copyright (C) 1989-95 Computational Logic, Inc. (CLI). All rights reserved.  File: acl2-doc-emacs.info, Node: FMT1, Next: FOURTH, Prev: FMT, Up: PROGRAMMING FMT1 :(str alist col co-channel state evisc) => (mv col state) See *Note FMT:: for further explanation. The tilde-directives are ~px pretty print vx (maybe after printing a newline) ~qx pretty print 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 ~p, separated by commas and a final "and" ~vx print elements of vx with ~p, 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-emacs.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-emacs.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-emacs.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 x, y 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.  File: acl2-doc-emacs.info, Node: IFF, Next: IFIX, Prev: IF, Up: PROGRAMMING IFF logical "if and only if" Iff is the ACL2 biconditional, "if and only if". (iff P Q) means that either P and Q are both false (i.e., nil) or both true (i.e., not nil).  File: acl2-doc-emacs.info, Node: IFIX, Next: ILLEGAL, Prev: IFF, Up: PROGRAMMING IFIX coerce to an integer Ifix simply returns any integer argument unchanged, returning 0 on a non-integer argument. Also see *Note NFIX::, see *Note RFIX::, and see *Note FIX:: for analogous functions that coerce to a natural number, a rational number, and a number, respectively. Ifix has a guard of t.  File: acl2-doc-emacs.info, Node: ILLEGAL, Next: IMAGPART, Prev: IFIX, Up: PROGRAMMING ILLEGAL cause a hard error (illegal ctx str alist) causes evaluation to halt with a short message using the "context" ctx. An error message is printed using the string str and alist alist that are of the same kind as expected by fmt. See *Note FMT::.  File: acl2-doc-emacs.info, Node: IMAGPART, Next: IMPLIES, Prev: ILLEGAL, Up: PROGRAMMING IMAGPART imaginary part of a complex number Basic axiom: (equal (imagpart x) (if (acl2-numberp x) (imagpart x) 0)) Guard for (imagpart x): (acl2-numberp x)  File: acl2-doc-emacs.info, Node: IMPLIES, Next: IMPROPER-CONSP, Prev: IMAGPART, Up: PROGRAMMING IMPLIES logical implication Implies is the ACL2 implication function. (implies P Q) means that either P is false (i.e., nil) or Q is true (i.e., not nil).  File: acl2-doc-emacs.info, Node: IMPROPER-CONSP, Next: INT=, Prev: IMPLIES, Up: PROGRAMMING IMPROPER-CONSP recognizer for improper (non-null-terminated) non-empty lists Improper-consp is the function that checks whether its argument is a non-empty list that ends in other than nil. See *Note PROPER-CONSP:: and also see *Note TRUE-LISTP::.  File: acl2-doc-emacs.info, Node: INT=, Next: INTEGER-LENGTH, Prev: IMPROPER-CONSP, Up: PROGRAMMING INT= test equality of two integers (int= x y) is logically equivalent to (equal x y). Unlike equal, int= requires its arguments to be numbers (or else causes a guard violation; see *Note GUARD::). Generally, int= is executed more efficiently than equal or = on integers.  File: acl2-doc-emacs.info, Node: INTEGER-LENGTH, Next: INTEGER-LISTP, Prev: INT=, Up: PROGRAMMING INTEGER-LENGTH number of bits in two's complement integer representation For non-negative integers, (integer-length i) is the minimum number of bits needed to represent the integer. Any integer can be represented as a signed two's complement field with a minimum of (+ (integer-length i) 1) bits. The guard for integer-length requires its argument to be an integer. Integer-length is defined in Common Lisp. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: INTEGER-LISTP, Next: INTEGERP, Prev: INTEGER-LENGTH, Up: PROGRAMMING INTEGER-LISTP recognizer for a true list of integers The predicate integer-listp tests whether its argument is a true list of integers.  File: acl2-doc-emacs.info, Node: INTEGERP, Next: INTERN, Prev: INTEGER-LISTP, Up: PROGRAMMING INTEGERP recognizer for whole numbers (integerp x) is true if and only if x is an integer.  File: acl2-doc-emacs.info, Node: INTERN, Next: INTERN-IN-PACKAGE-OF-SYMBOL, Prev: INTEGERP, Up: PROGRAMMING INTERN create a new symbol in a given package (intern symbol-name symbol-package-name) returns a symbol with the given symbol-name and the given symbol-package-name. We restrict Common Lisp's intern so that the second argument is either the symbol *main-lisp-package-name*, the value of that constant, or is one of "ACL2", "ACL2-INPUT-CHANNEL", "ACL2-OUTPUT-CHANNEL", or "KEYWORD". In ACL2 intern is actually implemented as a macro that expands to a call of a similar function whose second argument is a symbol. Invoke :pe intern to see the definition, or see *Note INTERN-IN-PACKAGE-OF-SYMBOL::. To see why is intern so restricted consider (intern "X" "P"). In particular, is it a symbol and if so, what is its symbol-package-name? One is tempted to say "yes, it is a symbol in the package "P"." But if package "P" has not yet been defined, that would be premature because the imports to the package are unknown. For example, if "P" were introduced with (defpkg "P" '(LISP::X)) then in Common Lisp (symbol-package-name (intern "X" "P")) returns "LISP". The obvious restriction on intern is that its second argument be the name of a package known to ACL2. We cannot express such a restriction (except, for example, by limiting it to those packages known at some fixed time, as we do). Instead, we provide intern-in-package-of-symbol which requires a "witness symbol" for the package instead of the package. The witness symbol is any symbol (expressible in ACL2) and uniquely specifies a package necessarily known to ACL2.  File: acl2-doc-emacs.info, Node: INTERN-IN-PACKAGE-OF-SYMBOL, Next: INTERSECTP-EQ, Prev: INTERN, Up: PROGRAMMING INTERN-IN-PACKAGE-OF-SYMBOL create a symbol with a given name Basic axiom: (equal (intern-in-package-of-symbol x y) (if (and (stringp x) (symbolp y)) (intern-in-package-of-symbol x y) nil)) Guard for (intern-in-package-of-symbol x y): (and (stringp x) (symbolp y)) Intuitively, (intern-in-package-of-symbol x y) creates a symbol with symbol-name x interned in the package containing y. More precisely, suppose x is a string, y is a symbol with symbol-package-name pkg and that the defpkg event creating pkg had the list of symbols imports as the value of its second argument. Then (intern-in-package-of-symbol x y) returns a symbol, ans, the symbol-name of ans is x, and the symbol-package-name of ans is pkg, unless x is the symbol-name of some member of imports with symbol-package-name ipkg, in which case the symbol-package-name of ans is ipkg. Because defpkg requires that there be no duplications among the symbol-names of the imports, intern-in-package-of-symbol is uniquely defined. For example, suppose "MY-PKG" was created by (defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)). Let w be 'my-pkg::witness. Observe that (symbolp w) is t ; w is a symbol (symbol-name w) is "WITNESS" ; w's name is "WITNESS" (symbol-package-name w) is "MY-PKG" ; w is in the package "MY-PKG" The construction of w illustrates one way to obtain a symbol in a given package: write it down as a constant using the double-colon notation. But another way to obtain a symbol in a given package is to create it with intern-in-package-of-symbol. (intern-in-package-of-symbol "XYZ" w) is MY-PKG::XYZ (intern-in-package-of-symbol "ABC" w) is ACL2::ABC (intern-in-package-of-symbol "CAR" w) is LISP::CAR (intern-in-package-of-symbol "car" w) is MY-PKG::|car|  File: acl2-doc-emacs.info, Node: INTERSECTP-EQ, Next: INTERSECTP-EQUAL, Prev: INTERN-IN-PACKAGE-OF-SYMBOL, Up: PROGRAMMING INTERSECTP-EQ test whether two lists of symbols intersect See *Note INTERSECTP-EQUAL::, which is logically the same function. (Intersectp-eq x y) has a guard that x and y are lists of symbols.  File: acl2-doc-emacs.info, Node: INTERSECTP-EQUAL, Next: IO, Prev: INTERSECTP-EQ, Up: PROGRAMMING INTERSECTP-EQUAL test whether two lists intersect (Intersectp-equal x y) returns t if x and y have a member in common, else it returns nil. Also see *Note INTERSECTP-EQ::, which is logically the same but can be more efficient since it uses eq instead of equal to look for members common to the two given lists. (Intersectp-equal x y) has a guard that x and y are true lists.  File: acl2-doc-emacs.info, Node: IO, Next: IRRELEVANT-FORMALS, Prev: INTERSECTP-EQUAL, Up: PROGRAMMING IO input/output facilities in ACL2 Example: (mv-let (channel state) (open-input-channel "foo.lisp" :object state) (mv-let (eofp obj state) (read-object channel state) (. . (let ((state (close-input-channel channel state))) (mv final-ans state))..))) Also see *Note FILE-READING-EXAMPLE::. ACL2 supports input and output facilities equivalent to a subset of those found in Common Lisp. ACL2 does not support random access files or bidirectional streams. In Common Lisp, input and output are to or from objects of type stream. In ACL2, input and output are to or from objects called "channels," which are actually symbols. Although a channel is a symbol, one may think of it intuitively as corresponding to a Common Lisp stream. Channels are in one of two ACL2 packages, "ACL2-INPUT-CHANNEL" and "ACL2-OUTPUT-CHANNEL". When one "opens" a file one gets back a channel whose symbol-name is the file name passed to "open," postfixed with -n, where n is a counter that is incremented every time an open or close occurs. There are three channels which are open from the beginning and which cannot be closed: acl2-input-channel::standard-character-input-0 acl2-input-channel::standard-object-input-0 acl2-input-channel::standard-character-output-0 All three of these are really Common Lisp's *standard-input* or *standard-output*, appropriately. For convenience, three global variables are bound to these rather tedious channel names: *standard-ci* *standard-oi* *standard-co* Common Lisp permits one to open a stream for several different kinds of io, e.g. character or byte. ACL2 permits an additional type called "object". In ACL2 an "io-type" is a keyword, either :character, :byte, or :object. When one opens a file, one specifies a type, which determines the kind of io operations that can be done on the channel returned. The types :character and :byte are familiar. Type :object is an abstraction not found in Common Lisp. An :object file is a file of Lisp objects. One uses read-object to read from :object files and print-object$ to print to :object files. (The reading and printing are really done with the Common Lisp read and print functions.) File-names are strings. ACL2 does not support the Common Lisp type pathname. Here are the signatures of the ACL2 io functions. See *Note SIGNATURE::. Input Functions: (open-input-channel (file-name io-type state) (mv channel state)) (open-input-channel-p (channel io-type state) boolean) (close-input-channel (channel state) state) (read-char$ (channel state) (mv char/nil state)) (peek-char$ (channel state) boolean) (read-byte$ (channel state) (mv byte/nil state)) (read-object (channel state) (mv eof-read-flg obj-read state)) Output Functions: (open-output-channel (file-name io-type state) (mv channel state)) (open-output-channel-p (channel io-type state) boolean) (close-output-channel (channel state) state) (princ$ (obj channel state) state) (write-byte$ (byte channel state) state) (print-object$ (obj channel state) state) (fms (string alist channel state evisc-tuple) state) (fmt (string alist channel state evisc-tuple) (mv col state)) (fmt1 (string alist col channel state evisc-tuple) (mv col state)) The "formatting" functions are particularly useful; see *Note FMT::. When one enters ACL2 with (lp), input and output are taken from *standard-oi* to *standard-co*. Because these are synonyms for *standard-input* and *standard-output*, one can drive ACL2 io off of arbitrary Common Lisp streams, bound to *standard-input* and *standard-output* before entry to ACL2.  File: acl2-doc-emacs.info, Node: IRRELEVANT-FORMALS, Next: KEYWORD-VALUE-LISTP, Prev: IO, Up: PROGRAMMING IRRELEVANT-FORMALS formals that are used but only insignificantly Let fn be a function of n arguments. Let x be the ith formal of fn. We say x is "irrelevant in fn" if x is not involved in either the guard or the measure for fn, x is used in the body, but the value of (fn a1...ai...an) is independent of ai. The easiest way to define a function with an irrelevant formal is simply not to use the formal in the guard, measure, or body of the function. Such formals are said to be "ignored" by Common Lisp and a special declaration is provided to allow ignored formals. ACL2 makes a distinction between ignored and irrelevant formals. An example of an irrelevant formal is x in the definition of fact below. (defun fact (i x) (declare (xargs :guard (and (integerp i) (<= 0 i)))) (if (zerop i) 0 (* i (fact (1- i) (cons i x))))). Observe that x is only used in recursive calls of fact; it never "gets out" into the result. ACL2 can detect some irrelevant formals by a closure analysis on how the formals are used. For example, if the ith formal is only used in the ith argument position of recursive calls, then it is irrelevant. This is how x is used above. It is possible for a formal to appear only in recursive calls but still be relevant. For example, x is *not* irrelevant below, even though it only appears in the recursive call. (defun fn (i x) (if (zerop i) 0 (fn x (1- i)))) The key observation above is that while x only appears in a recursive call, it appears in an argument position, namely i's, that is relevant. (The function above can be admitted with a :guard requiring both arguments to be nonnegative integers and the :measure (+ i x).) Establishing that a formal is irrelevant, in the sense defined above, can be an arbitrarily hard problem because it requires theorem proving. For example, is x irrelevant below? (defun test (i j k x) (if (cond i j k) x 0)) Note that the value of (test i j k x) is independent of x -- thus making x irrelevant -- precisely if (cond i j k) is a theorem. ACL2's syntactic analysis of a definition does not guarantee to notice all irrelevant formals. We regard the presence of irrelevant formals as an indication that something is wrong with the definition. We cause an error on such definitions and suggest that you recode the definition so as to eliminate the irrelevant formals. If you must have an irrelevant formal, one way to "trick" ACL2 into accepting the definition, without slowing down the execution of your function, is to use the formal in an irrelevant way in the guard. For example, to admit fact, above, with its irrelevant x one might use (defun fact (i x) (declare (xargs :guard (and (integerp i) (<= 0 i) (equal x x)))) (if (zerop i) 0 (* i (fact (1- i) (cons i x))))) For those who really want to turn off this feature, we have provided a way to use the acl2-defaults-table for this purpose; see *Note SET-IRRELEVANT-FORMALS-OK::. If you need to introduce a function with an irrelevant formal, please explain to the authors why this should be allowed.  File: acl2-doc-emacs.info, Node: KEYWORD-VALUE-LISTP, Next: KEYWORDP, Prev: IRRELEVANT-FORMALS, Up: PROGRAMMING KEYWORD-VALUE-LISTP recognizer for true lists whose even-position elements are keywords (keyword-value-listp l) is true if and only if l is a list of even length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword.  File: acl2-doc-emacs.info, Node: KEYWORDP, Next: LAST, Prev: KEYWORD-VALUE-LISTP, Up: PROGRAMMING KEYWORDP recognizer for keywords (Keywordp x) is true if and only if x is a keyword, i.e., a symbol in the "KEYWORD" package. Such symbols are typically printed using a colon (:) followed by the symbol-name of the symbol. Keywordp has a guard of t. Keywordp is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: LAST, Next: LENGTH, Prev: KEYWORDP, Up: PROGRAMMING LAST the last cons (not element) of a list (Last l) is the last cons of a list. Here are examples. ACL2 !>(last '(a b . c)) (B . C) ACL2 !>(last '(a b c)) (C) (Last l) has a guard of (listp l); thus, l need not be a true-listp. Last is a Common Lisp function. See any Common Lisp documentation for more information. Unlike Common Lisp, we do not allow an optional second argument for last.  File: acl2-doc-emacs.info, Node: LENGTH, Next: LET, Prev: LAST, Up: PROGRAMMING LENGTH length of a string or proper list Length is the function for determining the length of a sequence. In ACL2, the argument is required to be either a true-listp or a string. Length is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: LET, Next: LET*, Prev: LENGTH, Up: PROGRAMMING LET binding of lexically scoped (local) variables Example LET Form: (let ((x (* x x)) (y (* 2 x))) (list x y)) If the form above is executed in an environment in which x has the value -2, then the result is '(4 -4). Let expressions bind variables so that their "local" values, the values they have when the "body" of the let is evaluated, are possibly different than their "global" values, the values they have in the context in which the let expression appears. In the let expression above, the local variables bound by the let are x and y. They are locally bound to the values delivered by the two forms (* x x) and (* 2 x), respectively, that appear in the "bindings" of the let. The body of the let is (list x y). Suppose that the let expression above occurs in a context in which x has the value -2. (The global value of y is irrelevant to this example.) For example, one might imagine that the let form above occurs as the body of some function, fn, with the formal parameter x and we are evaluating (fn -2). To evaluate the let above in a context in which x is -2, we first evaluate the two forms specifying the local values of the variables. Thus, (* x x) is evaluated and produces 4 (because x is -2) and (* 2 x) is evaluated and produces -4 (because x is -2). Then x and y are bound to these values and the body of the let is evaluated. Thus, when the body, (list x y) is evaluated, x is 4 and y is -4. Thus, the body produces '(4 -4). Note that the binding of y, which is written after the binding of x and which mentions x, nevertheless uses the global value of x, not the new local value. That is, the local variables of the let are bound "in parallel" rather than "sequentially." In contrast, if the Example LET* Form: (let* ((x (* x x)) (y (* 2 x))) (list x y)) is evaluated when the global value of x is -2, then the result is '(4 8), because the local value of y is computed after x has been bound to 4. Let* binds its local variables "sequentially." General LET Forms: (let ((var1 term1) ... (varn termn)) body) and (let ((var1 term1) ... (varn termn)) (declare ...) ... (declare ...) body) where the vari are distinct variables, the termi are terms involving only variables bound in the environment containing the let, and body is a term involving only the vari plus the variables bound in the environment containing the let. Each vari must be used in body or else declared ignored. A let form is evaluated by first evaluating each of the termi, obtaining for each a vali. Then, each vari is bound to the corresponding vali and body is evaluated. Actually, let forms are just abbreviations for certain uses of lambda notation. In particular (let ((var1 term1) ... (varn termn)) (declare ...) body) is equivalent to ((lambda (var1 ... varn) (declare ...) body) term1 ... termn). Let* forms are used when it is desired to bind the vari sequentially, i.e., when the local values of preceding varj are to be used in the computation of the local value for vari. General LET* Forms: (let* ((var1 term1) ... (varn termn)) body) where the vari are distinct variables, the termi are terms involving only variables bound in the environment containing the let* and those varj such that j(mod 14 3) 2 ACL2 !>(mod -14 3) 1 ACL2 !>(mod 14 -3) -1 ACL2 !>(mod -14 -3) -2 ACL2 !>(mod -15 -3) 0 ACL2 !> (Mod i j) is that number k that (* j (floor i j)) added to k equals i. The guard for (mod i j) requires that i and j are rational numbers and j is non-zero. Mod is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: MV, Next: MV-LET, Prev: MOD, Up: PROGRAMMING MV returning multiple values Mv is the mechanism provided by ACL2 for returning two or more values. Logically, (mv x1 x2 ... xn) is the same as (list x1 x2 ... xn), a list of the indicated values. However, ACL2 avoids the cost of building this list structure, with the cost that mv may only be used in a certain style in definitions: if a function ever returns using mv (either directly, or by calling another function that returns multiple values), then this function must always return the same number of multiple values. For more explanation of the multiple value mechanism, see *Note MV-LET::. ACL2 does not support the Common Lisp construct values, whose logical meaning seems difficult to characterize. Mv is the ACL2 analogue of that construct.  File: acl2-doc-emacs.info, Node: MV-LET, Next: MV-NTH, Prev: MV, Up: PROGRAMMING MV-LET calling multi-valued ACL2 functions Example Form: (mv-let (x y z) ; local variables (mv 1 2 3) ; multi-valued expression (declare (ignore y)) ; optional declarations (cons x z)) ; body The form above binds the three "local variables," x, y, and z, to the three results returned by the multi-valued expression and then evaluates the body. The result is '(1 . 3). The second local, y, is declared ignored. The multi-valued expression can be any ACL2 expression that returns k results, where k is the number of local variables listed. Often however it is simply the application of a k-valued function. Mv-let is the standard way to invoke a multi-valued function when the caller must manipulate the vector of results returned. General Form: (mv-let (var1 ... vark) term body) or (mv-let (var1 ... vark) term (declare ...) ... (declare ...) body) where the vari are distinct variables, term is a term that returns k results and mentions only variables bound in the environment containing the mv-let expression, and body is a term mentioning only the vari and variables bound in the environment containing the mv-let. Each vari must occur in body unless it is declared ignored in one of the optional declare forms, unless this requirement is turned off; see *Note SET-IGNORE-OK::. The value of the mv-let term is the result of evaluating body in an environment in which the vari are bound, in order, to the k results obtained by evaluating term in the environment containing the mv-let. Here is an extended example that illustrates both the definition of a multi-valued function and the use of mv-let to call it. Consider a simple binary tree whose interior nodes are conses and whose leaves are non-conses. Suppose we often need to know the number, n, of interior nodes of such a tree; the list, syms, of symbols that occur as leaves; and the list, ints, of integers that occur as leaves. (Observe that there may be leaves that are neither symbols nor integers.) Using a multi-valued function we can collect all three results in one pass. Here is the first of two definitions of the desired function. This definition is "primitive recursive" in that it has only one argument and that argument is reduced in size on every recursion. (defun count-and-collect (x) ; We return three results, (mv n syms ints) as described above. (cond ((atom x) ; X is a leaf. Thus, there are 0 interior nodes, and depending on ; whether x is a symbol, an integer, or something else, we return ; the list containing x in as the appropriate result. (cond ((symbolp x) (mv 0 (list x) nil)) ((integerp x)(mv 0 nil (list x))) (t (mv 0 nil nil)))) (t ; X is an interior node. First we process the car, binding n1, syms1, and ; ints1 to the answers. (mv-let (n1 syms1 ints1) (count-and-collect (car x)) ; Next we process the cdr, binding n2, syms2, and ints2. (mv-let (n2 syms2 ints2) (count-and-collect (car x)) ; Finally, we compute the answer for x from those obtained for its car ; and cdr, remembering to increment the node count by one for x itself. (mv (1+ (+ n1 n2)) (append syms1 syms2) (append ints1 ints2))))))) This use of multiple values to "do several things at once" is very common in ACL2. However, the function above is inefficient because it appends syms1 to syms2 and ints1 to ints2, copying the list structures of syms1 and ints1 in the process. By adding "accumulators" to the function, we can make the code more efficient. (defun count-and-collect1 (x n syms ints) (cond ((atom x) (cond ((symbolp x) (mv n (cons x syms) ints)) ((integerp x) (mv n syms (cons x ints))) (t (mv n syms ints)))) (t (mv-let (n2 syms2 ints2) (count-and-collect1 (cdr x) (1+ n) syms ints) (count-and-collect1 (car x) n2 syms2 ints2))))) We claim that (count-and-collect x) returns the same triple of results as (count-and-collect1 x 0 nil nil). The reader is urged to study this claim until convinced that it is true and that the latter method of computing the results is more efficient. One might try proving the theorem (defthm count-and-collect-theorem (equal (count-and-collect1 x 0 nil nil) (count-and-collect x))). Hint: the inductive proof requires attacking a more general theorem. ACL2 does not support the Common Lisp construct multiple-value-bind, whose logical meaning seems difficult to characterize. Mv-let is the ACL2 analogue of that construct.  File: acl2-doc-emacs.info, Node: MV-NTH, Next: NFIX, Prev: MV-LET, Up: PROGRAMMING MV-NTH the mv-nth element (zero-based) of a list (Mv-nth n l) is the nth element of l, zero-based. If n is greater than or equal to the length of l, then mv-nth returns nil. (Mv-nth n l) has a guard that n is a non-negative integer and l is a true-listp. Mv-nth is equivalent to the Common Lisp function nth, but is used by ACL2 to access the nth value returned by a multiply valued expression. For an example of the use of mv-nth, try ACL2 !>:trans1 (mv-let (erp val state) (read-object ch state) (value (list erp val)))  File: acl2-doc-emacs.info, Node: NFIX, Next: NINTH, Prev: MV-NTH, Up: PROGRAMMING NFIX coerce to a natural number Nfix simply returns any natural number argument unchanged, returning 0 on an argument that is not a natural number. Also see *Note NFIX::, see *Note RFIX::, and see *Note FIX:: for analogous functions that coerce to an integer, a rational number, and a number, respectively. Nfix has a guard of t.  File: acl2-doc-emacs.info, Node: NINTH, Next: NO-DUPLICATESP, Prev: NFIX, Up: PROGRAMMING NINTH ninth member of the list See any Common Lisp documentation for details.  File: acl2-doc-emacs.info, Node: NO-DUPLICATESP, Next: NONNEGATIVE-INTEGER-QUOTIENT, Prev: NINTH, Up: PROGRAMMING NO-DUPLICATESP check for duplicates in a list (no-duplicatesp l) is true if and only if no member of l occurs twice in l. (no-duplicatesp l) has a guard of (true-listp l). Membership is tested using member-equal, hence using equal as the test.  File: acl2-doc-emacs.info, Node: NONNEGATIVE-INTEGER-QUOTIENT, Next: NOT, Prev: NO-DUPLICATESP, Up: PROGRAMMING NONNEGATIVE-INTEGER-QUOTIENT natural number division function Example Forms: (nonnegative-integer-quotient 14 3) ; equals 4 (nonnegative-integer-quotient 15 3) ; equals 5 (nonnegative-integer-quotient i j) returns the integer quotient of the integers i and (non-zero) j, i.e., the largest k such that (* j k) is less than or equal to i. Also see *Note FLOOR::, see *Note CEILING:: and see *Note TRUNCATE::, which are derived from this function and apply to rational numbers. The guard of (nonnegative-integer-quotient i j) requires that i is a nonnegative integer and j is an integer.  File: acl2-doc-emacs.info, Node: NOT, Next: NTH, Prev: NONNEGATIVE-INTEGER-QUOTIENT, Up: PROGRAMMING NOT logical negation Iff is the ACL2 negation function. The negation of nil is t and the negation of anything else is nil. Not is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: NTH, Next: NTHCDR, Prev: NOT, Up: PROGRAMMING NTH the nth element (zero-based) of a list (Nth n l) is the nth element of l, zero-based. If n is greater than or equal to the length of l, then nth returns nil. (Nth n l) has a guard that n is a non-negative integer and l is a true-listp. Nth is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: NTHCDR, Next: NULL, Prev: NTH, Up: PROGRAMMING NTHCDR final segment of a list (Nthcdr n l) removes the first n elements from the list l. The following is a theorem. (implies (and (integerp n) (<= 0 n) (true-listp l)) (equal (length (nthcdr n l)) (if (<= n (length l)) (- (length l) n) 0))) For related functions, see *Note TAKE:: and see *Note BUTLAST::. The guard of (nthcdr n l) requires that n is a nonnegative integer and l is a true list. Nthcdr is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: NULL, Next: NUMERATOR, Prev: NTHCDR, Up: PROGRAMMING NULL recognizer for the empty list Null is the function that checks whether its argument is nil. For recursive definitions it is often preferable to test for the end of a list using endp instead of null; see *Note ENDP::. Null is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: NUMERATOR, Next: ODDP, Prev: NULL, Up: PROGRAMMING NUMERATOR dividend of a ratio in lowest terms Basic axiom: (equal (numerator x) (if (rationalp x) (numerator x) 0)) Guard for (numerator x): (rationalp x)  File: acl2-doc-emacs.info, Node: ODDP, Next: OR, Prev: NUMERATOR, Up: PROGRAMMING ODDP test whether an integer is odd (oddp x) is true if and only if x is odd, i.e., not even in the sense of evenp. The guard for oddp requires its argument to be an integer. Oddp is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: OR, Next: PAIRLIS, Prev: ODDP, Up: PROGRAMMING OR conjunction Or is the macro for disjunctions. Or takes any number of arguments and returns the first that is non-nil, or nil if there is no non-nil element. Or is a Common Lisp macro. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: PAIRLIS, Next: PAIRLIS$, Prev: OR, Up: PROGRAMMING PAIRLIS see pairlis$ The Common Lisp language allows its pairlis function to construct an alist in any order! So we have to define our own version: See *Note PAIRLIS$::.  File: acl2-doc-emacs.info, Node: PAIRLIS$, Next: PLUSP, Prev: PAIRLIS, Up: PROGRAMMING PAIRLIS$ zipper together two lists The Common Lisp language allows its pairlis function to construct an alist in any order! So we have to define our own version, pairlis$. It returns the list of pairs obtained by consing together successive respective members of the given lists. The guard for pairlis$ requires that its arguments are true lists.  File: acl2-doc-emacs.info, Node: PLUSP, Next: POSITION, Prev: PAIRLIS$, Up: PROGRAMMING PLUSP test whether a rational number is positive (Plusp x) is true if and only if x > 0. The guard of plusp requires its argument to be a rational number. Plusp is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-emacs.info, Node: POSITION, Next: POSITION-EQ, Prev: PLUSP, Up: PROGRAMMING POSITION position of an item in a string or a list, using eql as test (Position item seq) is the least index (zero-based) of the element item in the string or list seq, if in fact item is an element of seq. Otherwise (position item seq) is nil. (Position item lst) is provably the same in the ACL2 logic as (position-equal item lst). It has a stronger guard than position-equal because uses eql to test equality of item with members of lst. Its guard requires that lst is a true list, and moreover, either (eqlablep item) or all members of lst are eqlablep. See *Note POSITION-EQUAL:: and see *Note POSITION-EQ::. Position is a Common Lisp function. See any Common Lisp documentation for more information. Since ACL2 functions cannot take keyword arguments (though macros can), the ACL2 functions position-equal and position-eq are defined to correspond to calls of the Common Lisp function position whose keyword argument :test is equal or eq, respectively.