		Search-engine friendly clone of the ACL2 documentation.

Parser

Read-stringlit

Read a string literal token.

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

This is called when we expect a string literal token. We read the next token, ensuring it exists and is a string literal. We return the string literal if successful.

Definitions and Theorems

Function: read-stringlit

(defun read-stringlit (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (parstatep parstate)))
  (let ((__function__ 'read-stringlit))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-stringlit)
          (irr-span)
          parstate)
         ((erp token span parstate)
          (read-token parstate))
         ((unless (and token (token-case token :string)))
          (reterr-msg :where (position-to-msg (span->start span))
                      :expected "a string literal"
                      :found (token-to-msg token)))
         (stringlit (token-string->unwrap token)))
      (retok stringlit span parstate))))

Theorem: stringlitp-of-read-stringlit.stringlit

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

Theorem: spanp-of-read-stringlit.span

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

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

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

Theorem: parsize-of-read-stringlit-uncond

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

Theorem: parsize-of-read-stringlit-cond

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