		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Output-file-parsep

Parsing of Leo output files.

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

Note also that, while file-parsep passes the empty list of identifiers to token-fringe, here we pass the list consisting of the output identifier. This is because this identifier is treated a bit like a keyword in the grammar of output files: it does not appear as identifier in the grammar, but ``directly'' as %s"output". 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: output-file-parsep

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

Theorem: booleanp-of-output-file-parsep

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

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

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

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

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

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

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

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

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