		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Statement-parses?

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

Signature
(statement-parses? statement-string) → yes/no
Arguments: statement-string — Guard (stringp statement-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 statement.

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

Definitions and Theorems

Function: statement-parses?

(defun statement-parses? (statement-string)
 (declare (xargs :guard (stringp statement-string)))
 (let ((__function__ 'statement-parses?))
  (declare (ignorable __function__))
  (b* ((tree? (parse-fragment-to-cst "statement" statement-string)))
    (and (abnf::treep tree?)
         (abnf-tree-with-root-p tree? "statement")))))

Theorem: booleanp-of-statement-parses?

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