		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemize-leo

Lexes the Unicode code points leo-codepoints into a list of lexemes.

Signature
(lexemize-leo leo-codepoints) → leo-lexemes
Arguments: leo-codepoints — Guard (nat-listp leo-codepoints).
Returns: leo-lexemes — Type (abnf::tree-list-resultp leo-lexemes).

A lexeme is a token, comment, or whitespace. lexemize-leo returns two values: an error flag and a list of these lexemes in abnf::tree form. Lexemes are further separated into keyword, literal, identifier, or symbol. Recombining these lexemes is done in the parser.

If the input cannot be fully lexed, a reserrp is returned.

Definitions and Theorems

Function: lexemize-leo

(defun lexemize-leo (leo-codepoints)
 (declare (xargs :guard (nat-listp leo-codepoints)))
 (let ((__function__ 'lexemize-leo))
  (declare (ignorable __function__))
  (b* (((mv trees rest-input)
        (lex-*-lexeme leo-codepoints))
       ((when (reserrp trees))
        (reserrf (cons :unexpected-reserrp trees)))
       ((unless (null rest-input))
        (reserrf (cons :cannot-fully-lex (cons trees rest-input)))))
    trees)))

Theorem: tree-list-resultp-of-lexemize-leo

(defthm tree-list-resultp-of-lexemize-leo
  (b* ((leo-lexemes (lexemize-leo leo-codepoints)))
    (abnf::tree-list-resultp leo-lexemes))
  :rule-classes :rewrite)