		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-lexer

Plex-spaces

Lex consecutive spaces during preprocessing.

Signature
(plex-spaces first-pos ppstate) → (mv erp lexeme span new-ppstate)
Arguments: first-pos — Guard (positionp first-pos).; ppstate — Guard (ppstatep ppstate).
Returns: lexeme — Type (plexemep lexeme).; span — Type (spanp span).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is called just after a space character (code 32) has been read; the position of that space character is passed as input here.

We read zero or more additional spaces, and we return a lexeme for spaces, with the count incremented by one to account for the first space.

Definitions and Theorems

Function: plex-spaces-loop

(defun plex-spaces-loop (prev-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (positionp prev-pos)
                              (ppstatep ppstate))))
  (b* (((reterr) 0 (irr-position) ppstate)
       ((erp char pos ppstate)
        (pread-char ppstate)))
    (cond ((not char)
           (retok 0 (position-fix prev-pos)
                  ppstate))
          ((utf8-= char 32)
           (b* (((erp nspaces last-pos ppstate)
                 (plex-spaces-loop pos ppstate)))
             (retok (1+ nspaces) last-pos ppstate)))
          (t (b* ((ppstate (punread-char ppstate)))
               (retok 0 (position-fix prev-pos)
                      ppstate))))))

Theorem: natp-of-plex-spaces-loop.nspaces

(defthm natp-of-plex-spaces-loop.nspaces
  (b* (((mv acl2::?erp
            ?nspaces ?last-pos ?new-ppstate)
        (plex-spaces-loop prev-pos ppstate)))
    (natp nspaces))
  :rule-classes (:rewrite :type-prescription))

Theorem: positionp-of-plex-spaces-loop.last-pos

(defthm positionp-of-plex-spaces-loop.last-pos
  (b* (((mv acl2::?erp
            ?nspaces ?last-pos ?new-ppstate)
        (plex-spaces-loop prev-pos ppstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-spaces-loop.new-ppstate

(defthm ppstatep-of-plex-spaces-loop.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp
                     ?nspaces ?last-pos ?new-ppstate)
                 (plex-spaces-loop prev-pos ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-spaces-loop-uncond

(defthm ppstate->size-of-plex-spaces-loop-uncond
  (b* (((mv acl2::?erp
            ?nspaces ?last-pos ?new-ppstate)
        (plex-spaces-loop prev-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Function: plex-spaces

(defun plex-spaces (first-pos ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (positionp first-pos)
                              (ppstatep ppstate))))
  (b* (((reterr)
        (irr-plexeme)
        (irr-span)
        ppstate)
       ((erp nspaces last-pos ppstate)
        (plex-spaces-loop first-pos ppstate)))
    (retok (plexeme-spaces (1+ nspaces))
           (make-span :start first-pos
                      :end last-pos)
           ppstate)))

Theorem: plexemep-of-plex-spaces.lexeme

(defthm plexemep-of-plex-spaces.lexeme
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-spaces first-pos ppstate)))
    (plexemep lexeme))
  :rule-classes :rewrite)

Theorem: spanp-of-plex-spaces.span

(defthm spanp-of-plex-spaces.span
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-spaces first-pos ppstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: ppstatep-of-plex-spaces.new-ppstate

(defthm ppstatep-of-plex-spaces.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
                 (plex-spaces first-pos ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-plex-spaces-uncond

(defthm ppstate->size-of-plex-spaces-uncond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-ppstate)
        (plex-spaces first-pos ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)