		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lexemize-pfcs

Lexes the Unicode codepoints pfcs-codepoints into lexemes.

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

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

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

Definitions and Theorems

Function: lexemize-pfcs

(defun lexemize-pfcs (pfcs-codepoints)
 (declare (xargs :guard (nat-listp pfcs-codepoints)))
 (let ((__function__ 'lexemize-pfcs))
  (declare (ignorable __function__))
  (b* (((mv trees rest-input)
        (lex-*-lexeme pfcs-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-pfcs

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