		Search-engine friendly clone of the ACL2 documentation.

Svex

Svcall-rw

Safely construct an svex for a function call, with rewriting.

(call svcall-rw) constructs an svex that is equivalent to the application of fn to the given args. This macro is ``safe'' in that, at compile time, it ensures that fn is one of the known functions and that it is being given the right number of arguments.

Macro: svcall-rw

(defmacro svcall-rw (fn &rest args)
          (svcall-rw-fn fn args))

Definitions and Theorems

Function: svcall-rw-fn

(defun
   svcall-rw-fn (fn args)
   (declare (xargs :guard t))
   (b* ((look (assoc fn *svex-op-table*))
        ((unless look)
         (er hard? 'svcall
             "Svex function doesn't exist: ~x0" fn))
        (formals (third look))
        ((unless (eql (len formals) (len args)))
         (er hard? 'svcall
             "Wrong arity for call of ~x0" fn)))
       (cons 'svex-rewrite-fncall
             (cons '1000
                   (cons '-1
                         (cons (cons 'quote (cons fn 'nil))
                               (cons (cons 'list args) '(t t))))))))