Note-2-6-guards
ACL2 Version 2.6 Notes on Guard-related Changes
When you declare that a function treats certain formals as
:stobjs, the guard of the function is automatically
extended to include the corresponding stobj-recognizer calls. For example, if
a definition includes (declare (xargs :stobjs (ST))) then the guard of
the function is changed by the addition of the conjunct (ST-P ST).
One impact of this is that if you use the built-in ACL2 state as a
formal parameter of a function, (STATE-P STATE) is added to the guard.
This may introduce a guard where there was none in previous versions of the
system. In older versions, therefore, no attempt would be made to verify-guards, while in the new version, we would attempt guard verification.
You may wish to add (declare (xargs :verify-guards nil)) to such
definitions.
A related change affects users who do not use stobjs or state. In
previous versions of the system — as now — a type declaration
extended the guard you provided explicitly. Thus, if you wrote (declare
(type integer n)) then (INTEGERP n) was added to your guard. This is
still the case and :stobjs recognizers are similarly added. But in older
versions of the system we ``added'' the conjuncts without checking whether
they were already present in the guard you provided. This sometimes produced
such guards as (and (integerp n) (integerp n)) where the first was
produced by your type declaration and the second was your :guard.
We now eliminate redundant conjuncts; this may rearrange the order of the
conjuncts.
The guard conjectures for functions using stobjs have been simplified
somewhat by taking advantage of the syntactic restrictions checked for
single-threaded objects.
The following functions have been modified so that character and string
arguments are restricted to standard characters. (See standard-char-p
and see standard-char-listp.)
upper-case-p lower-case-p char-upcase char-downcase string-downcase1 string-downcase
string-upcase1 string-upcase char-equal
string-equal1 string-equal
Also, function standard-string-alistp replaces function
string-alistp, with concomitant changes in the guard to assoc-string-equal, and in variable *acl2-exports*. Also, lemma
standard-string-alistp-forward-to-alistp replaces lemma
string-alistp-forward-to-alistp. There is a new lemma
standard-char-p-nth, which has also been added to
*acl2-exports*.
The guard had been inadvertently omitted from the definition of the
function substitute (and its subroutine substitute-ac). This
omission has been corrected; also, the guard is slightly stronger than the
documentation had claimed (and that has been corrected).
