defevaluator-fast - ACL2 Book

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

other

(program)

other

(defxdoc defevaluator-fast
  :parents (defevaluator)
  :short "Formerly a faster alternative to @(see defevaluator), now just an alias."
  :long "<p>See @(see defevaluator).  This used to be a higher-performance
reimplementation of defevaluator, but then defevaluator was changed to do
basically the same as this function, so we then changed this to just be an
alias for defevaluator.</p>")

defevaluator-fastmacro

(defmacro defevaluator-fast
  (&rest args)
  `(defevaluator . ,ARGS))

other

(logic)

local

(local (progn (defevaluator-fast foo-ev
      foo-ev-lst
      ((xxxjoin fn args) (integer-abs x)
        (or-macro lst)
        (and-macro lst)
        (list-macro lst)
        (true-listp x)
        (eq x y)
        (rewrite-equiv x)
        (hide x)
        (not p)
        (implies p q)
        (booleanp x)
        (xor p q)
        (iff p q)
        (o< x y)
        (o-p x)
        (symbolp x)
        (symbol-package-name x)
        (symbol-name x)
        (stringp x)
        (realpart x)
        (rationalp x)
        (pkg-witness pkg)
        (numerator x)
        (intern-in-package-of-symbol str sym)
        (integerp x)
        (imagpart x)
        (if x
          y
          z)
        (equal x y)
        (denominator x)
        (consp x)
        (cons x y)
        (coerce x y)
        (complex-rationalp x)
        (complex x y)
        (code-char x)
        (characterp x)
        (char-code x)
        (cdr x)
        (car x)
        (< x y)
        (unary-/ x)
        (unary-- x)
        (binary-+ x y)
        (binary-* x y)
        (bad-atom<= x y)
        (acl2-numberp x)))
    (defun stupid-cp (x) (list x))
    (defthm stupid-cp-correct
      (implies (and (pseudo-term-listp cl)
          (alistp a)
          (foo-ev (conjoin-clauses (stupid-cp cl)) a))
        (foo-ev (disjoin cl) a))
      :rule-classes :clause-processor)))

local

(local (progn (defevaluator-fast foo2-ev
      foo2-ev-lst
      ((xxxjoin fn args) (integer-abs x)
        (or-macro lst)
        (and-macro lst)
        (list-macro lst)
        (true-listp x)
        (eq x y)
        (rewrite-equiv x)
        (hide x)
        (not p)
        (implies p q)
        (booleanp x)
        (xor p q)
        (iff p q)
        (o< x y)
        (o-p x)
        (symbolp x)
        (symbol-package-name x)
        (symbol-name x)
        (stringp x)
        (realpart x)
        (rationalp x)
        (pkg-witness pkg)
        (numerator x)
        (intern-in-package-of-symbol str sym)
        (integerp x)
        (imagpart x)
        (if x
          y
          z)
        (equal x y)
        (denominator x)
        (consp x)
        (cons x y)
        (coerce x y)
        (complex-rationalp x)
        (complex x y)
        (code-char x)
        (characterp x)
        (char-code x)
        (cdr x)
        (car x)
        (< x y)
        (unary-/ x)
        (unary-- x)
        (binary-+ x y)
        (binary-* x y)
        (bad-atom<= x y)
        (acl2-numberp x))
      :namedp t)
    (defun stupid-cp2 (x) (list x))
    (defthm stupid-cp2-correct
      (implies (and (pseudo-term-listp cl)
          (alistp a)
          (foo2-ev (conjoin-clauses (stupid-cp cl)) a))
        (foo2-ev (disjoin cl) a))
      :rule-classes :clause-processor)))

mk-defeval-entriesfunction

(defun mk-defeval-entries
  (fns world)
  (if (atom fns)
    nil
    (let ((formals (getprop (car fns) 'formals nil 'current-acl2-world world)))
      (cons (cons (car fns) formals)
        (mk-defeval-entries (cdr fns) world)))))