		Search-engine friendly clone of the ACL2 documentation.

Flattening

Flatten-fundecl

Flatten a function declaration.

Signature
(flatten-fundecl decl env) → new-decl
Arguments: decl — Guard (fundeclp decl).; env — Guard (fenvp env).
Returns: new-decl — Type (fundecl-resultp new-decl).

The flattening environment passed to this ACL2 function is meant to consist of the known values of the constant parameters. We are not yet handling function specialization here (which is where these environments will be calculated).

Any case, given such an environment, the function declaration is flattened by flattening its body.

Definitions and Theorems

Function: flatten-fundecl

(defun flatten-fundecl (decl env)
  (declare (xargs :guard (and (fundeclp decl) (fenvp env))))
  (let ((__function__ 'flatten-fundecl))
    (declare (ignorable __function__))
    (b* (((fundecl decl) decl)
         ((okf new-body)
          (flatten-statement-list decl.body env)))
      (change-fundecl decl :body new-body))))

Theorem: fundecl-resultp-of-flatten-fundecl

(defthm fundecl-resultp-of-flatten-fundecl
  (b* ((new-decl (flatten-fundecl decl env)))
    (fundecl-resultp new-decl))
  :rule-classes :rewrite)

Theorem: flatten-fundecl-of-fundecl-fix-decl

(defthm flatten-fundecl-of-fundecl-fix-decl
  (equal (flatten-fundecl (fundecl-fix decl) env)
         (flatten-fundecl decl env)))

Theorem: flatten-fundecl-fundecl-equiv-congruence-on-decl

(defthm flatten-fundecl-fundecl-equiv-congruence-on-decl
  (implies (fundecl-equiv decl decl-equiv)
           (equal (flatten-fundecl decl env)
                  (flatten-fundecl decl-equiv env)))
  :rule-classes :congruence)

Theorem: flatten-fundecl-of-fenv-fix-env

(defthm flatten-fundecl-of-fenv-fix-env
  (equal (flatten-fundecl decl (fenv-fix env))
         (flatten-fundecl decl env)))

Theorem: flatten-fundecl-fenv-equiv-congruence-on-env

(defthm flatten-fundecl-fenv-equiv-congruence-on-env
  (implies (fenv-equiv env env-equiv)
           (equal (flatten-fundecl decl env)
                  (flatten-fundecl decl env-equiv)))
  :rule-classes :congruence)