		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)
                  (unsigned-byte-listp 8 fringe)
                  (>= (len fringe) 5)))
     nil)
    (double-quote-p (equal (nth 3 fringe) (char-code #\")))
    (hex-chars-and-underbars (subseq fringe 4 (- (len fringe) 1)))
    ((unless (unsigned-byte-listp 8 hex-chars-and-underbars))
     (raise "Internal error: character codes ~x0."
            hex-chars-and-underbars))
    (hex-chars-and-underbars (nats=>chars hex-chars-and-underbars))
    ((when (endp hex-chars-and-underbars))
     (make-literal-hex-string
          :get (make-hex-string :content nil
                                :double-quote-p double-quote-p)))
    ((unless
      (and
          (consp hex-chars-and-underbars)
          (consp (cdr hex-chars-and-underbars))
          (str::hex-digit-char-p (first hex-chars-and-underbars))
          (str::hex-digit-char-p (second hex-chars-and-underbars))))
     (raise "Internal error: characters ~x0."
            hex-chars-and-underbars))
    (digit1 (make-hex-digit :get (first hex-chars-and-underbars)))
    (digit2 (make-hex-digit :get (second hex-chars-and-underbars)))
    (pair (make-hex-pair :1st digit1 :2nd digit2))
    (rest (hex-chars-and-uscores-to-hex-string-rest-element-list
               (cddr hex-chars-and-underbars)))
    (content (make-hex-string-content :first pair
                                      :rest rest))
    (hex-string (make-hex-string :content content
                                 :double-quote-p double-quote-p)))
   (make-literal-hex-string :get hex-string))))

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)