		Search-engine friendly clone of the ACL2 documentation.

Vl-echarlist-from-chars

Vl-echarlist-from-chars-aux

Signature
(vl-echarlist-from-chars-aux x filename line col nrev) → nrev
Arguments: x — Guard (character-listp x).; filename — Guard (stringp filename).; line — Guard (posp line).; col — Guard (natp col).

Definitions and Theorems

Function: vl-echarlist-from-chars-aux

(defun vl-echarlist-from-chars-aux (x filename line col nrev)
  (declare (xargs :stobjs (nrev)))
  (declare (type (integer 0 *) line)
           (type (integer 0 *) col))
  (declare (xargs :guard (and (character-listp x)
                              (stringp filename)
                              (posp line)
                              (natp col))))
  (declare (xargs :split-types t))
  (let ((__function__ 'vl-echarlist-from-chars-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (nrev-fix nrev))
         (echar (make-vl-echar-fast :char (car x)
                                    :filename filename
                                    :line line
                                    :col col))
         (nrev (nrev-push echar nrev))
         ((the character c) (car x))
         (line (if (eql c #\Newline)
                   (the (integer 0 *) (+ 1 line))
                 line))
         (col (if (eql c #\Newline)
                  0
                (the (integer 0 *) (+ 1 col)))))
      (vl-echarlist-from-chars-aux (cdr x)
                                   filename line col nrev))))