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