Major Section: PROGRAMMING
See cw for an introduction to the comment window and the usual way to print it.
Function fmt-to-comment-window is identical to fmt1 (see fmt),
except that the channel is in essence *standard-co* and the ACL2
state is neither an input nor an output.
General Form: (fmt-to-comment-window fmt-string alist col evisc-tuplewhere these arguments are as desribed for
fmt1; see fmt.
:(str alist col co-channel state evisc) => (mv col state)
Major Section: PROGRAMMING
See 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
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
Major Section: PROGRAMMING
(Hard-error 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.
Hard-error has a guard of t. Also see illegal for a
similar capability which however has a guard of nil that supports
static checking using guard verification, rather than using dynamic
(run-time) checking. This distinction is illustrated elsewhere:
see prog2$ for examples.
Semantically, hard-error ignores its arguments and always returns
nil. But if a call (hard-error ctx str alist) is encountered
during evaluation, then the string str is printed using the
association list alist (as in fmt), after which evaluation halts
immediately. Here is a trivial, contrived example.
ACL2 !>(cons 3 (hard-error 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))))
HARD ACL2 ERROR in MY-CONTEXT: Printing 4: four
ACL2 Error in TOP-LEVEL: Evaluation aborted.
ACL2 !>
Major Section: PROGRAMMING
(Identity x) equals x; what else can we say?
Identity is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(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.
Major Section: PROGRAMMING
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).
Major Section: PROGRAMMING
Ifix simply returns any integer argument unchanged, returning 0
on a non-integer argument. Also see nfix, see rfix,
see realfix and see fix for analogous functions that coerce to
a natural number, a rational number, a real, and a number,
respectively.
Ifix has a guard of t.
Major Section: PROGRAMMING
(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, and see prog2$ for an
example of how to use a related function, hard-error
(see hard-error).
The difference between illegal and hard-error is that the former
has a guard of nil while the latter has a guard ot t. Thus,
you may want to use illegal rather than hard-error when you intend
to do guard verification at some point, and you expect the guard
to guarantee that the illegal call is never executed.
See prog2$ for an example.
Major Section: PROGRAMMING
Completion Axiom:
(equal (imagpart x)
(if (acl2-numberp x)
(imagpart x)
0))
Guard for (imagpart x):
(acl2-numberp x)
Major Section: PROGRAMMING
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).
Major Section: PROGRAMMING
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.
Major Section: PROGRAMMING
(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.
Major Section: PROGRAMMING
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.
Major Section: PROGRAMMING
The predicate integer-listp tests whether its argument is a true
list of integers.
Major Section: PROGRAMMING
(integerp x) is true if and only if x is an integer.
Major Section: PROGRAMMING
(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))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.
Major Section: PROGRAMMING
Completion 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|
Major Section: PROGRAMMING
See intersectp-equal, which is logically the same function.
(Intersectp-eq x y) has a guard that x and y are lists of
symbols.
Major Section: PROGRAMMING
(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.
Major Section: PROGRAMMING
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 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-0All 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 names, formals and output descriptions of the ACL2 io functions.
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))The ``formatting'' functions are particularly useful; see fmt and see cw. In particular,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)) (cw string arg0 arg1 ... argn) nil)
cw prints to a
``comment window'' and does not involve the ACL2 state, so many may
find it easier to use than fmt and its variants.
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.
By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp. As with Common Lisp,
ACL2 supports printing in a "downcase" mode, where symbols are
printed in lower case. Many printing functions (some details below)
print characters in lower case for a symbol when the ACL2 state
global variable print-case has value :downcase and vertical bars
are not necessary for printing that symbol. (Thus, this state global
functions in complete analogy to the Common Lisp global
*print-case*.) The value print-case is returned by
(acl2-print-case), and may be set using the macro
set-acl2-print-case (which returns state), as follows.
:set-acl2-print-case :upcase ; Default printing
(set-acl2-print-case :upcase) ; Same as above
:set-acl2-print-case :downcase ; Print symbols in lower case when
; vertical bars are not required
(set-acl2-print-case :downcase) ; Same as above
The ACL2 user can expect that the :downcase setting will have an
effect for formatted output (see fmt and see fms) when the
directives are ~p, ~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and not for built-in
function print-object$. For other printing functions, the effect of
:downcase is unspecified.
Major Section: PROGRAMMING
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 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 (p 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 (p 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 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.
Major Section: PROGRAMMING
(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.
Major Section: PROGRAMMING
(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.
cons (not element) of a list
Major Section: PROGRAMMING
(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.
Major Section: PROGRAMMING
Len returns the length of a list.
A Common Lisp function that is appropriate for both strings and
proper lists is length; see length. The guard for len is t.
Major Section: PROGRAMMING
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.
Major Section: PROGRAMMING
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 variables (not necessarily distinct), the
termi are terms involving only variables bound in the environment
containing the let* and those varj such that j<i, 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 either
some subsequent termj or in body. Note that let* does not permit
the inclusion of declare forms.
The above let* is equivalent to
(let ((var1 term1)) ... (let ((varn termn)) body)...)Thus, the
termi are evaluated successively and after each
evaluation the corresponding vali is bound to the value of termi.
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.
Major Section: PROGRAMMING
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 8). See let for a discussion
of both let and let*, or read on for a briefer discussion.
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.
Major Section: PROGRAMMING
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 defined in Common Lisp. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
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.
Major Section: PROGRAMMING
(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.