		Search-engine friendly clone of the ACL2 documentation.

Json-encoding

Json-encode-atom

Signature
(json-encode-atom x acc) → new-acc
Arguments: x — Guard (atom x).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: json-encode-atom

(defun json-encode-atom (x acc)
 (declare (xargs :guard (atom x)))
 (let ((__function__ 'json-encode-atom))
  (declare (ignorable __function__))
  (let*
   ((acc (cons #\" acc))
    (acc
      (cond ((symbolp x)
             (json-encode-str (symbol-name x)
                              (if (keywordp x) (cons #\: acc) acc)))
            ((integerp x)
             (if (< x 0)
                 (revappend (str::nat-to-dec-chars (- x))
                            (cons #\- acc))
               (revappend (str::nat-to-dec-chars x)
                          acc)))
            ((characterp x)
             (json-encode-char x acc))
            ((stringp x) (json-encode-str x acc))
            ((acl2-numberp x)
             (json-encode-chars (explode-atom x 10)
                                acc))
            (t (progn$ (raise "Bad ACL2 object: ~x0" x)
                       acc)))))
   (cons #\" acc))))

Theorem: character-listp-of-json-encode-atom

(defthm character-listp-of-json-encode-atom
  (implies (character-listp acc)
           (b* ((new-acc (json-encode-atom x acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)