		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemize-leo-from-bytes

Lexes the UTF-8 bytes into a list of lexemes.

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

A lexeme is a token, comment, or whitespace. lexemize-leo-from-bytes 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-from-bytes

(defun lexemize-leo-from-bytes (leo-bytes)
  (declare (xargs :guard (nat-listp leo-bytes)))
  (let ((__function__ 'lexemize-leo-from-bytes))
    (declare (ignorable __function__))
    (b* (((unless (unsigned-byte-listp 8 leo-bytes))
          (reserrf (cons :invalid-octets leo-bytes)))
         (codepoints (acl2::utf8=>ustring leo-bytes))
         ((unless (nat-listp codepoints))
          (reserrf (cons :invalid-utf-8 leo-bytes))))
      (lexemize-leo codepoints))))

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

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