• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
      • Json-encoding
        • Json-encode-main
        • Json-encode-weird-char
        • Json-encode-atom
        • Json-encode
        • Json-encode-chars
        • Json-encode-char
        • Json-encode-str
        • Json-simple-alist-p
        • Json-comma-and-maybe-newline
      • Security
      • Command
      • In-main-thread
      • Message
      • Start
      • Bindings
      • Stop
      • Try-in-main-thread
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Json-encoding

Json-encode-weird-char

Convert special characters into \uXXXX sequences.

Signature

(json-encode-weird-char code acc) → new-acc

Returns

new-acc — Type (character-listp new-acc), given (character-listp acc).

This lets us properly encode weird things like control characters.

BOZO we could use more readable encoding like \n and \t in some cases. For now we do it dumbly.

Definitions and Theorems

Function: json-encode-weird-char

(defun json-encode-weird-char (code acc)
       (declare (type (unsigned-byte 8) code))
       (let ((__function__ 'json-encode-weird-char))
            (declare (ignorable __function__))
            (b* ((lo (logand code 15))
                 (hi (logand (ash code -4) 15))
                 (acc (cons #\\ acc))
                 (acc (cons #\u acc))
                 (acc (cons #\0 acc))
                 (acc (cons #\0 acc))
                 (acc (cons (digit-to-char hi) acc))
                 (acc (cons (digit-to-char lo) acc)))
                acc)))

Theorem: character-listp-of-json-encode-weird-char

(defthm character-listp-of-json-encode-weird-char
        (implies (character-listp acc)
                 (b* ((new-acc (json-encode-weird-char code acc)))
                     (character-listp new-acc)))
        :rule-classes :rewrite)