		Search-engine friendly clone of the ACL2 documentation.

Tokenizer

Tokenize-pfcs

Lexes the bytes of pfcs-string into a list of tokens.

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

The returned trees are for rulenames identifier, integer, operator, or separator. Each token is represented by an abnf::tree. Discards whitespace. If the input structure from any lexeme down to the specific token type is incorrect, returns an error result value of type reserr instead of a list of tokens. Also, if the input string ends in the middle of a token, returns reserr.

Definitions and Theorems

Function: tokenize-pfcs

(defun tokenize-pfcs (pfcs-string)
 (declare (xargs :guard (stringp pfcs-string)))
 (let ((__function__ 'tokenize-pfcs))
  (declare (ignorable __function__))
  (b* ((lexeme-trees-result (lexemize-pfcs-from-string pfcs-string))
       ((when (reserrp lexeme-trees-result))
        (reserrf "problem lexing pfcs-string"))
       (subtoken-trees (filter-and-reduce-lexeme-tree-to-subtoken-trees
                            lexeme-trees-result))
       ((when (reserrp subtoken-trees))
        (reserrf "problem with structure of lexeme tree")))
    subtoken-trees)))

Theorem: tree-list-resultp-of-tokenize-pfcs

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