		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Lexp

Declarative specification of lexing.

Signature
(lexp ucodes trees) → yes/no
Arguments: ucodes — Guard (unicode-listp ucodes).; trees — Guard (abnf::tree-listp trees).
Returns: yes/no — Type (booleanp yes/no).

A sequence of Unicode characters can be lexed to a sequence of lexeme CSTs iff the fringe of the CST sequence is the Unicode sequence, the longest lexeme rule holds, and identifiers are lexed correctly. There should be at most one CST sequence satisfying these requirements, but this remains to be formally proved.

Definitions and Theorems

Function: lexp

(defun lexp (ucodes trees)
  (declare (xargs :guard (and (unicode-listp ucodes)
                              (abnf::tree-listp trees))))
  (let ((__function__ 'lexp))
    (declare (ignorable __function__))
    (and (grammar-lexp ucodes trees)
         (longest-lexp trees)
         (identifier-lexp-list trees))))

Theorem: booleanp-of-lexp

(defthm booleanp-of-lexp
  (b* ((yes/no (lexp ucodes trees)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: lexp-of-unicode-list-fix-ucodes

(defthm lexp-of-unicode-list-fix-ucodes
  (equal (lexp (unicode-list-fix ucodes) trees)
         (lexp ucodes trees)))

Theorem: lexp-unicode-list-equiv-congruence-on-ucodes

(defthm lexp-unicode-list-equiv-congruence-on-ucodes
  (implies (unicode-list-equiv ucodes ucodes-equiv)
           (equal (lexp ucodes trees)
                  (lexp ucodes-equiv trees)))
  :rule-classes :congruence)

Theorem: lexp-of-tree-list-fix-trees

(defthm lexp-of-tree-list-fix-trees
  (equal (lexp ucodes (abnf::tree-list-fix trees))
         (lexp ucodes trees)))

Theorem: lexp-tree-list-equiv-congruence-on-trees

(defthm lexp-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv trees trees-equiv)
           (equal (lexp ucodes trees)
                  (lexp ucodes trees-equiv)))
  :rule-classes :congruence)