		Search-engine friendly clone of the ACL2 documentation.

Lexer

Make-test-tokens

A simple way to lex an ACL2 string.

Signature
(make-test-tokens string &key (config '*vl-default-loadconfig*)) → tokens
Arguments: string — Should be free of preprocessor symbols.
Guard (stringp string).; config — Guard (vl-loadconfig-p config).
Returns: tokens — Type (vl-tokenlist-p tokens).

This is mainly intended for testing parser routines. We don't bother to preprocess the input and just ignore any warning.

Definitions and Theorems

Function: make-test-tokens-fn

(defun make-test-tokens-fn (string config)
  (declare (xargs :guard (and (stringp string)
                              (vl-loadconfig-p config))))
  (let ((__function__ 'make-test-tokens))
    (declare (ignorable __function__))
    (b* ((echars (vl-echarlist-from-str string))
         ((mv successp tokens ?warnings)
          (vl-lex echars
                  :config config
                  :warnings nil))
         ((unless successp)
          (raise "Lexing failed."))
         ((mv tokens ?cmap)
          (vl-kill-whitespace-and-comments tokens)))
      tokens)))

Theorem: vl-tokenlist-p-of-make-test-tokens

(defthm vl-tokenlist-p-of-make-test-tokens
  (b* ((tokens (make-test-tokens-fn string config)))
    (vl-tokenlist-p tokens))
  :rule-classes :rewrite)