		Search-engine friendly clone of the ACL2 documentation.

Extended-characters

Vl-echarlist-from-chars

Transform an ordinary character list into a vl-echarlist-p.

Signature
(vl-echarlist-from-chars x &key (filename '"[internal character list]") (line '1) (col '0)) → ans
Arguments: x — The characters to convert.
Guard (character-listp x).; filename — Filename for every echar we build.
Guard (stringp filename).; line — Starting line.
Guard (posp line).; col — Starting column.
Guard (natp col).
Returns: ans — Type (vl-echarlist-p ans).

Definitions and Theorems

Function: vl-echarlist-from-chars-fn

(defun
 vl-echarlist-from-chars-fn
 (x filename line col)
 (declare (xargs :guard (and (character-listp x)
                             (stringp filename)
                             (posp line)
                             (natp col))))
 (let
  ((__function__ 'vl-echarlist-from-chars))
  (declare (ignorable __function__))
  (mbe
   :logic (b* (((when (atom x)) nil)
               (line (pos-fix line))
               (col (nfix col))
               (x1 (char-fix (car x)))
               (echar (make-vl-echar-fast :char x1
                                          :filename filename
                                          :line line
                                          :col col))
               (line (if (eql x1 #\Newline) (+ 1 line) line))
               (col (if (eql x1 #\Newline) 0 (+ 1 col))))
              (cons echar
                    (vl-echarlist-from-chars-fn (cdr x)
                                                filename line col)))
   :exec
   (if
    (atom x)
    nil
    (with-local-nrev
         (vl-echarlist-from-chars-aux x filename line col nrev))))))

Theorem: vl-echarlist-p-of-vl-echarlist-from-chars

(defthm vl-echarlist-p-of-vl-echarlist-from-chars
        (b* ((ans (vl-echarlist-from-chars-fn x filename line col)))
            (vl-echarlist-p ans))
        :rule-classes :rewrite)

Theorem: true-listp-of-vl-echarlist-from-chars-fn

(defthm
     true-listp-of-vl-echarlist-from-chars-fn
     (true-listp (vl-echarlist-from-chars-fn x filename line col))
     :rule-classes :type-prescription)

Theorem: vl-echarlist->chars-of-vl-echarlist-from-chars-fn

(defthm
  vl-echarlist->chars-of-vl-echarlist-from-chars-fn
  (implies
       (force (character-listp x))
       (equal (vl-echarlist->chars
                   (vl-echarlist-from-chars-fn x filename line col))
              x)))

Theorem: vl-echarlist-from-chars-aux-removal

(defthm
 vl-echarlist-from-chars-aux-removal
 (implies
   (and (character-listp x)
        (natp col)
        (posp line))
   (equal
        (vl-echarlist-from-chars-aux x filename line col acc)
        (append acc
                (vl-echarlist-from-chars-fn x filename line col)))))

Theorem: vl-echarlist-from-chars-fn-of-make-character-list-x

(defthm vl-echarlist-from-chars-fn-of-make-character-list-x
        (equal (vl-echarlist-from-chars-fn (make-character-list x)
                                           filename line col)
               (vl-echarlist-from-chars-fn x filename line col)))

Theorem: vl-echarlist-from-chars-fn-charlisteqv-congruence-on-x

(defthm
 vl-echarlist-from-chars-fn-charlisteqv-congruence-on-x
 (implies
     (str::charlisteqv x x-equiv)
     (equal (vl-echarlist-from-chars-fn x filename line col)
            (vl-echarlist-from-chars-fn x-equiv filename line col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-chars-fn-of-str-fix-filename

(defthm vl-echarlist-from-chars-fn-of-str-fix-filename
        (equal (vl-echarlist-from-chars-fn x (str-fix filename)
                                           line col)
               (vl-echarlist-from-chars-fn x filename line col)))

Theorem: vl-echarlist-from-chars-fn-streqv-congruence-on-filename

(defthm
 vl-echarlist-from-chars-fn-streqv-congruence-on-filename
 (implies
     (streqv filename filename-equiv)
     (equal (vl-echarlist-from-chars-fn x filename line col)
            (vl-echarlist-from-chars-fn x filename-equiv line col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-chars-fn-of-pos-fix-line

(defthm vl-echarlist-from-chars-fn-of-pos-fix-line
        (equal (vl-echarlist-from-chars-fn x filename (pos-fix line)
                                           col)
               (vl-echarlist-from-chars-fn x filename line col)))

Theorem: vl-echarlist-from-chars-fn-pos-equiv-congruence-on-line

(defthm
 vl-echarlist-from-chars-fn-pos-equiv-congruence-on-line
 (implies
     (acl2::pos-equiv line line-equiv)
     (equal (vl-echarlist-from-chars-fn x filename line col)
            (vl-echarlist-from-chars-fn x filename line-equiv col)))
 :rule-classes :congruence)

Theorem: vl-echarlist-from-chars-fn-of-nfix-col

(defthm
     vl-echarlist-from-chars-fn-of-nfix-col
     (equal (vl-echarlist-from-chars-fn x filename line (nfix col))
            (vl-echarlist-from-chars-fn x filename line col)))

Theorem: vl-echarlist-from-chars-fn-nat-equiv-congruence-on-col

(defthm
 vl-echarlist-from-chars-fn-nat-equiv-congruence-on-col
 (implies
     (acl2::nat-equiv col col-equiv)
     (equal (vl-echarlist-from-chars-fn x filename line col)
            (vl-echarlist-from-chars-fn x filename line col-equiv)))
 :rule-classes :congruence)

Subtopics

Vl-echarlist-from-chars-aux