		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Scan-backward-for-non-whitespace

Signature
(scan-backward-for-non-whitespace idx x) → result-idx
Arguments: idx — Guard (natp idx).; x — Guard (stringp x).
Returns: result-idx — Type (natp result-idx).

Definitions and Theorems

Function: scan-backward-for-non-whitespace

(defun scan-backward-for-non-whitespace (idx x)
  (declare (xargs :guard (and (natp idx) (stringp x))))
  (declare (xargs :guard (<= idx (length x))))
  (let ((__function__ 'scan-backward-for-non-whitespace))
    (declare (ignorable __function__))
    (b* (((when (zp idx)) (length x))
         ((unless (mbt (< 0 (length x)))) 0)
         (idx (mbe :logic (1- (min idx (length x)))
                   :exec (1- idx)))
         ((when (not (vl-whitespace-p (char x idx))))
          (lnfix idx)))
      (scan-backward-for-non-whitespace idx x))))

Theorem: natp-of-scan-backward-for-non-whitespace

(defthm natp-of-scan-backward-for-non-whitespace
  (b* ((result-idx (scan-backward-for-non-whitespace idx x)))
    (natp result-idx))
  :rule-classes :type-prescription)

Theorem: scan-backward-for-non-whitespace-upper-bound

(defthm scan-backward-for-non-whitespace-upper-bound
  (b* ((?result-idx (scan-backward-for-non-whitespace idx x)))
    (<= result-idx (length x)))
  :rule-classes :linear)

Theorem: scan-backward-for-non-whitespace-finds-non-whitespace

(defthm scan-backward-for-non-whitespace-finds-non-whitespace
  (b* ((?result-idx (scan-backward-for-non-whitespace idx x)))
    (implies (not (equal result-idx (length x)))
             (not (vl-whitespace-p (char x result-idx))))))

Theorem: scan-backward-for-non-whitespace-bound-when-non-whitespace-exists

(defthm
  scan-backward-for-non-whitespace-bound-when-non-whitespace-exists
  (b* ((?result-idx (scan-backward-for-non-whitespace idx x)))
    (implies (and (< (nfix nw-idx) (length x))
                  (not (vl-whitespace-p (char x nw-idx)))
                  (< (nfix nw-idx) (nfix idx)))
             (and (<= (nfix nw-idx) result-idx)
                  (< result-idx (length x))))))

Theorem: scan-backward-for-non-whitespace-gte-than-scan-for-non-whitespace

(defthm
  scan-backward-for-non-whitespace-gte-than-scan-for-non-whitespace
  (<= (scan-for-non-whitespace 0 x)
      (scan-backward-for-non-whitespace (length x)
                                        x))
  :rule-classes :linear)