		Search-engine friendly clone of the ACL2 documentation.

Svex

Svcall

Safely construct an svex for a function call.

(call svcall) just constructs an svex that applies 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

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

Definitions and Theorems

Function: svcall-fn

(defun svcall-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-call
                 (cons (cons 'quote (cons fn 'nil))
                       (cons (cons 'list args) 'nil)))))