		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Jkeyword-tree

Tree for a (non-restricted) keyword.

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

This is used in grammar-jkeywordp-when-jkeywordp.

Definitions and Theorems

Function: jkeyword-tree

(defun jkeyword-tree (keyword)
  (declare (xargs :guard (jkeywordp keyword)))
  (let ((__function__ 'jkeyword-tree))
    (declare (ignorable __function__))
    (let ((keyword (mbe :logic
                        (if (jkeywordp keyword)
                            keyword
                          (string=>unicode "_"))
                        :exec keyword)))
      (abnf::tree-nonleaf
           (abnf::rulename "keyword")
           (list (list (abnf::tree-leafterm keyword)))))))

Theorem: return-type-of-jkeyword-tree

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

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

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