(put-assoc-equal name val alist) requires that alist
is an alistp.
Major Section: PROGRAMMING
(Put-assoc-equal name val alist) returns an alist that is the same
as the list alist, except that the first pair in alist with a
car of name is replaced by (cons name val), if there is
one. If there is no such pair, then (cons name val) is added at
the end.
The guard of (put-assoc-equal name val alist) requires that alist
is an alistp.
eql as test
Major Section: PROGRAMMING
(Rassoc x alist) is similar to (assoc x alist), the difference
being that it looks for the first pair in the given alist whose
cdr, rather than car, is eql to x. See assoc.
The guard of rassoc requires its second argument to be an alist,
and in addition, that either its first argument is eqlablep or
else all second components of pairs belonging to the second argument
are eqlablep. See eqlablep.
Rassoc is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
The predicate rational-listp tests whether its argument is a true
list of rational numbers.
Major Section: PROGRAMMING
(rationalp x) is true if and only if x is an rational
number.
Major Section: PROGRAMMING
For most ACL2 users, this is a macro abbreviating rationalp. In
ACL2(r) (see real), this macro abbreviates the predicate realp,
which holds for real numbers as well (including rationals). Most
ACL2 users can ignore this macro and use rationalp instead,
but many books in the ACL2 distribution use real/rationalp so that
these books will be suitable for ACL2(r) as well.
Major Section: PROGRAMMING
Realfix simply returns any real number argument unchanged,
returning 0 on a non-real argument. Also see nfix,
see ifix, see rfix, and see fix for analogous functions
that coerce to a natural number, an integer, a rational, and a
number, respectively.
Realfix has a guard of t.
Major Section: PROGRAMMING
Completion Axiom:
(equal (realpart x)
(if (acl2-numberp x)
(realpart x)
0))
Guard for (realpart x):
(acl2-numberp x)
Major Section: PROGRAMMING
ACL2 does not in general allow the redefinition of functions because
logical inconsistency can result: previously stored theorems can be
rendered invalid if the axioms defining the functions involved are
changed. However, to permit prototyping of both :program and
:logic mode systems, ACL2 permits redefinition if the user has
accepted logical responsibility for the consequences by setting
ld-redefinition-action to an appropriate non-nil value. The
refusal of ACL2 to support the unrestricted redefinition of
:program mode functions may appear somewhat capricious. After
all, what are the logical consequences of changing a definition if
no axioms are involved?
Three important points should be made before we discuss redefinition further.
The first is that ACL2 does support redefinition (of both
:program and :logic functions) when
ld-redefinition-action is non-nil.
The second is that a ``redefinition'' that does not change the mode,
formals or body of a function is considered redundant and is
permitted even when ld-redefinition-action is nil. We
recognize and permit redundant definitions because it is not
uncommon for two distinct books to share identical function
definitions. When determining whether the body of a function is
changed by a proposed redefinition, we actually compare the
untranslated versions of the two bodies. See term. For
example, redundancy is not recognized if the old body is (list a b)
and the new body is (cons a (cons b nil)). We use the
untranslated bodies because of the difficulty of translating the new
body in the presence of the old syntactic information, given the
possibility that the redefinition might attempt to change the
signature of the function, i.e., the number of formals, the
number of results, or the position of single-threaded objects in either.
The third important point is that a ``redefinition'' that preserves
the formals and body but changes the mode from :program to
:logic is permitted even when ld-redefinition-action is
nil. That is what verify-termination does.
This note addresses the temptation to allow redefiniton of
:program functions in situations other than the three
described above. Therefore, suppose ld-redefinition-action is
nil and consider the cases.
Case 1. Suppose the new definition attempts to change the formals
or more generally the signature of the function. Accepting
such a redefinition would render ill-formed other :program
functions which call the redefined function. Subsequent attempts to
evaluate those callers could arbitrarily damage the Common Lisp
image. Thus, redefinition of :program functions under these
circumstances requires the user's active approval, as would be
sought with ld-redefinition-action '(:query . :overwrite).
Case 2. Suppose the new definition attempts to change the body
(even though it preserves the signature). At one time we
believed this was acceptable and ACL2 supported the quiet
redefinition of :program mode functions in this circumstance.
However, because such functions can be used in macros and redundancy
checking is based on untranslated bodies, this turns out to be
unsound! It is therefore now prohibited. We illustrate such an
unsoundness below. Let foo-thm1.lisp be a book with the
following contents.
(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm1 (iff (foo x) x) :rule-classes nil)Note that the macro form
(p x) translates to (if x t nil).
The :program function p1 is used to generate this
translation. The function foo is defined so that (foo x) is
(p x) and a theorem about foo is proved, namely, that (foo x)
is true iff x is true.
Now let foo-thm2.lisp be a book with the following contents.
(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)In this book, the
:program function p1 is defined so that
(p x) means just the negation of what it meant in the first book,
namely, (if x nil t). The function foo is defined identically
-- more precisely, the untranslated body of foo is identical
in the two books, but because of the difference between the two
versions of the the :program function p1 the axioms
defining the two foos are different. In the second book we prove
the theorem that (foo x) is true iff x is nil.
Now consider what would happen if the signature-preserving
redefinition of :program functions were permitted and these
two books were included. When the second book is included the
redefinition of p1 would be permitted since the signature is
preserved and p1 is just a :program. But then when the
redefinition of foo is processed it would be considered redundant
and thus be permitted. The result would be a logic in which it was
possible to prove that (foo x) is equivalent to both x and
(not x). In particular, the following sequence leads to a proof
of nil:
(include-book "foo-thm1")
(include-book "foo-thm2")
(thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))
It might be possible to loosen the restrictions on the redefinition
of :program functions by allowing signature-preserving
redefinition of :program functions not involved in macro
definitions. Alternatively, we could implement definition
redundancy checking based on the translated bodies of functions
(though that is quite problematic). Barring those two changes, we
believe it is necessary simply to impose the same restrictions on
the redefinition of :program mode functions as we do on
:logic mode functions.
truncate
Major Section: PROGRAMMING
ACL2 !>(rem 14 3) 2 ACL2 !>(rem -14 3) -2 ACL2 !>(rem 14 -3) 2 ACL2 !>(rem -14 -3) -2 ACL2 !>(rem -15 -3) 0 ACL2 !>
(Rem i j) is that number k that (* j (truncate i j)) added
to k equals i.
The guard for (rem i j) requires that i and j are rational
(real, in ACL2(r)) numbers and j is non-zero.
Rem is a Common Lisp function. See any Common Lisp documentation
for more information.
eql
Major Section: PROGRAMMING
(remove x l) is l if x is not a member of l, else is the
result of removing all occurrences of x from l.
The guard for (remove x l) requires l to be a true list and
moreover, either x is eqlablep or all elements of l are
eqlablep.
Remove is a Common Lisp function. See any Common Lisp
documentation for more information. Note that we do not allow
keyword arguments (such as test) in ACL2 functions, in
particular, in remove.
eql) a list
Major Section: PROGRAMMING
Remove-duplicates returns the result of deleting duplicate
elements from the beginning of the given string or true list, i.e.,
leaving the last element in place. For example,
(remove-duplicates '(1 2 3 2 4))is equal to
'(1 3 2 4).
The guard for Remove-duplicates requires that its argument is a
string or a true-list of eqlablep objects. It uses the function
eql to test for equality between elements of its argument.
Remove-duplicates is a Common Lisp function. See any Common Lisp
documentation for more information. Note that we do not allow
keyword arguments (such as test) in ACL2 functions, in
particular, in remove-duplicates. But
see remove-duplicates-equal, which is similar but uses the
function equal to test for duplicate elements.
Major Section: PROGRAMMING
Remove-duplicates-equal is the same as remove-duplicates,
except that its argument must be a true list (not a string), and
equal is used to check membership rather than eql.
See remove-duplicates.
The guard for Remove-duplicates-equal requires that its argument
is a true list. Note that unlike remove-duplicates, it does not
allow string arguments.
cdr) of the list
Major Section: PROGRAMMING
In the logic, rest is just a macro for cdr.
Rest is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Revappend x y) concatenates the reverse of the list x to y,
which is also typically a list.
The following theorem characterizes this English description.
(equal (revappend x y)
(append (reverse x) y))
Hint: This lemma follows immediately from the definition of reverse
and the following lemma.
(defthm revappend-append
(equal (append (revappend x y) z)
(revappend x (append y z))))
The guard for (revappend x y) requires that x is a true list.
Revappend is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Reverse x) is the result of reversing the order of the
elements of the list or string x.
The guard for reverse requires that its argument is a true list
or a string.
Reverse is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
Rfix simply returns any rational number argument unchanged,
returning 0 on a non-rational argument. Also see nfix,
see ifix, see realfix, and see fix for analogous
functions that coerce to a natural number, an integer, a real, and a
number, respectively.
Rfix has a guard of t.
Major Section: PROGRAMMING
Example Forms: ACL2 !>(round 14 3) 5 ACL2 !>(round -14 3) -5 ACL2 !>(round 14 -3) -5 ACL2 !>(round -14 -3) 5 ACL2 !>(round 13 3) 4 ACL2 !>(round -13 3) -4 ACL2 !>(round 13 -3) -4 ACL2 !>(round -13 -3) 4 ACL2 !>(round -15 -3) 5 ACL2 !>(round 15 -2) -8
(Round i j) is the result of taking the quotient of i and j
and rounding off to the nearest integer. When the quotient is
exactly halfway between consecutive integers, it rounds to the even
one.
The guard for (round i j) requires that i and j are
rational (real, in ACL2(r)) numbers and j is non-zero.
Round is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
Major Section: PROGRAMMING
(Set-difference-equal x y) equals a list whose members
(see member-equal) contains the members of x that are not
members of y. More precisely, the resulting list is the same as
one gets by deleting the members of y from x, leaving the
remaining elements in the same order as they had in x.
The guard for set-difference-equal requires both arguments to be
true lists. Essentially, set-difference-equal has the same
functionality as the Common Lisp function set-difference, except
that it uses the equal function to test membership rather than
eql. However, we do not include the function set-difference
in ACL2, because the Common Lisp language does not specify the order
of the elements in the list that it returns.
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
Major Section: PROGRAMMING
(Signum x) is 0 if x is 0, -1 if x is negative,
and is 1 otherwise.
The guard for signum requires its argument to be rational (real, in
ACL2(r)) number.
Signum is a Common Lisp function. See any Common Lisp
documentation for more information.
From ``Common Lisp the Language'' page 206, we see a definition of
signum in terms of abs. As explained elsewhere
(see abs), the guard for abs requires its argument to be a
rational (real, in ACL2(r)) number; hence, we make the same
restriction for signum.
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
Major Section: PROGRAMMING
(standard-char-listp x) is true if and only if x is a
null-terminated list all of whose members are standard characters.
See standard-char-p.
Standard-char-listp has a guard of t.
Major Section: PROGRAMMING
(Standard-char-p x) is true if and only if x is a ``standard''
character, i.e., a member of the list *standard-chars*. This
list includes #Newline and #Space characters, as well as the usual
punctuation and alphanumeric characters.
Standard-char-p has a guard requiring its argument to be a
character.
Standard-char-p is a Common Lisp function. See any Common Lisp
documentation for more information.
ld prints
Major Section: PROGRAMMING
Standard-co is an ld special (see ld). The accessor is
(standard-co state) and the updater is (set-standard-co val state).
Standard-co must be an open character output channel. It is to this
channel that ld prints the prompt, the form to be evaluated, and the
results. The event commands such as defun, defthm, etc., which
print extensive commentary do not print to standard-co but rather to
a different channel, proofs-co, so that you may redirect this
commentary while still interacting via standard-co.
See proofs-co.
``Standard-co'' stands for ``standard character output.'' The
initial value of standard-co is the same as the value of
*standard-co* (see *standard-co*).
Major Section: PROGRAMMING
Standard-oi is an ld special (see ld). The accessor is
(standard-oi state) and the updater is (set-standard-oi val state).
Standard-oi must be an open object input channel, a true list of
objects, or a list of objects whose last cdr is an open object input
channel. It is from this source that ld takes the input forms to
process. When ld is called, if the value specified for standard-oi
is a string or a list of objects whose last cdr is a string, then ld
treats the string as a file name and opens an object input channel
from that file. The channel opened by ld is closed by ld upon
termination.
``Standard-oi'' stands for ``standard object input.'' The
read-eval-print loop in ld reads the objects in standard-oi and
treats them as forms to be evaluated. The initial value of
standard-oi is the same as the value of *standard-oi*
(see *standard-oi*).
Major Section: PROGRAMMING
(String x) coerces x to a string. If x is already a
string, then it is returned unchanged; if x is a symbol, then its
symbol-name is returned; and if x is a character, the
corresponding one-character string is returned.
The guard for string requires its argument to be a string, a
symbol, or a character.
String is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(String-alistp x) is true if and only if x is a list of pairs
of the form (cons key val) where key is a string.
String-alistp has a guard of t.
Major Section: PROGRAMMING
NOTE: It is probably more efficient to use the Common Lisp function
concatenate in place of string-append. That is,
(string-append str1 str2)is equal to
(concatenate 'string str1 str2).
At any rate, string-append takes two arguments, which are both
strings (if the guard is to be met), and returns a string obtained
concatenating together the characters in the first string followed
by those in the second. See concatenate.
Major Section: PROGRAMMING
For a string x, (string-downcase x) is the result of applying
char-downcase to each character in x.
The guard for string-downcase requires its argument to be a string.
String-downcase is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
For strings str1 and str2, (string-equal str1 str2) is true if
and only str1 and str2 are the same except perhaps for the cases of
their characters.
The guard on string-equal requires that its arguments are strings.
String-equal is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
The predicate string-listp tests whether its argument is a
true-listp of strings.
Major Section: PROGRAMMING
For a string x, (string-upcase x) is the result of applying
char-upcase to each character in x.
The guard for string-upcase requires its argument to be a string.
String-upcase is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(String< str1 str2) is non-nil if and only if the string
str1 precedes the string str2 lexicographically, where
character inequalities are tested using char<. When non-nil,
(string< str1 str2) is the first position (zero-based) at which
the strings differ. Here are some examples.
ACL2 !>(string< "abcd" "abu") 2 ACL2 !>(string< "abcd" "Abu") NIL ACL2 !>(string< "abc" "abcde") 3 ACL2 !>(string< "abcde" "abc") NIL
The guard for string< specifies that its arguments are strings.
String< is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(String<= str1 str2) is non-nil if and only if the string
str1 precedes the string str2 lexicographically or the strings
are equal. When non-nil, (string<= str1 str2) is the first
position (zero-based) at which the strings differ, if they differ,
and otherwise is their common length. See string<.
The guard for string<= specifies that its arguments are strings.
String<= is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(String> str1 str2) is non-nil if and only if str2 precedes
str1 lexicographically. When non-nil, (string> str1 str2)
is the first position (zero-based) at which the strings differ.
See string<.
String> is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(String>= str1 str2) is non-nil if and only if the string
str2 precedes the string str1 lexicographically or the strings
are equal. When non-nil, (string>= str1 str2) is the first
position (zero-based) at which the strings differ, if they differ,
and otherwise is their common length. See string>.
The guard for string>= specifies that its arguments are strings.
String>= is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(stringp x) is true if and only if x is a string.
Major Section: PROGRAMMING
(strip-cars x) is the list obtained by walking through the list
x and collecting up all first components (cars).
This function is implemented in a tail-recursive way, despite its
logical definition.
(strip-cars x) has a guard of (alistp x).
Major Section: PROGRAMMING
(strip-cdrs x) has a guard of (alistp x), and returns the list
obtained by walking through the list x and collecting up all
second components (cdrs). This function is implemented in a
tail-recursive way, despite its logical definition.
Major Section: PROGRAMMING
(Sublis alist tree) is obtained by replacing every leaf of
tree with the result of looking that leaf up in the association
list alist. However, a leaf is left unchanged if it is not found
as a key in alist.
Leaves are lookup up using the function assoc. The guard for
(sublis alist tree) requires (eqlable-alistp alist). This
guard ensures that the guard for assoc will be met for each
lookup generated by sublis.
Sublis is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
For any natural numbers start and end, where start <=
end <= (length seq), (subseq seq start end) is the
subsequence of seq from index start up to, but not including,
index end. End may be nil, which which case it is treated
as though it is (length seq), i.e., we obtain the subsequence of
seq from index start all the way to the end.
The guard for (subseq seq start end) is that seq is a
true list or a string, start and end are integers (except,
end may be nil, in which case it is treated as (length seq)
for ther rest of this discussion), and 0 <= start <=
end <= (length seq).
Subseq is a Common Lisp function. See any Common Lisp
documentation for more information. Note: In Common Lisp the third
argument of subseq is optional, but in ACL2 it is required,
though it may be nil as explained above.
member of one list is a member of the other
Major Section: PROGRAMMING
(Subsetp x y) is true if and only if every member of the list
x is a member of the list y.
Membership is tested using the function member. Thus, the guard
for subsetp requires that its arguments are true lists, and
moreover, at least one satisfies eqlable-listp. This guard
ensures that the guard for member will be met for each call
generated by subsetp.
Subsetp is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Subsetp-equal x y) returns t if every member of x is a
member of y, where membership is tested using member-equal.
The guard for subsetp-equal requires both arguments to be true
lists. Subsetp-equal has the same functionality as the Common Lisp
function subsetp, except that it uses the equal function to
test membership rather than eql.
Major Section: PROGRAMMING
(Subst new old tree) is obtained by substituting new for every
occurence of old in the given tree.
Equality to old is determined using the function eql. The
guard for (subst new old tree) requires (eqlablep old), which
ensures that the guard for eql will be met for each comparison
generated by subst.
Subst is defined in Common Lisp. See any Common Lisp
documentation for more information.
eql as test
Major Section: PROGRAMMING
(Substitute new old seq) is the result of replacing each occurrence
of old in seq, which is a list or a string, with new.
The guard for substitute requires that either seq is a string, or else
seq is a true-listp such that either all of its members are
eqlablep or old is eqlablep.
Substitute is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the test used in
substitute is eql.
Major Section: PROGRAMMING
(symbol-< x y) is non-nil if and only if either the
symbol-name of the symbol x lexicographially precedes the
symbol-name of the symbol y (in the sense of string<) or
else the symbol-names are equal and the symbol-package-name of
x lexicographically precedes that of y (in the same sense).
So for example, (symbol-< 'abcd 'abce) and
(symbol-< 'acl2::abcd 'foo::abce) are true.
The guard for symbol specifies that its arguments are symbols.
Major Section: PROGRAMMING
(Symbol-alistp x) is true if and only if x is a list of pairs
of the form (cons key val) where key is a symbolp.
Major Section: PROGRAMMING
The predicate symbol-listp tests whether its argument is a
true list of symbols.
Major Section: PROGRAMMING
Completion Axiom:
(equal (symbol-name x)
(if (symbolp x)
(symbol-name x)
""))
Guard for (symbol-name x):
(symbolp x)
Major Section: PROGRAMMING
Completion Axiom:
(equal (symbol-package-name x)
(if (symbolp x)
(symbol-package-name x)
""))
Guard for (symbol-package-name x):
(symbolp x)