		Search-engine friendly clone of the ACL2 documentation.

Svex-apply

Svex-apply-cases

Generates the main case statement for svex-apply.

Macro: svex-apply-cases

(defmacro svex-apply-cases (fn args)
  (cons 'case
        (cons fn
              (svex-apply-cases-fn args *svex-op-table*))))

Definitions and Theorems

Function: svex-apply-collect-args

(defun svex-apply-collect-args (n max argsvar)
  (let* ((n (nfix n)) (max (nfix max)))
    (if (zp (- max n))
        nil
      (cons (cons '4veclist-nth-safe
                  (cons n (cons argsvar 'nil)))
            (svex-apply-collect-args (+ 1 n)
                                     max argsvar)))))

Function: svex-apply-cases-fn

(defun svex-apply-cases-fn (argsvar optable)
 (b*
  (((when (atom optable))
    '((otherwise
           (or (raise "Attempting to apply unknown function ~x0~%"
                      fn)
               (4vec-x)))))
   ((list sym fn args) (car optable))
   (call
    (cons
     'mbe
     (cons
      ':logic
      (cons
       (cons fn
             (svex-apply-collect-args 0 (len args)
                                      argsvar))
       (cons
        ':exec
        (cons
         (cons
          'let
          (cons
           (cons
            (cons
             'arity-check
             (cons
              (cons
               'or
               (cons
                (cons 'eql
                      (cons '(len args)
                            (cons (len args) 'nil)))
                (cons
                 (cons
                  'raise
                  (cons
                   '"Improper arity for ~x0: expected ~x1 arguments but found ~x2.~%"
                   (cons (cons 'quote (cons sym 'nil))
                         (cons (cons 'quote (cons (len args) 'nil))
                               '((len args))))))
                 'nil)))
              'nil))
            'nil)
           (cons '(declare (ignore arity-check))
                 (cons (cons fn
                             (svex-apply-collect-args 0 (len args)
                                                      argsvar))
                       'nil))))
         'nil)))))))
  (cons (cons sym (cons call 'nil))
        (svex-apply-cases-fn argsvar (cdr optable)))))