		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-hex-number

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

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

Definitions and Theorems

Function: cst2ast-hex-number

(defun cst2ast-hex-number (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'cst2ast-hex-number))
  (declare (ignorable __function__))
  (b*
   ((fringe (abnf::tree->string tree))
    ((unless (unsigned-byte-listp 8 fringe))
     (prog2$
      (er
         hard? 'top-level
         "unexpected type of leafterm nats when parsing identifier")
      nil))
    ((unless (and (listp fringe)
                  (> (len fringe) 2)
                  (equal (first fringe) (char-code #\0))
                  (equal (second fringe)
                         (char-code #\x))))
     nil)
    (hex-digit-char-codes (cddr fringe))
    ((unless (unsigned-byte-listp 8 hex-digit-char-codes))
     nil)
    (hex-digit-chars (nats=>chars hex-digit-char-codes))
    ((unless (str::hex-digit-char-list*p hex-digit-chars))
     nil)
    (hex-digits (cst2ast-hex-digit-char-list hex-digit-chars)))
   (make-literal-hex-number :get hex-digits))))

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

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