		Search-engine friendly clone of the ACL2 documentation.

Lexer

Only-whitespace-backward-through-line

Check that the only preceding characters on the line are whitespace.

Signature
(only-whitespace-backward-through-line parstate) → only-whitespace
Arguments: parstate — Guard (parstatep parstate).
Returns: only-whitespace — Type (booleanp only-whitespace).

We begin with the character immediately before the last read character, and check that every character is whitespace until we reach either a new-line or the start of the file.

Since read-char converts all recognized new-line sequences into a single line feed character, we detect new-lines by simply checking for a line feed.

Definitions and Theorems

Function: only-whitespace-backward-through-line-loop

(defun only-whitespace-backward-through-line-loop (i parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (natp i) (parstatep parstate))))
 (declare (xargs :guard (< i (parstate->chars-length parstate))))
 (let ((__function__ 'only-whitespace-backward-through-line-loop))
  (declare (ignorable __function__))
  (b* ((char+pos (parstate->char i parstate))
       (char (char+position->char char+pos)))
    (cond ((utf8-= char 10) t)
          ((or (utf8-= char 32)
               (and (utf8-<= 9 char)
                    (utf8-<= char 12)))
           (if (= (mbe :logic (nfix i)
                       :exec (the unsigned-byte i))
                  0)
               t
             (only-whitespace-backward-through-line-loop (- i 1)
                                                         parstate)))
          (t nil)))))

Theorem: booleanp-of-only-whitespace-backward-through-line-loop

(defthm booleanp-of-only-whitespace-backward-through-line-loop
 (b* ((all-whitespace
           (only-whitespace-backward-through-line-loop i parstate)))
   (booleanp all-whitespace))
 :rule-classes :rewrite)

Function: only-whitespace-backward-through-line

(defun only-whitespace-backward-through-line (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'only-whitespace-backward-through-line))
  (declare (ignorable __function__))
  (b*
   ((chars-read (parstate->chars-read parstate))
    ((when (utf8-= chars-read 1)) t)
    ((when (or (< chars-read 1)
               (<= (parstate->chars-length parstate)
                   chars-read)))
     (raise "Internal error: chars-read index ~x0 out of bound ~x1."
            chars-read
            (parstate->chars-length parstate))))
   (only-whitespace-backward-through-line-loop (- chars-read 2)
                                               parstate))))

Theorem: booleanp-of-only-whitespace-backward-through-line

(defthm booleanp-of-only-whitespace-backward-through-line
  (b* ((only-whitespace
            (only-whitespace-backward-through-line parstate)))
    (booleanp only-whitespace))
  :rule-classes :rewrite)