		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Token-parses?

Checks if the given string can be parsed to a Leo token CST.

Signature
(token-parses? token-string) → yes/no
Arguments: token-string — Guard (stringp token-string).
Returns: yes/no — Type (booleanp yes/no).

Checks that the given string is lexed, tokenized, and parsed successfully and checks that the CST from parsing has the root rule name token.

Does not check that the lexemes have the same fringe as the given string. For that you want token-parses-same-fringe?.

Definitions and Theorems

Function: token-parses?

(defun token-parses? (token-string)
 (declare (xargs :guard (stringp token-string)))
 (let ((__function__ 'token-parses?))
  (declare (ignorable __function__))
  (b*
   ((tree? (parse-fragment-to-cst "token" token-string))
    ((unless (abnf::treep tree?)) nil)
    (rulename (abnf::check-tree-nonleaf? tree?))
    ((unless (stringp rulename)) nil)
    ((unless
        (member-equal rulename
                      '("keyword" "identifier" "atomic-literal"
                                  "numeral" "annotation" "symbol")))
     nil))
   (abnf-tree-with-root-p tree? rulename))))

Theorem: booleanp-of-token-parses?

(defthm booleanp-of-token-parses?
  (b* ((yes/no (token-parses? token-string)))
    (booleanp yes/no))
  :rule-classes :rewrite)