magic-ev

(mutual-recursion (defun magic-ev
    (x alist state hard-errp aokp)
    (declare (xargs :guard (and (pseudo-termp x) (symbol-alistp alist))
        :verify-guards nil
        :stobjs state))
    (cond ((not x) (mv nil nil))
      ((atom x) (mv nil (cdr (assoc-eq x alist))))
      ((eq (car x) 'quote) (mv nil (cadr x)))
      ((consp (car x)) (b* (((mv err args) (magic-ev-lst (cdr x) alist state hard-errp aokp)) ((when err) (mv err args))
            (new-alist (pairlis$ (cadar x) args)))
          (magic-ev (caddar x) new-alist state hard-errp aokp)))
      ((eq (car x) 'if) (b* (((mv err test) (magic-ev (cadr x) alist state hard-errp aokp)) ((when err) (mv err test)))
          (if test
            (if (equal (cadr x) (caddr x))
              (mv nil test)
              (magic-ev (caddr x) alist state hard-errp aokp))
            (magic-ev (cadddr x) alist state hard-errp aokp))))
      (t (b* (((mv err args) (magic-ev-lst (cdr x) alist state hard-errp aokp)) ((when err) (mv err args))
            ((when (programp (car x) (w state))) (mv (msg "program mode: ~x0" (car x)) nil)))
          (magic-ev-fncall (car x) args state hard-errp aokp)))))
  (defun magic-ev-lst
    (x alist state hard-errp aokp)
    (declare (xargs :guard (and (pseudo-term-listp x) (symbol-alistp alist))
        :stobjs state))
    (if (endp x)
      (mv nil nil)
      (b* (((mv err first) (magic-ev (car x) alist state hard-errp aokp)) ((when err) (mv err first))
          ((mv err rest) (magic-ev-lst (cdr x) alist state hard-errp aokp))
          ((when err) (mv err rest)))
        (mv nil (cons first rest))))))