		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Contextual-keyword-tree

Tree for a contextual keyword.

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

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

Definitions and Theorems

Function: contextual-keyword-tree

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

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

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

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

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