FMT1

Parent topic:  PROGRAMMING
Home

See 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

FOURTH

Parent topic:  PROGRAMMING
Home

See any Common Lisp documentation for details.

IDENTITY

Parent topic:  PROGRAMMING
Home

(Identity x) equals x; what else can we say?

Identity is a Common Lisp function. See any Common Lisp documentation for more information.

IF

Parent topic:  PROGRAMMING
Home

(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.

IFF

Parent topic:  PROGRAMMING
Home

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).

IFIX

Parent topic:  PROGRAMMING
Home

Ifix simply returns any integer argument unchanged, returning 0 on a non-integer argument. Also see nfix, see rfix, and see fix for analogous functions that coerce to a natural number, a rational number, and a number, respectively.

Ifix has a guard of t.

ILLEGAL

Parent topic:  PROGRAMMING
Home

(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 fmt.

IMAGPART

Parent topic:  PROGRAMMING
Home

Basic axiom:

(equal (imagpart x)
       (if (acl2-numberp x)
           (imagpart x)
         0))

Guard for (imagpart x):

(acl2-numberp x)

IMPLIES

Parent topic:  PROGRAMMING
Home

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).

IMPROPER-CONSP

Parent topic:  PROGRAMMING
Home

Improper-consp is the function that checks whether its argument is a non-empty list that ends in other than nil. See proper-consp and also see true-listp.

INT=

Parent topic:  PROGRAMMING
Home

(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 guard). Generally, int= is executed more efficiently than equal or = on integers.

INTEGER-LENGTH

Parent topic:  PROGRAMMING
Home

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.

INTEGER-LISTP

Parent topic:  PROGRAMMING
Home

The predicate integer-listp tests whether its argument is a true list of integers.

INTEGERP

Parent topic:  PROGRAMMING
Home

(integerp x) is true if and only if x is an integer.

INTERN

Parent topic:  PROGRAMMING
Home

(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 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)) 

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.

INTERN-IN-PACKAGE-OF-SYMBOL

Parent topic:  PROGRAMMING
Home

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)).

(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"

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|

INTERSECTP-EQ

Parent topic:  PROGRAMMING
Home

See intersectp-equal, which is logically the same function.

(Intersectp-eq x y) has a guard that x and y are lists of symbols.

INTERSECTP-EQUAL

Parent topic:  PROGRAMMING
Home

(Intersectp-equal x y) returns t if x and y have a member in common, else it returns nil. Also see 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.

IO

Parent topic:  PROGRAMMING
Home

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))..)))

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

For convenience, three global variables are bound to these rather tedious channel names:

  *standard-ci*
  *standard-oi*
  *standard-co*

File-names are strings. ACL2 does not support the Common Lisp type pathname.

Here are the signatures of the ACL2 io functions. See 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))

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.

IRRELEVANT-FORMALS

Parent topic:  PROGRAMMING
Home

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))))).

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))))

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))

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)))))

If you need to introduce a function with an irrelevant formal, please explain to the authors why this should be allowed.

KEYWORD-VALUE-LISTP

Parent topic:  PROGRAMMING
Home

(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.

KEYWORDP

Parent topic:  PROGRAMMING
Home

(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.

LAST

Parent topic:  PROGRAMMING
Home

(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.

LENGTH

Parent topic:  PROGRAMMING
Home

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.

LET

Parent topic:  PROGRAMMING
Home

Example LET Form:
(let ((x (* x x))
      (y (* 2 x)))
 (list x y))

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))

General LET Forms:
(let ((var1 term1) ... (varn termn)) body) 
and
(let ((var1 term1) ... (varn termn))
 (declare ...) ... (declare ...)
 body)

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)

((lambda (var1 ... varn)
   (declare ...)
   body)
 term1 ... termn).

General LET* Forms:
(let* ((var1 term1) ... (varn termn)) body) 

The above let* is equivalent to

(let ((var1 term1))
 ...
 (let ((varn termn)) body)...)

Each (vari termi) pair in a let or let* form is called a ``binding'' of vari and the vari are called the ``local variables'' of the let or let*. The common use of let and let* is to save the values of certain expressions (the termi) so that they may be referenced several times in the body without suggesting their recomputation.

Let is part of Common Lisp. See any Common Lisp documentation for more information.

LET*

Parent topic:  PROGRAMMING
Home

Example LET* Form:
(let* ((x (* x x))
       (y (* 2 x)))
 (list x y))

