Convenient routine for HTML encoding a string.
Function:
(defun vl-html-encode-string (x tabsize) (declare (xargs :guard (and (stringp x) (posp tabsize)))) (declare (type string x) (type unsigned-byte tabsize)) (declare (xargs :split-types t)) (let ((__function__ 'vl-html-encode-string)) (declare (ignorable __function__)) (b* (((mv ?col acc) (vl-html-encode-string-aux x 0 (length x) 0 tabsize nil))) (str::rchars-to-string acc))))
Theorem:
(defthm stringp-of-vl-html-encode-string (b* ((html-x (vl-html-encode-string x tabsize))) (stringp html-x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-html-encode-string-of-str-fix-x (equal (vl-html-encode-string (str-fix x) tabsize) (vl-html-encode-string x tabsize)))
Theorem:
(defthm vl-html-encode-string-streqv-congruence-on-x (implies (streqv x x-equiv) (equal (vl-html-encode-string x tabsize) (vl-html-encode-string x-equiv tabsize))) :rule-classes :congruence)
Theorem:
(defthm vl-html-encode-string-of-pos-fix-tabsize (equal (vl-html-encode-string x (pos-fix tabsize)) (vl-html-encode-string x tabsize)))
Theorem:
(defthm vl-html-encode-string-pos-equiv-congruence-on-tabsize (implies (acl2::pos-equiv tabsize tabsize-equiv) (equal (vl-html-encode-string x tabsize) (vl-html-encode-string x tabsize-equiv))) :rule-classes :congruence)