		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Expression-parses?

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

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

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

Definitions and Theorems

Function: expression-parses?

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

Theorem: booleanp-of-expression-parses?

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