• Top

• Sv::vl-moddb.lisp

Svcall-join

Signature

(svcall-join operator args) → svex

Arguments

args — Guard (sv::svexlist-p args).

Returns

svex — Type (sv::svex-p svex).

Definitions and Theorems

Function: svcall-join

(defun svcall-join (operator args)
  (declare (xargs :guard (sv::svexlist-p args)))
  (declare (xargs :guard (and (assoc operator sv::*svex-op-table*)
                              (consp args))))
  (let ((__function__ 'svcall-join))
    (declare (ignorable __function__))
    (if (atom (cdr args))
        (sv::svex-fix (car args))
      (sv::svex-call operator
                     (list (car args)
                           (svcall-join operator (cdr args)))))))

Theorem: svex-p-of-svcall-join

(defthm svex-p-of-svcall-join
  (b* ((svex (svcall-join operator args)))
    (sv::svex-p svex))
  :rule-classes :rewrite)

Theorem: vars-of-svcall-join

(defthm vars-of-svcall-join
  (b* ((?svex (svcall-join operator args)))
    (implies (not (member v (sv::svexlist-vars args)))
             (not (member v (sv::svex-vars svex))))))

Theorem: svcall-join-of-svexlist-fix-args

(defthm svcall-join-of-svexlist-fix-args
  (equal (svcall-join operator (sv::svexlist-fix args))
         (svcall-join operator args)))

Theorem: svcall-join-svexlist-equiv-congruence-on-args

(defthm svcall-join-svexlist-equiv-congruence-on-args
  (implies (sv::svexlist-equiv args args-equiv)
           (equal (svcall-join operator args)
                  (svcall-join operator args-equiv)))
  :rule-classes :congruence)