		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

File-parses-same-fringe?

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

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

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

Definitions and Theorems

Function: file-parses-same-fringe?

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

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

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