		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Abs-unicode-input-character

Abstract a unicode-input-character tree to a Unicode character.

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

Whether the tree is a raw character or a Unicode escape, it always denotes a single Unicode character, which we abstract this kind of trees to.

A unicode-input-character tree has a single subtree, accessible via caar. This subtree is either a unicode-escape tree or a raw-input-character tree.

Definitions and Theorems

Function: abs-unicode-input-character

(defun abs-unicode-input-character (tree)
 (declare
  (xargs
     :guard (abnf-tree-with-root-p tree "unicode-input-character")))
 (let ((__function__ 'abs-unicode-input-character))
   (declare (ignorable __function__))
   (b* ((subtree (caar (abnf::tree-nonleaf->branches tree))))
     (if (abnf-tree-with-root-p subtree "unicode-escape")
         (abs-unicode-escape subtree)
       (abs-raw-input-character subtree)))))

Theorem: unicodep-of-abs-unicode-input-character

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