		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Input-file-parsep

Parsing of Leo input files.

Signature
(input-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 is analogous to file-parsep, but for input files instead of (code) files.

Note also that, while file-parsep passes the empty list of identifiers to token-fringe, here we pass the list consisting of the private identifier. This is because this identifier is treated a bit like a keyword in the grammar of input files: it does not appear as identifier in the grammar, but ``directly'' as %s"private". Therefore, when we calculate the token fringe for a CST of an input file we need to turn that into a token identifier in order to properly relate it to the list of tokens filtered from the list of lexemes.

Definitions and Theorems

Function: input-file-parsep

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

Theorem: booleanp-of-input-file-parsep

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

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

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

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

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

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

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

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

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