		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-rulename

A rulename parse tree is abstracted to its corresponding rule name.

Signature
(abstract-rulename tree) → rulename
Arguments: tree — Guard (treep tree).
Returns: rulename — Type (rulenamep rulename).

The characters are converted to lowercase, according to the normalized representation required by rulename-wfp.

Definitions and Theorems

Function: abstract-rulename

(defun abstract-rulename (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) (rulename "")))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))))
        (fail))
       (trees-alpha (car treess))
       (trees-alpha/digit/dash (cadr treess))
       ((unless (consp trees-alpha)) (fail))
       (tree-alpha (car trees-alpha))
       (char (abstract-alpha tree-alpha))
       (chars (abstract-*-alpha/digit/dash trees-alpha/digit/dash))
       (charstring (implode (downcase-charlist (cons char chars)))))
    (rulename charstring)))

Theorem: rulenamep-of-abstract-rulename

(defthm rulenamep-of-abstract-rulename
  (b* ((rulename (abstract-rulename tree)))
    (rulenamep rulename))
  :rule-classes :rewrite)