		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-ext-declon

Validate an external declaration.

Signature
(valid-ext-declon edecl table ienv) → (mv erp new-edecl new-table)
Arguments: edecl — Guard (ext-declonp edecl).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-edecl — Type (ext-declonp new-edecl).; new-table — Type (valid-tablep new-table).

For now we do not do anything with assembler statements. The empty external declaration is always valid. We check that declarations contain no return statements.

Definitions and Theorems

Function: valid-ext-declon

(defun valid-ext-declon (edecl table ienv)
 (declare (xargs :guard (and (ext-declonp edecl)
                             (valid-tablep table)
                             (ienvp ienv))))
 (declare (xargs :guard (ext-declon-unambp edecl)))
 (b* (((reterr)
       (irr-ext-declon)
       (irr-valid-table)))
  (ext-declon-case
   edecl :fundef
   (b* (((erp new-fundef table)
         (valid-fundef edecl.fundef table ienv)))
     (retok (ext-declon-fundef new-fundef)
            table))
   :declon
   (b*
    (((erp new-decl types table)
      (valid-declon edecl.declon table ienv))
     ((unless (emptyp types))
      (retmsg$
       "The top-level declaration ~x0 ~
                           contains return statements."
       edecl.declon)))
    (retok (ext-declon-declon new-decl)
           table))
   :empty (retok (ext-declon-empty)
                 (valid-table-fix table))
   :asm (retok (ext-declon-fix edecl)
               (valid-table-fix table)))))

Theorem: maybe-msgp-of-valid-ext-declon.erp

(defthm maybe-msgp-of-valid-ext-declon.erp
  (b* (((mv acl2::?erp ?new-edecl ?new-table)
        (valid-ext-declon edecl table ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: ext-declonp-of-valid-ext-declon.new-edecl

(defthm ext-declonp-of-valid-ext-declon.new-edecl
  (b* (((mv acl2::?erp ?new-edecl ?new-table)
        (valid-ext-declon edecl table ienv)))
    (ext-declonp new-edecl))
  :rule-classes :rewrite)

Theorem: valid-tablep-of-valid-ext-declon.new-table

(defthm valid-tablep-of-valid-ext-declon.new-table
  (b* (((mv acl2::?erp ?new-edecl ?new-table)
        (valid-ext-declon edecl table ienv)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: ext-declon-unambp-of-valid-ext-declon

(defthm ext-declon-unambp-of-valid-ext-declon
  (implies (ext-declon-unambp edecl)
           (b* (((mv acl2::?erp ?new-edecl ?new-table)
                 (valid-ext-declon edecl table ienv)))
             (implies (not erp)
                      (ext-declon-unambp new-edecl)))))

Theorem: valid-ext-declon-of-ext-declon-fix-edecl

(defthm valid-ext-declon-of-ext-declon-fix-edecl
  (equal (valid-ext-declon (ext-declon-fix edecl)
                           table ienv)
         (valid-ext-declon edecl table ienv)))

Theorem: valid-ext-declon-ext-declon-equiv-congruence-on-edecl

(defthm valid-ext-declon-ext-declon-equiv-congruence-on-edecl
  (implies (ext-declon-equiv edecl edecl-equiv)
           (equal (valid-ext-declon edecl table ienv)
                  (valid-ext-declon edecl-equiv table ienv)))
  :rule-classes :congruence)

Theorem: valid-ext-declon-of-valid-table-fix-table

(defthm valid-ext-declon-of-valid-table-fix-table
  (equal (valid-ext-declon edecl (valid-table-fix table)
                           ienv)
         (valid-ext-declon edecl table ienv)))

Theorem: valid-ext-declon-valid-table-equiv-congruence-on-table

(defthm valid-ext-declon-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-ext-declon edecl table ienv)
                  (valid-ext-declon edecl table-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-ext-declon-of-ienv-fix-ienv

(defthm valid-ext-declon-of-ienv-fix-ienv
  (equal (valid-ext-declon edecl table (ienv-fix ienv))
         (valid-ext-declon edecl table ienv)))

Theorem: valid-ext-declon-ienv-equiv-congruence-on-ienv

(defthm valid-ext-declon-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-ext-declon edecl table ienv)
                  (valid-ext-declon edecl table ienv-equiv)))
  :rule-classes :congruence)