		Search-engine friendly clone of the ACL2 documentation.

Tokenizer

Tokenize-pfcs-bytes

Lexes the bytes of a pfcs system into a list of tokens.

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

This does the same thing as tokenize-pfcs, but does not need to convert the string to bytes first.

Definitions and Theorems

Function: tokenize-pfcs-bytes

(defun tokenize-pfcs-bytes (pfcs-bytes)
  (declare (xargs :guard (nat-listp pfcs-bytes)))
  (let ((__function__ 'tokenize-pfcs-bytes))
    (declare (ignorable __function__))
    (b* ((lexeme-trees-result (lexemize-pfcs-from-bytes pfcs-bytes))
         ((when (reserrp lexeme-trees-result))
          (reserrf "problem lexing pfcs-bytes"))
         (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-bytes

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