		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

File-lex-parse-p

Lexing and parsing of Leo files.

The complete lexing and parsing requirements for Leo files are formalized via the following predicate, which combines the lexing and parsing predicates defined above. It says that the Unicode character sequence ucodes is lexed and parsed into a CST file iff the characters are lexed into a CST sequence lexemes, and the tokens filtered from the latter can be parsed into a file.

It should be the case that this lexing and parsing is unambiguous, i.e. that for every list of Unicode characters there is at most one CST for which the predicate holds; but this remains to be formally proved. If none exists, the Unicode character list does not form a syntactically valid Leo file. If one exists, the Unicode character sequence forms a syntactically valid Leo file, organized according to that CST.

Definitions and Theorems

Theorem: file-lex-parse-p-suff

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

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

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

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

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

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

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

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

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

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

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