		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