		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Token-parses-same-fringe?

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

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

Same as token-parses?, but this does some additional checks, so it is better for testing.

Definitions and Theorems

Function: token-parses-same-fringe?

(defun token-parses-same-fringe? (token-string)
 (declare (xargs :guard (stringp token-string)))
 (let ((__function__ 'token-parses-same-fringe?))
  (declare (ignorable __function__))
  (b*
   (((mv tree? lexemes)
     (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))
   (and
       (abnf-tree-with-root-p tree? rulename)
       (abnf-tree-list-with-root-p lexemes "lexeme")
       (equal (abnf::tree-list->string lexemes)
              (acl2::utf8=>ustring (string=>nats token-string)))))))

Theorem: booleanp-of-token-parses-same-fringe?

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