		Search-engine friendly clone of the ACL2 documentation.

Html-encoding

Html-encode-chars-aux

Convert a character list into HTML. Outputs to an accumulator. Tracks the column number to handle tab characters.

Signature
(html-encode-chars-aux x col tabsize acc) → (mv new-col new-acc)
Arguments: x — The characters to convert.
Guard (character-listp x).; col — Current column number.
Guard (natp col).; tabsize — Width of tab characters.
Guard (posp tabsize).; acc — Accumulator for output characters, reverse order.
Returns: new-col — Updated column number after printing x.
Type (natp new-col).; new-acc — Updated output.
Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: html-encode-chars-aux

(defun html-encode-chars-aux (x col tabsize acc)
  (declare (xargs :guard (and (character-listp x)
                              (natp col)
                              (posp tabsize))))
  (declare (type unsigned-byte col tabsize))
  (declare (xargs :split-types t))
  (let ((acl2::__function__ 'html-encode-chars-aux))
    (declare (ignorable acl2::__function__))
    (b* (((when (atom x)) (mv (lnfix col) acc))
         (acc (html-encode-push (car x)
                                col tabsize acc))
         (col (html-encode-next-col (car x)
                                    col tabsize)))
      (html-encode-chars-aux (cdr x)
                             col tabsize acc))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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