		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-equal-svex-evals-metafun

Signature
(svdecomp-equal-svex-evals-metafun x mfc state) → newx
Arguments: x — Guard (pseudo-termp x).
Returns: newx — Type (pseudo-termp newx), given the guard.

Definitions and Theorems

Function: svdecomp-equal-svex-evals-metafun

(defun svdecomp-equal-svex-evals-metafun (x mfc state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (pseudo-termp x)))
 (declare (ignorable mfc))
 (let ((__function__ 'svdecomp-equal-svex-evals-metafun))
  (declare (ignorable __function__))
  (b*
   (((acl2::when-match x
                       (equal (svex-eval '(:? svex1) (:? env1))
                              (svex-eval '(:? svex2) (:? env2))))
     (cwtime
      (b*
       (((mv env1 env2)
         (mbe :logic (mv env1 env2)
              :exec
              (let ((pair (hons env1 env2)))
                (mv (car pair) (cdr pair)))))
        ((unless (and (svex-p svex1) (svex-p svex2)))
         (cw
          "svdecomp-svex-eval-meta failed because the svex was not svex-p~%")
         x)
        ((mv err symenv1)
         (map-alist-term-keys-to-val-terms env1))
        ((when err)
         (fmt-to-comment-window
          "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%"
          (cons (cons '#\0 err) 'nil)
          0 '(nil 8 10 nil)
          nil)
         x)
        ((mv err symenv2)
         (map-alist-term-keys-to-val-terms env2))
        ((when err)
         (cw
          "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%"
          err)
         x)
        ((mv newsvexlist1 newenv1)
         (cwtime (svdecomp-normalize-svexlist-eval (list svex1)
                                                   symenv1 10)
                 :mintime 1))
        ((mv newsvexlist2 newenv2)
         (cwtime (svdecomp-normalize-svexlist-eval (list svex2)
                                                   symenv2 10)
                 :mintime 1))
        (limit (svdecomp-get-rewrite-limit state))
        ((mv newsvexlist1 newsvexlist2)
         (cwtime (svexlists-rewrite-until-same
                      newsvexlist1 newsvexlist2 limit)
                 :mintime 1))
        (newsvex1 (nth 0 newsvexlist1))
        (newsvex2 (nth 0 newsvexlist2)))
       (if (hons-equal newenv1 newenv2)
           (cw "Environments are equal.~%")
         (cw "Environments differ~%"))
       (if (hons-equal newsvex1 newsvex2)
           (cw "Svexes are equal.~%")
         (cw "Svexes differ.~%"))
       (svdecomp-svex?-eval-compare-term
            newsvex1
            newsvex2 newenv1 newenv2 'svex-eval))
      :name svdecomp-equal-svex-evals-metafun)))
   x)))

Theorem: pseudo-termp-of-svdecomp-equal-svex-evals-metafun

(defthm pseudo-termp-of-svdecomp-equal-svex-evals-metafun
  (implies
       (and (state-p state) (pseudo-termp x))
       (b* ((newx (svdecomp-equal-svex-evals-metafun x mfc state)))
         (pseudo-termp newx)))
  :rule-classes :rewrite)

Theorem: svdecomp-equal-svex-evals-meta

(defthm svdecomp-equal-svex-evals-meta
 (equal (svdecomp-ev x a)
        (svdecomp-ev (svdecomp-equal-svex-evals-metafun x mfc state)
                     a))
 :rule-classes ((:meta :trigger-fns (equal))))