		Search-engine friendly clone of the ACL2 documentation.

Lexer

Lex-token

Lex a token.

Signature
(lex-token input) → (mv tree rest-input)
Arguments: input — Guard (nat-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; rest-input — Type (nat-listp rest-input).

More precisely, lex a keyword, identifier, atomic-literal, numeral (that is not part of an atomic literal), or symbol.

If the next input is an at sign, the token may only be an annotation. If the next input is a double quote, the token may only be a string literal. If the next input is a decimal digit, the token may only be a numeric literal or a bare numeral. Otherwise, we try to lex something that starts with a letter (identifier, or keyword, or boolean, or address). Note that we need to wrap string, boolean and address literals with atomic-literal so that the returned CST will match the lexical grammar rules. Finally, we try to lex a symbol.

Definitions and Theorems

Function: lex-token

(defun lex-token (input)
 (declare (xargs :guard (nat-listp input)))
 (let ((__function__ 'lex-token))
   (declare (ignorable __function__))
   (b*
    (((when (endp input))
      (mv (reserrf :end-of-input) nil))
     (next (lnfix (car input)))
     ((when (= next (char-code #\@)))
      (b* (((mv tree input) (lex-annotation input))
           ((when (reserrp tree))
            (mv (reserrf-push tree) input)))
        (mv (abnf-tree-wrap tree "token")
            input)))
     ((when (= next (char-code #\")))
      (b* (((mv tree input)
            (lex-string-literal input))
           ((when (reserrp tree))
            (mv (reserrf-push tree) input)))
        (mv (abnf-tree-wrap (abnf-tree-wrap tree "atomic-literal")
                            "token")
            input)))
     ((when (or (and (<= (char-code #\0) next)
                     (<= next (char-code #\9)))))
      (b*
        (((mv tree input1)
          (lex-numeric-literal input))
         ((when (not (reserrp tree)))
          (mv (abnf-tree-wrap (abnf-tree-wrap tree "atomic-literal")
                              "token")
              input1))
         ((mv tree input2) (lex-numeral input))
         ((when (not (reserrp tree)))
          (mv (abnf-tree-wrap tree "token")
              input2)))
        (mv (reserrf-push tree)
            (nat-list-fix input))))
     ((mv tree input)
      (lex-identifier/keyword/boolean/address input))
     ((when (not (reserrp tree)))
      (mv (abnf-tree-wrap
               (cond ((abnf-tree-with-root-p tree "boolean-literal")
                      (abnf-tree-wrap tree "atomic-literal"))
                     ((abnf-tree-with-root-p tree "address-literal")
                      (abnf-tree-wrap tree "atomic-literal"))
                     (t tree))
               "token")
          input))
     ((mv tree input) (lex-symbol input))
     ((when (not (reserrp tree)))
      (mv (abnf-tree-wrap tree "token")
          input)))
    (mv (reserrf :no-token) input))))

Theorem: tree-resultp-of-lex-token.tree

(defthm tree-resultp-of-lex-token.tree
  (b* (((mv ?tree ?rest-input)
        (lex-token input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: nat-listp-of-lex-token.rest-input

(defthm nat-listp-of-lex-token.rest-input
  (b* (((mv ?tree ?rest-input)
        (lex-token input)))
    (nat-listp rest-input))
  :rule-classes :rewrite)

Theorem: len-of-lex-token-<=

(defthm len-of-lex-token-<=
  (b* (((mv ?tree ?rest-input)
        (lex-token input)))
    (<= (len rest-input) (len input)))
  :rule-classes :linear)

Theorem: len-of-lex-token-<

(defthm len-of-lex-token-<
  (b* (((mv ?tree ?rest-input)
        (lex-token input)))
    (implies (not (reserrp tree))
             (< (len rest-input) (len input))))
  :rule-classes :linear)

Theorem: lex-token-of-nat-list-fix-input

(defthm lex-token-of-nat-list-fix-input
  (equal (lex-token (nat-list-fix input))
         (lex-token input)))

Theorem: lex-token-nat-list-equiv-congruence-on-input

(defthm lex-token-nat-list-equiv-congruence-on-input
  (implies (acl2::nat-list-equiv input input-equiv)
           (equal (lex-token input)
                  (lex-token input-equiv)))
  :rule-classes :congruence)