		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-hex-string

Given a :nonleaf tree with rulename "hex-string", return the appropriate literal AST node.

Signature
(cst2ast-hex-string tree) → ast-node?
Arguments: tree — Guard (abnf::treep tree).
Returns: ast-node? — Type (literal-optionp ast-node?).

Definitions and Theorems

Function: cst2ast-hex-string

(defun cst2ast-hex-string (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'cst2ast-hex-string))
  (declare (ignorable __function__))
  (b*
    (((unless (and (abnf::treep tree)
                   (abnf::tree-case tree :nonleaf)))
      nil)
     (fringe (abnf::tree-list-list->string
                  (abnf::tree-nonleaf->branches tree)))
     ((unless (and (true-listp fringe)
                   (acl2::unsigned-byte-listp 8 fringe)
                   (>= (len fringe) 5)))
      nil)
     (hex-chars-and-underbars (subseq fringe 4 (- (len fringe) 1)))
     (hex-char-codes (remove-equal (char-code #\_)
                                   hex-chars-and-underbars))
     ((unless (acl2::unsigned-byte-listp 8 hex-char-codes))
      nil)
     (hex-chars (acl2::nats=>chars hex-char-codes))
     ((unless (str::hex-digit-char-list*p hex-chars))
      nil)
     (hex-pairs (hex-chars-to-hex-pair-list hex-chars))
     ((unless (hex-pair-listp hex-pairs))
      nil))
   (make-literal-hex-string
       :get
       (make-hex-string :content hex-pairs
                        :double-quote-p (equal (nth 3 fringe)
                                               (char-code #\")))))))

Theorem: literal-optionp-of-cst2ast-hex-string

(defthm literal-optionp-of-cst2ast-hex-string
  (b* ((ast-node? (cst2ast-hex-string tree)))
    (literal-optionp ast-node?))
  :rule-classes :rewrite)