		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Abs-unicode-escape

Abstract a unicode-escape tree to a Unicode character.

Signature
(abs-unicode-escape tree) → unicode
Arguments: tree — Guard (abnf-tree-with-root-p tree "unicode-escape").
Returns: unicode — Type (unicodep unicode), given the guard.

A unicode-escape tree consists of a Unicode escape, which is essentially a number represented via four hexadecimal digit characters. We abstract this kind of tree to the Unicode character whose code is the number represented by the four hexadecimal digits, in big-endian order.

A unicode-escape tree has six subtrees, for the backslash, the `u' letter, and the four hexadecimal digits. We obtain the hex-digit subtrees (ignoring the other two subtrees), abstract them to four natural numbers below 16, and combine them in big-endian order.

Definitions and Theorems

Function: abs-unicode-escape

(defun abs-unicode-escape (tree)
  (declare
       (xargs :guard (abnf-tree-with-root-p tree "unicode-escape")))
  (let ((__function__ 'abs-unicode-escape))
    (declare (ignorable __function__))
    (b* ((subtrees (abnf::tree-nonleaf->branches tree))
         (subtree1 (car (third subtrees)))
         (subtree2 (car (fourth subtrees)))
         (subtree3 (car (fifth subtrees)))
         (subtree4 (car (sixth subtrees)))
         (val1 (abs-hex-digit subtree1))
         (val2 (abs-hex-digit subtree2))
         (val3 (abs-hex-digit subtree3))
         (val4 (abs-hex-digit subtree4)))
      (+ (ash val1 12)
         (ash val2 8)
         (ash val3 4)
         val4))))

Theorem: unicodep-of-abs-unicode-escape

(defthm unicodep-of-abs-unicode-escape
  (implies (and (abnf-tree-with-root-p tree '"unicode-escape"))
           (b* ((unicode (abs-unicode-escape tree)))
             (unicodep unicode)))
  :rule-classes :rewrite)