		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Grammar-lexp

Grammatical lexing.

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

The lexical grammar specifies how a sequence of Unicode characters can be organized into a sequence of lexemes; more precisely, into a sequence of lexeme CSTs. This is the case when the fringe of the lexeme CSTs is the Unicode character sequence.

Given a Unicode character sequence ucodes there may be zero or one or more CST sequences that satisfy this predicate. If there is zero, ucodes is not syntactically valid Leo code. If there is one or more, ucodes may be syntactically valid Leo code, if additional requirements are satisfied.

If for each ucodes there were always at most one trees such that this predicate holds, the lexical grammar would be unambiguous, and lexing requirements would be completely defined by this predicate. However, the lexical grammar is ambiguous: for example, ** could form either two * symbol tokens or a single ** symbol token. It is common for lexical grammars of programming languages to be ambiguous, and to be disambiguated by extra-grammatical requirements, similar to the ones formalized later.

Definitions and Theorems

Function: grammar-lexp

(defun grammar-lexp (ucodes trees)
  (declare (xargs :guard (and (unicode-listp ucodes)
                              (abnf::tree-listp trees))))
  (let ((__function__ 'grammar-lexp))
    (declare (ignorable __function__))
    (and (abnf-tree-list-with-root-p (abnf::tree-list-fix trees)
                                     "lexeme")
         (equal (unicode-list->codepoint-list ucodes)
                (abnf::tree-list->string trees)))))

Theorem: booleanp-of-grammar-lexp

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

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

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

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

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

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

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

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

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