		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)