NOTE-2-6-GUARDS

ACL2 Version 2.6 Notes on Guard-related Changes 
Major Section:  NOTE-2-6

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