Fast way to figure out the new column after printing a JSON string with proper encoding.
(jp-col-after-printing-string-aux col x n xl) → new-col
Function:
(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:
(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)