• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
        • Html-encode-string-aux
        • Html-encode-chars-aux
        • Html-encode-push
        • Html-encode-string-basic-aux
        • Html-encode-string
        • Html-encode-char-basic
        • Html-encode-chars-basic-aux
        • Html-encode-string-basic
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)