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