		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-transform

Signature
(check-transform transform ctxt) → (mv err? obligs)
Arguments: transform — Guard (transformp transform).; ctxt — Guard (contextp ctxt).
Returns: obligs — Type (proof-obligation-listp obligs).

Definitions and Theorems

Function: check-transform

(defun check-transform (transform ctxt)
 (declare (xargs :guard (and (transformp transform)
                             (contextp ctxt))))
 (let ((__function__ 'check-transform))
   (declare (ignorable __function__))
   (b*
     (((transform transfm) transform)
      (transfm-name transfm.transform-name)
      (arg-info (assoc-equal transfm-name
                             *transform-argument-table*))
      ((unless arg-info)
       (mv (list :unsupported-transform transfm-name)
           nil))
      (default-arg-info
           (assoc-equal transfm-name
                        *transform-argument-defaults-table*))
      (fn-def (get-function-definition transfm.old-function-name
                                       (context->tops ctxt)))
      ((unless fn-def)
       (mv (list :function-not-found
                 (identifier->name transfm.old-function-name))
           nil))
      (new-fn-def (get-function-definition transfm.new-function-name
                                           (context->tops ctxt)))
      ((when new-fn-def)
       (mv (list :function-already-defined
                 (identifier->name transfm.new-function-name))
           nil))
      (err? (check-transform-args transfm.arguments (cdr arg-info)
                                  (cdr default-arg-info)
                                  ctxt))
      ((when err?) (mv err? nil)))
     (mv nil nil))))

Theorem: proof-obligation-listp-of-check-transform.obligs

(defthm proof-obligation-listp-of-check-transform.obligs
  (b* (((mv ?err? ?obligs)
        (check-transform transform ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-transform-of-transform-fix-transform

(defthm check-transform-of-transform-fix-transform
  (equal (check-transform (transform-fix transform)
                          ctxt)
         (check-transform transform ctxt)))

Theorem: check-transform-transform-equiv-congruence-on-transform

(defthm check-transform-transform-equiv-congruence-on-transform
  (implies (transform-equiv transform transform-equiv)
           (equal (check-transform transform ctxt)
                  (check-transform transform-equiv ctxt)))
  :rule-classes :congruence)

Theorem: check-transform-of-context-fix-ctxt

(defthm check-transform-of-context-fix-ctxt
  (equal (check-transform transform (context-fix ctxt))
         (check-transform transform ctxt)))

Theorem: check-transform-context-equiv-congruence-on-ctxt

(defthm check-transform-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (check-transform transform ctxt)
                  (check-transform transform ctxt-equiv)))
  :rule-classes :congruence)