		Search-engine friendly clone of the ACL2 documentation.

Html-encoding

Html-encode-string-aux

Core of converting strings into HTML, output to an accumulator.

Signature
(html-encode-string-aux x n xl col tabsize acc) → (mv new-col new-acc)
Arguments: x — String we're encoding.
Guard (stringp x).; n — Current position in x. Should typically start as 0.
Guard (natp n).; xl — Guard (eql xl (length x)).; col — Current column we're printing to.
Guard (natp col).; tabsize — Guard (posp tabsize).
Returns: new-col — Type (natp new-col).; new-acc — Type (character-listp new-acc), given (character-listp acc).

This is similar to html-encode-chars-aux, but encodes part of a the string x instead of a character list.

Definitions and Theorems

Function: html-encode-string-aux

(defun html-encode-string-aux (x n xl col tabsize acc)
 (declare (xargs :guard (and (stringp x)
                             (natp n)
                             (natp col)
                             (posp tabsize)
                             (eql xl (length x)))))
 (declare (type string x)
          (type unsigned-byte n xl col tabsize))
 (declare (xargs :split-types t :guard (<= n xl)))
 (let ((acl2::__function__ 'html-encode-string-aux))
  (declare (ignorable acl2::__function__))
  (mbe
      :logic
      (html-encode-chars-aux (nthcdr n (explode x))
                             col tabsize acc)
      :exec
      (b* (((when (mbe :logic (zp (- (length (str-fix x)) (nfix n)))
                       :exec (eql n xl)))
            (mv (lnfix col) acc))
           (char1 (char x n))
           (acc (html-encode-push char1 col tabsize acc))
           (col (html-encode-next-col char1 col tabsize)))
        (html-encode-string-aux x (+ 1 (lnfix n))
                                xl col tabsize acc)))))

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

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

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

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

Theorem: html-encode-string-aux-of-str-fix-x

(defthm html-encode-string-aux-of-str-fix-x
  (equal (html-encode-string-aux (str-fix x)
                                 n xl col tabsize acc)
         (html-encode-string-aux x n xl col tabsize acc)))

Theorem: html-encode-string-aux-streqv-congruence-on-x

(defthm html-encode-string-aux-streqv-congruence-on-x
 (implies
      (streqv x x-equiv)
      (equal (html-encode-string-aux x n xl col tabsize acc)
             (html-encode-string-aux x-equiv n xl col tabsize acc)))
 :rule-classes :congruence)

Theorem: html-encode-string-aux-of-nfix-n

(defthm html-encode-string-aux-of-nfix-n
  (equal (html-encode-string-aux x (nfix n)
                                 xl col tabsize acc)
         (html-encode-string-aux x n xl col tabsize acc)))

Theorem: html-encode-string-aux-nat-equiv-congruence-on-n

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

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

(defthm html-encode-string-aux-of-nfix-col
  (equal (html-encode-string-aux x n xl (nfix col)
                                 tabsize acc)
         (html-encode-string-aux x n xl col tabsize acc)))

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

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

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

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

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

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