		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-escape

Evaluate an escape to a list of bytes.

Signature
(eval-escape esc) → bytes
Arguments: esc — Guard (escapep esc).
Returns: bytes — Type (acl2::ubyte8-listp bytes).

The evaluation of plain string literals involves first turning the string into a sequence of bytes. Here we turn an escape into a sequence of bytes. An escape consisting of a backslash followed by a single character is turned into a singleton byte list with the character's code. A \x... escape is turned into a singleton byte list with the value of the escape. A \u... escape is turned into a list of 1, 2, or 3 bytes that is the UTF-8 encoding of the code point.

Definitions and Theorems

Function: eval-escape

(defun eval-escape (esc)
  (declare (xargs :guard (escapep esc)))
  (let ((__function__ 'eval-escape))
    (declare (ignorable __function__))
    (escape-case esc
                 :single-quote (list (char-code #\'))
                 :double-quote (list (char-code #\"))
                 :backslash (list (char-code #\\))
                 :letter-n (list 10)
                 :letter-r (list 13)
                 :letter-t (list 9)
                 :line-feed (list 10)
                 :carriage-return (list 13)
                 :x (list (eval-hex-pair esc.get))
                 :u (ubyte16-to-utf8 (eval-hex-quad esc.get)))))

Theorem: ubyte8-listp-of-eval-escape

(defthm ubyte8-listp-of-eval-escape
  (b* ((bytes (eval-escape esc)))
    (acl2::ubyte8-listp bytes))
  :rule-classes :rewrite)

Theorem: eval-escape-of-escape-fix-esc

(defthm eval-escape-of-escape-fix-esc
  (equal (eval-escape (escape-fix esc))
         (eval-escape esc)))

Theorem: eval-escape-escape-equiv-congruence-on-esc

(defthm eval-escape-escape-equiv-congruence-on-esc
  (implies (escape-equiv esc esc-equiv)
           (equal (eval-escape esc)
                  (eval-escape esc-equiv)))
  :rule-classes :congruence)