		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-char-val

A char-val parse tree is abstracted to its corresponding character value notation.

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

Definitions and Theorems

Function: abstract-char-val

(defun abstract-char-val (tree)
 (declare (xargs :guard (treep tree)))
 (b* (((fun (fail))
       (prog2$ (abstract-fail)
               (char-val-sensitive "")))
      ((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))
      ((unless (tree-case subtree :nonleaf))
       (fail))
      (rulename (tree-nonleaf->rulename? subtree)))
   (if (equal rulename
              (rulename "case-sensitive-string"))
       (char-val-sensitive (abstract-case-sensitive-string subtree))
     (b* (((mv charstring iprefix)
           (abstract-case-insensitive-string subtree)))
       (char-val-insensitive iprefix charstring)))))

Theorem: char-val-p-of-abstract-char-val

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