		Search-engine friendly clone of the ACL2 documentation.

Jp-str

Jp-col-after-printing-string-aux

Fast way to figure out the new column after printing a JSON string with proper encoding.

Signature
(jp-col-after-printing-string-aux col x n xl) → new-col
Arguments: col — Current column we're at.
Guard (natp col).; x — String we're about to print, not yet reversed.
Guard (stringp x).; n — Current position in X.
Guard (natp n).; xl — Pre-computed length of X.
Guard (natp xl).
Returns: new-col — Type (natp new-col).

Definitions and Theorems

Function: jp-col-after-printing-string-aux

(defun jp-col-after-printing-string-aux (col x n xl)
  (declare (xargs :guard (and (natp col)
                              (stringp x)
                              (natp n)
                              (natp xl))))
  (declare (type (integer 0 *) col n xl)
           (type string x))
  (declare (xargs :guard (and (<= n xl) (= xl (length x)))))
  (let ((__function__ 'jp-col-after-printing-string-aux))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (nfix xl) (nfix n)))
                     :exec (= n xl)))
          (lnfix col))
         ((the (unsigned-byte 8) code)
          (char-code (char x n)))
         ((when (or (<= code 31) (>= code 127)))
          (jp-col-after-printing-string-aux (+ 6 col)
                                            x (+ 1 (lnfix n))
                                            xl)))
      (jp-col-after-printing-string-aux (+ 1 col)
                                        x (+ 1 (lnfix n))
                                        xl))))

Theorem: natp-of-jp-col-after-printing-string-aux

(defthm natp-of-jp-col-after-printing-string-aux
  (b* ((new-col (jp-col-after-printing-string-aux col x n xl)))
    (natp new-col))
  :rule-classes :type-prescription)