The difference between let and let* is that the former binds its local variables in parallel while the latter binds them sequentially. Thus, in let*, the term evaluated to produce the local value of one of the locally bound variables is permitted to reference any locally bound variable occurring earlier in the binding list and the value so obtained is the newly computed local value of that variable. See let.

Let* is a Common Lisp macro. See any Common Lisp documentation for more information.

LIST

Parent topic:  PROGRAMMING
Home

List is the macro for building a list of objects. For example, (list 5 6 7) returns a list of length 3 whose elements are 5, 6, and 7 respectively. Also see list*.

List is a Common Lisp function. See any Common Lisp documentation for more information.

LIST*

Parent topic:  PROGRAMMING
Home

List* is the Common Lisp macro for building a list of objects from given elements and a tail. For example, (list* 5 6 '(7 8 9)) equals the list '(5 6 7 8 9). Also see list.

List* is a Common Lisp function. See any Common Lisp documentation for more information.

LISTP

Parent topic:  PROGRAMMING
Home

(listp x) is true when x is either a cons pair or is nil.

Listp has no guard, i.e., its guard is t.

Listp is a Common Lisp function. See any Common Lisp documentation for more information.

LOGAND

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logand returns their bitwise logical `and'.

The guard for logand requires its arguments to be integers. Logand is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGANDC1

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logandc1 returns the bitwise logical `and' of the second with the bitwise logical `not' of the first.

The guard for logandc1 requires its arguments to be integers. Logandc1 is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGANDC2

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logandc2 returns the bitwise logical `and' of the first with the bitwise logical `not' of the second.

The guard for logandc2 requires its arguments to be integers. Logandc2 is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGBITP

Parent topic:  PROGRAMMING
Home

For a nonnegative integer i and an integer j, (logbitp i j) is the value of the ith bit in the two's complement representation of j.

(Logbitp i j) has a guard that i is a nonnegative integer and j is an integer.

Logbitp is a Common Lisp function. See any Common Lisp documentation for more information.

LOGCOUNT

Parent topic:  PROGRAMMING
Home

(Logcount x) is the number of ``on'' bits in the two's complement representation of x.

(Logcount x) has a guard of (integerp x).

Logcount is a Common Lisp function. See any Common Lisp documentation for more information.

LOGEQV

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logeqv returns the bitwise logical equivalence of the first with the second.

The guard for logeqv requires its arguments to be integers. Logeqv is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGIOR

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logior returns their bitwise logical inclusive or.

The guard for logior requires its arguments to be integers. Logior is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGNAND

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, lognand returns their bitwise logical `nand'.

The guard for lognand requires its arguments to be integers. Lognand is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGNOR

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, lognor returns the bitwise logical `nor' of the first with the second.

The guard for lognor requires its arguments to be integers. Lognor is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGNOT

Parent topic:  PROGRAMMING
Home

(lognot i) is the two's complement bitwise `not' of the integer i.

Lognot is actually defined by coercing its argument to an integer (see ifix), negating the result, and then subtracting 1.

The guard for lognot requires its argument to be an integer.

Lognot is a Common Lisp function. See any Common Lisp documentation for more information.

LOGORC1

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logorc1 returns the bitwise logical inclusive or of the second with the bitwise logical `not' of the first.

The guard for logorc1 requires its arguments to be integers. Logorc1 is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGORC2

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logorc2 returns the bitwise logical inclusive or of the first with the bitwise logical `not' of the second.

The guard for logorc2 requires its arguments to be integers. Logorc2 is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGTEST

Parent topic:  PROGRAMMING
Home

When integers x and y are viewed in their two's complement representation, (logtest x y) is true if and only if there is some position for which both x and y have a `1' bit in that position.

The guard for logtest requires its arguments to be integers. Logtest is defined in Common Lisp. See any Common Lisp documentation for more information.

LOGXOR

Parent topic:  PROGRAMMING
Home

When integers are viewed in their two's complement representation, logxor returns the bitwise logical exclusive or of the first with the second.

The guard for logxor requires its arguments to be integers. Logxor is defined in Common Lisp. See any Common Lisp documentation for more information.

LOWER-CASE-P

Parent topic:  PROGRAMMING
Home

(Lower-case-p x) is true if and only if x is a lower case character, i.e., a member of the list #A, #B, ..., #Z.

The guard for lower-case-p requires its argument to be a character.

Lower-case-p is a Common Lisp function. See any Common Lisp documentation for more information.