		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemize-leo-from-string

Lexes the UTF-8 leo-string into a list of lexemes.

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

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

Since ACL2 strings are sequences of characters with codes from 0 to 255, leo-string, when converted to codes, is required to be valid UTF-8.

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

Definitions and Theorems

Function: lexemize-leo-from-string

(defun lexemize-leo-from-string (leo-string)
  (declare (xargs :guard (stringp leo-string)))
  (let ((__function__ 'lexemize-leo-from-string))
    (declare (ignorable __function__))
    (b* (((unless (stringp leo-string))
          (reserrf (cons :not-a-string leo-string)))
         (octets (string=>nats leo-string)))
      (lexemize-leo-from-bytes octets))))

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

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