		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Reserved-keyword-tree

Tree for a reserved keyword.

Signature
(reserved-keyword-tree keyword) → tree
Arguments: keyword — Guard (reserved-keywordp keyword).
Returns: tree — Type (abnf-tree-with-root-p tree "reserved-keyword").

This is used in grammar-reserved-keywordp-when-reserved-keywordp.

Definitions and Theorems

Function: reserved-keyword-tree

(defun reserved-keyword-tree (keyword)
 (declare (xargs :guard (reserved-keywordp keyword)))
 (let ((keyword (mbe :logic
                     (if (reserved-keywordp keyword)
                         keyword
                       (string=>unicode "_"))
                     :exec keyword)))
  (abnf::tree-nonleaf (abnf::rulename "reserved-keyword")
                      (list (list (abnf::tree-leafterm keyword))))))

Theorem: return-type-of-reserved-keyword-tree

(defthm return-type-of-reserved-keyword-tree
  (b* ((tree (reserved-keyword-tree keyword)))
    (abnf-tree-with-root-p tree "reserved-keyword"))
  :rule-classes :rewrite)

Theorem: tree->string-of-reserved-keyword-tree

(defthm tree->string-of-reserved-keyword-tree
  (equal (abnf::tree->string (reserved-keyword-tree keyword))
         (if (reserved-keywordp keyword)
             keyword
           (string=>unicode "_"))))