		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))))))))