		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

File-parsep

Parsing of Leo files.

Signature
(file-parsep tokens file) → yes/no
Arguments: tokens — Guard (abnf::tree-listp tokens).; file — Guard (abnf::treep file).
Returns: yes/no — Type (booleanp yes/no).

This relates a list of token CSTs to a CST. The predicate holds iff the CST is for a file and the list of token CSTs is the token fringe of the file CST.

Definitions and Theorems

Function: file-parsep

(defun file-parsep (tokens file)
  (declare (xargs :guard (and (abnf::tree-listp tokens)
                              (abnf::treep file))))
  (let ((__function__ 'file-parsep))
    (declare (ignorable __function__))
    (and (abnf-tree-with-root-p (abnf::tree-fix file)
                                "file")
         (equal (token-fringe file nil)
                (abnf::tree-list-fix tokens)))))

Theorem: booleanp-of-file-parsep

(defthm booleanp-of-file-parsep
  (b* ((yes/no (file-parsep tokens file)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: file-parsep-of-tree-list-fix-tokens

(defthm file-parsep-of-tree-list-fix-tokens
  (equal (file-parsep (abnf::tree-list-fix tokens)
                      file)
         (file-parsep tokens file)))

Theorem: file-parsep-tree-list-equiv-congruence-on-tokens

(defthm file-parsep-tree-list-equiv-congruence-on-tokens
  (implies (abnf::tree-list-equiv tokens tokens-equiv)
           (equal (file-parsep tokens file)
                  (file-parsep tokens-equiv file)))
  :rule-classes :congruence)

Theorem: file-parsep-of-tree-fix-file

(defthm file-parsep-of-tree-fix-file
  (equal (file-parsep tokens (abnf::tree-fix file))
         (file-parsep tokens file)))

Theorem: file-parsep-tree-equiv-congruence-on-file

(defthm file-parsep-tree-equiv-congruence-on-file
  (implies (abnf::tree-equiv file file-equiv)
           (equal (file-parsep tokens file)
                  (file-parsep tokens file-equiv)))
  :rule-classes :congruence)