		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemize-pfcs-from-string

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

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

A lexeme is a token or whitespace. lexemize-pfcs-from-string returns two values: an error flag and a list of these lexemes in abnf::tree form.

Since ACL2 strings are sequences of characters with codes from 0 to 255, pfcs-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-pfcs-from-string

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

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

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