		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-hex-val

A hex-val parse tree is abstracted to its corresponding numeric value notation.

Signature
(abstract-hex-val tree) → num-val
Arguments: tree — Guard (treep tree).
Returns: num-val — Type (num-val-p num-val).

Definitions and Theorems

Function: abstract-hex-val

(defun abstract-hex-val (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail)
                (num-val-direct (num-base-hex) nil)))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))
                     (consp (cddr treess))))
        (fail))
       (trees-1st-num (cadr treess))
       (1st-num (abstract-*hexdig trees-1st-num))
       (trees-rest (caddr treess))
       ((unless (consp trees-rest)) (fail))
       (tree-rest (car trees-rest))
       (rest (abstract-hex-val-rest tree-rest)))
    (if (nat-listp rest)
        (num-val-direct (num-base-hex)
                        (cons 1st-num rest))
      (num-val-range (num-base-hex)
                     1st-num rest))))

Theorem: num-val-p-of-abstract-hex-val

(defthm num-val-p-of-abstract-hex-val
  (b* ((num-val (abstract-hex-val tree)))
    (num-val-p num-val))
  :rule-classes :rewrite)