		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Input-file-lex-parse-p

Lexing and parsing of Leo input files.

This is analogous to file-lex-parse-p, but for input files instead of (code) files.

Definitions and Theorems

Theorem: input-file-lex-parse-p-suff

(defthm input-file-lex-parse-p-suff
  (implies (and (abnf::tree-listp lexemes)
                (lexp ucodes lexemes)
                (input-file-parsep (filter-tokens lexemes)
                                   file))
           (input-file-lex-parse-p ucodes file)))

Theorem: booleanp-of-input-file-lex-parse-p

(defthm booleanp-of-input-file-lex-parse-p
  (b* ((yes/no (input-file-lex-parse-p ucodes file)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: input-file-lex-parse-p-of-unicode-list-fix-ucodes

(defthm input-file-lex-parse-p-of-unicode-list-fix-ucodes
  (equal (input-file-lex-parse-p (unicode-list-fix ucodes)
                                 file)
         (input-file-lex-parse-p ucodes file)))

Theorem: input-file-lex-parse-p-unicode-list-equiv-congruence-on-ucodes

(defthm
     input-file-lex-parse-p-unicode-list-equiv-congruence-on-ucodes
  (implies (unicode-list-equiv ucodes ucodes-equiv)
           (equal (input-file-lex-parse-p ucodes file)
                  (input-file-lex-parse-p ucodes-equiv file)))
  :rule-classes :congruence)

Theorem: input-file-lex-parse-p-of-tree-fix-file

(defthm input-file-lex-parse-p-of-tree-fix-file
  (equal (input-file-lex-parse-p ucodes (abnf::tree-fix file))
         (input-file-lex-parse-p ucodes file)))

Theorem: input-file-lex-parse-p-tree-equiv-congruence-on-file

(defthm input-file-lex-parse-p-tree-equiv-congruence-on-file
  (implies (abnf::tree-equiv file file-equiv)
           (equal (input-file-lex-parse-p ucodes file)
                  (input-file-lex-parse-p ucodes file-equiv)))
  :rule-classes :congruence)