		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-extdecl

Validate an external declaration.

Signature
(valid-extdecl edecl table ienv) → (mv erp new-edecl new-table)
Arguments: edecl — Guard (extdeclp edecl).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-edecl — Type (extdeclp 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-extdecl

(defun valid-extdecl (edecl table ienv)
 (declare (xargs :guard (and (extdeclp edecl)
                             (valid-tablep table)
                             (ienvp ienv))))
 (declare (xargs :guard (extdecl-unambp edecl)))
 (let ((__function__ 'valid-extdecl))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-extdecl)
        (irr-valid-table)))
   (extdecl-case
    edecl :fundef
    (b* (((erp new-fundef table)
          (valid-fundef edecl.unwrap table ienv)))
      (retok (extdecl-fundef new-fundef)
             table))
    :decl
    (b*
     (((erp new-decl types table)
       (valid-decl edecl.unwrap table ienv))
      ((unless (emptyp types))
       (reterr
        (msg
         "The top-level declaration ~x0 ~
                               contains return statements."
         edecl.unwrap))))
     (retok (extdecl-decl new-decl) table))
    :empty (retok (extdecl-empty)
                  (valid-table-fix table))
    :asm (retok (extdecl-fix edecl)
                (valid-table-fix table))))))

Theorem: extdeclp-of-valid-extdecl.new-edecl

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

Theorem: valid-tablep-of-valid-extdecl.new-table

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

Theorem: extdecl-unambp-of-valid-extdecl

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

Theorem: valid-extdecl-of-extdecl-fix-edecl

(defthm valid-extdecl-of-extdecl-fix-edecl
  (equal (valid-extdecl (extdecl-fix edecl)
                        table ienv)
         (valid-extdecl edecl table ienv)))

Theorem: valid-extdecl-extdecl-equiv-congruence-on-edecl

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

Theorem: valid-extdecl-of-valid-table-fix-table

(defthm valid-extdecl-of-valid-table-fix-table
  (equal (valid-extdecl edecl (valid-table-fix table)
                        ienv)
         (valid-extdecl edecl table ienv)))

Theorem: valid-extdecl-valid-table-equiv-congruence-on-table

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

Theorem: valid-extdecl-of-ienv-fix-ienv

(defthm valid-extdecl-of-ienv-fix-ienv
  (equal (valid-extdecl edecl table (ienv-fix ienv))
         (valid-extdecl edecl table ienv)))

Theorem: valid-extdecl-ienv-equiv-congruence-on-ienv

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