		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-svex-eval-metafun

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

Definitions and Theorems

Function: svdecomp-svex-eval-metafun

(defun svdecomp-svex-eval-metafun (x)
 (declare (xargs :guard (pseudo-termp x)))
 (let ((__function__ 'svdecomp-svex-eval-metafun))
  (declare (ignorable __function__))
  (b*
   (((acl2::unless-match x (svex-eval '(:? svex) (:? env)))
     (cw
      "svdecomp-svex-eval-meta failed, probably running on non-concrete svex~%")
     x)
    ((unless (svex-p svex))
     (cw
      "svdecomp-svex-eval-meta failed because the svex was not svex-p~%")
     x)
    ((mv err symenv)
     (map-alist-term-keys-to-val-terms env))
    ((when err)
     (cw
      "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%"
      err)
     x)
    ((mv newsvexlist newenv)
     (svdecomp-normalize-svexlist-eval (list svex)
                                       symenv 10)))
   (cons 'svex-eval
         (cons (cons 'quote
                     (cons (car newsvexlist) 'nil))
               (cons (svdecomp-symenv->term newenv)
                     'nil))))))

Theorem: pseudo-termp-of-svdecomp-svex-eval-metafun

(defthm pseudo-termp-of-svdecomp-svex-eval-metafun
  (implies (and (pseudo-termp x))
           (b* ((newx (svdecomp-svex-eval-metafun x)))
             (pseudo-termp newx)))
  :rule-classes :rewrite)

Theorem: svdecomp-svex-eval-meta

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