		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-hexdig

A HEXDIG parse tree is abstracted to its hexadecimal digit.

Signature
(abstract-hexdig tree) → hexdig
Arguments: tree — Guard (treep tree).
Returns: hexdig — Type (integer-range-p 0 16 hexdig).

Definitions and Theorems

Function: abstract-hexdig

(defun abstract-hexdig (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) 0))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       ((when (tree-case subtree :nonleaf))
        (abstract-digit subtree))
       (nat (abstract-terminal subtree)))
    (cond ((member nat
                   (list (char-code #\A) (char-code #\a)))
           10)
          ((member nat
                   (list (char-code #\B) (char-code #\b)))
           11)
          ((member nat
                   (list (char-code #\C) (char-code #\c)))
           12)
          ((member nat
                   (list (char-code #\D) (char-code #\d)))
           13)
          ((member nat
                   (list (char-code #\E) (char-code #\e)))
           14)
          (t 15))))

Theorem: return-type-of-abstract-hexdig

(defthm return-type-of-abstract-hexdig
  (b* ((hexdig (abstract-hexdig tree)))
    (integer-range-p 0 16 hexdig))
  :rule-classes :rewrite)

Theorem: natp-of-abstract-hexdig

(defthm natp-of-abstract-hexdig
  (b* ((hexdig (abstract-hexdig tree)))
    (natp hexdig))
  :rule-classes :type-prescription)

Theorem: abstract-hexdig-linear

(defthm abstract-hexdig-linear
  (b* ((hexdig (abstract-hexdig tree)))
    (< hexdig 16))
  :rule-classes :linear)