		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-translation-unit

Parse a translation unit.

Signature
(parse-translation-unit parstate) → (mv erp tunit new-parstate)
Arguments: parstate — Guard (parstatep parstate).
Returns: tunit — Type (transunitp tunit).; new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

This is called, by parse-file, on the initial parsing state, which contains all the file data bytes. We parse one or more external declarations, consistently with the grammar.

We also ensure that the file ends in new-line, as prescribed in [C:5.1.1.2/2]. We check that the end-of-file position, returned by parse-external-declaration-list, is at column 0: this means that, since the file is not empty, the last character is a new-line, otherwise that position would be at a non-zero column.

Definitions and Theorems

Function: parse-translation-unit

(defun parse-translation-unit (parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (parstatep parstate)))
  (let ((__function__ 'parse-translation-unit))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-transunit) parstate)
         ((erp extdecls & eof-pos parstate)
          (parse-external-declaration-list parstate))
         ((unless (= (position->column eof-pos) 0))
          (reterr (msg "The file does not end in new-line."))))
      (retok (transunit extdecls) parstate))))

Theorem: transunitp-of-parse-translation-unit.tunit

(defthm transunitp-of-parse-translation-unit.tunit
  (b* (((mv acl2::?erp ?tunit ?new-parstate)
        (parse-translation-unit parstate)))
    (transunitp tunit))
  :rule-classes :rewrite)

Theorem: parstatep-of-parse-translation-unit.new-parstate

(defthm parstatep-of-parse-translation-unit.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?tunit ?new-parstate)
                 (parse-translation-unit parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-translation-unit-uncond

(defthm parsize-of-parse-translation-unit-uncond
  (b* (((mv acl2::?erp ?tunit ?new-parstate)
        (parse-translation-unit parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-parse-translation-unit-cond

(defthm parsize-of-parse-translation-unit-cond
  (b* (((mv acl2::?erp ?tunit ?new-parstate)
        (parse-translation-unit parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)