		Search-engine friendly clone of the ACL2 documentation.

Html-encoding

Vl-html-encode-chars-aux

Print an HTML-encoded character-list.

Signature
(vl-html-encode-chars-aux x col tabsize acc) → (mv new-col new-acc)
Arguments: x — Characters we're transforming into HTML.
Guard (character-listp x).; col — Current column number we're at.
Guard (natp col).; tabsize — Guard (posp tabsize).; acc — Characters being accumulated in reverse order.
Returns: new-col — Updated column number.
Type (natp new-col).; new-acc — Updated accumulator with the HTML encoding of X.
Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: vl-html-encode-chars-aux

(defun vl-html-encode-chars-aux (x col tabsize acc)
  (declare (xargs :guard (and (character-listp x)
                              (natp col)
                              (posp tabsize))))
  (let ((__function__ 'vl-html-encode-chars-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv (lnfix col) acc))
         (char1 (mbe :logic (char-fix (car x))
                     :exec (car x)))
         (acc (vl-html-encode-push char1 col tabsize acc))
         (col (vl-html-encode-next-col char1 col tabsize)))
      (vl-html-encode-chars-aux (cdr x)
                                col tabsize acc))))

Theorem: natp-of-vl-html-encode-chars-aux.new-col

(defthm natp-of-vl-html-encode-chars-aux.new-col
  (b* (((mv ?new-col ?new-acc)
        (vl-html-encode-chars-aux x col tabsize acc)))
    (natp new-col))
  :rule-classes :type-prescription)

Theorem: character-listp-of-vl-html-encode-chars-aux.new-acc

(defthm character-listp-of-vl-html-encode-chars-aux.new-acc
  (implies (character-listp acc)
           (b* (((mv ?new-col ?new-acc)
                 (vl-html-encode-chars-aux x col tabsize acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)

Theorem: vl-html-encode-chars-aux-of-make-character-list-x

(defthm vl-html-encode-chars-aux-of-make-character-list-x
  (equal (vl-html-encode-chars-aux (make-character-list x)
                                   col tabsize acc)
         (vl-html-encode-chars-aux x col tabsize acc)))

Theorem: vl-html-encode-chars-aux-charlisteqv-congruence-on-x

(defthm vl-html-encode-chars-aux-charlisteqv-congruence-on-x
  (implies
       (str::charlisteqv x x-equiv)
       (equal (vl-html-encode-chars-aux x col tabsize acc)
              (vl-html-encode-chars-aux x-equiv col tabsize acc)))
  :rule-classes :congruence)

Theorem: vl-html-encode-chars-aux-of-nfix-col

(defthm vl-html-encode-chars-aux-of-nfix-col
  (equal (vl-html-encode-chars-aux x (nfix col)
                                   tabsize acc)
         (vl-html-encode-chars-aux x col tabsize acc)))

Theorem: vl-html-encode-chars-aux-nat-equiv-congruence-on-col

(defthm vl-html-encode-chars-aux-nat-equiv-congruence-on-col
  (implies
       (acl2::nat-equiv col col-equiv)
       (equal (vl-html-encode-chars-aux x col tabsize acc)
              (vl-html-encode-chars-aux x col-equiv tabsize acc)))
  :rule-classes :congruence)

Theorem: vl-html-encode-chars-aux-of-pos-fix-tabsize

(defthm vl-html-encode-chars-aux-of-pos-fix-tabsize
  (equal (vl-html-encode-chars-aux x col (pos-fix tabsize)
                                   acc)
         (vl-html-encode-chars-aux x col tabsize acc)))

Theorem: vl-html-encode-chars-aux-pos-equiv-congruence-on-tabsize

(defthm vl-html-encode-chars-aux-pos-equiv-congruence-on-tabsize
  (implies
       (acl2::pos-equiv tabsize tabsize-equiv)
       (equal (vl-html-encode-chars-aux x col tabsize acc)
              (vl-html-encode-chars-aux x col tabsize-equiv acc)))
  :rule-classes :congruence)