		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Expression-parses-same-fringe?

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

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

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

Definitions and Theorems

Function: expression-parses-same-fringe?

(defun expression-parses-same-fringe? (expression-string)
 (declare (xargs :guard (stringp expression-string)))
 (let ((__function__ 'expression-parses-same-fringe?))
  (declare (ignorable __function__))
  (b* (((mv tree? lexemes)
        (parse-fragment-to-cst+ "expression" expression-string)))
   (and
    (abnf::treep tree?)
    (abnf-tree-with-root-p tree? "expression")
    (abnf-tree-list-with-root-p lexemes "lexeme")
    (equal
         (abnf::tree-list->string lexemes)
         (acl2::utf8=>ustring (string=>nats expression-string)))))))

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

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