		Search-engine friendly clone of the ACL2 documentation.

Parser

Read-keyword

Read a specific keyword token.

Signature
(read-keyword keywd parstate) → (mv erp span new-parstate)
Arguments: keywd — Guard (stringp keywd).; parstate — Guard (parstatep parstate).
Returns: span — Type (spanp span).; new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

This is called when we expect a specific keyword. We pass the string for the keyword, and we read the next token, ensuring it exists and it is that keyword.

Definitions and Theorems

Function: read-keyword

(defun read-keyword (keywd parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (stringp keywd)
                              (parstatep parstate))))
  (let ((__function__ 'read-keyword))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-span) parstate)
         ((erp token span parstate)
          (read-token parstate))
         ((unless (token-keywordp token keywd))
          (reterr-msg :where (position-to-msg (span->start span))
                      :expected (msg "the keyword \"~s0\"" keywd)
                      :found (token-to-msg token))))
      (retok span parstate))))

Theorem: spanp-of-read-keyword.span

(defthm spanp-of-read-keyword.span
  (b* (((mv acl2::?erp ?span ?new-parstate)
        (read-keyword keywd parstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: parstatep-of-read-keyword.new-parstate

(defthm parstatep-of-read-keyword.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?span ?new-parstate)
                 (read-keyword keywd parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-read-keyword-uncond

(defthm parsize-of-read-keyword-uncond
  (b* (((mv acl2::?erp ?span ?new-parstate)
        (read-keyword keywd parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-read-keyword-cond

(defthm parsize-of-read-keyword-cond
  (b* (((mv acl2::?erp ?span ?new-parstate)
        (read-keyword keywd parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)