		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

File-parses?

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

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

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

Definitions and Theorems

Function: file-parses?

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

Theorem: booleanp-of-file-parses?

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