Parse a translation unit.
(parse-translation-unit pstate) → (mv erp tunit new-pstate)
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.
Function:
(defun parse-translation-unit (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-translation-unit)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit) (irr-parstate)) ((erp extdecls & eof-pos pstate) (parse-external-declaration-list pstate)) ((unless (= (position->column eof-pos) 0)) (reterr (msg "The file does not end in new-line.")))) (retok (transunit extdecls) pstate))))
Theorem:
(defthm transunitp-of-parse-translation-unit.tunit (b* (((mv acl2::?erp ?tunit ?new-pstate) (parse-translation-unit pstate))) (transunitp tunit)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-translation-unit.new-pstate (b* (((mv acl2::?erp ?tunit ?new-pstate) (parse-translation-unit pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-translation-unit-uncond (b* (((mv acl2::?erp ?tunit ?new-pstate) (parse-translation-unit pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-translation-unit-cond (b* (((mv acl2::?erp ?tunit ?new-pstate) (parse-translation-unit pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)