		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Svex-apply

Apply an svex function to some 4vec arguments.

Signature
(svex-apply fn args) → result
Arguments: fn — Name of the function to apply.
Guard (fnsym-p fn).; args — Arguments to apply it to.
Guard (4veclist-p args).
Returns: result — Result of applying the function.
Type (4vec-p result).

This function captures function application for svex-eval, using a big case statement on the fn to execute.

SVEX uses a fixed language of known functions with fixed arities. If we are given a known function of proper arity, we execute the corresponding 4vec operation on its arguments.

Attempting to apply any unknown function produces an all-X result in the logic, and causes a run-time error during execution.
Applying a function to the wrong number of arguments produces an all-X result in the logic, and causes a run-time error during execution.

Definitions and Theorems

Function: svex-apply

(defun svex-apply (fn args)
  (declare (xargs :guard (and (fnsym-p fn) (4veclist-p args))))
  (let ((__function__ 'svex-apply))
    (declare (ignorable __function__))
    (let* ((fn (mbe :exec fn :logic (fnsym-fix fn)))
           (args (mbe :logic (4veclist-fix args)
                      :exec args)))
      (svex-apply-cases fn args))))

Theorem: 4vec-p-of-svex-apply

(defthm 4vec-p-of-svex-apply
  (b* ((result (svex-apply fn args)))
    (4vec-p result))
  :rule-classes :rewrite)

Theorem: svex-apply-of-fnsym-fix-fn

(defthm svex-apply-of-fnsym-fix-fn
  (equal (svex-apply (fnsym-fix fn) args)
         (svex-apply fn args)))

Theorem: svex-apply-fnsym-equiv-congruence-on-fn

(defthm svex-apply-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-apply fn args)
                  (svex-apply fn-equiv args)))
  :rule-classes :congruence)

Theorem: svex-apply-of-4veclist-fix-args

(defthm svex-apply-of-4veclist-fix-args
  (equal (svex-apply fn (4veclist-fix args))
         (svex-apply fn args)))

Theorem: svex-apply-4veclist-equiv-congruence-on-args

(defthm svex-apply-4veclist-equiv-congruence-on-args
  (implies (4veclist-equiv args args-equiv)
           (equal (svex-apply fn args)
                  (svex-apply fn args-equiv)))
  :rule-classes :congruence)

Subtopics

Svex-apply-cases: Generates the main case statement for svex-apply.
Svex-apply-monotonocity: svex-apply is almost always monotonic :-(