		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-compute-masks

Signature
(svexlist-compute-masks x mask-al) → mask-al1
Arguments: x — Guard (svexlist-p x).; mask-al — Guard (svex-mask-alist-p mask-al).
Returns: mask-al1 — Type (svex-mask-alist-p mask-al1).

Definitions and Theorems

Function: svexlist-compute-masks

(defun svexlist-compute-masks (x mask-al)
  (declare (xargs :guard (and (svexlist-p x)
                              (svex-mask-alist-p mask-al))))
  (let ((__function__ 'svexlist-compute-masks))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mbe :logic (svex-mask-alist-fix mask-al)
               :exec mask-al))
         (first (car x))
         ((when (not (eq (svex-kind first) :call)))
          (svexlist-compute-masks (cdr x)
                                  mask-al))
         (mask (svex-mask-lookup first mask-al))
         ((when (sparseint-equal mask 0))
          (svexlist-compute-masks (cdr x)
                                  mask-al))
         (args (svex-call->args first))
         (argmasks (svex-argmasks mask (svex-call->fn first)
                                  args))
         (mask-al (svex-args-apply-masks args argmasks mask-al)))
      (svexlist-compute-masks (cdr x)
                              mask-al))))

Theorem: svex-mask-alist-p-of-svexlist-compute-masks

(defthm svex-mask-alist-p-of-svexlist-compute-masks
  (b* ((mask-al1 (svexlist-compute-masks x mask-al)))
    (svex-mask-alist-p mask-al1))
  :rule-classes :rewrite)

Theorem: svexlist-compute-masks-lookup-subsumes-prev-lookup

(defthm svexlist-compute-masks-lookup-subsumes-prev-lookup
  (4vmask-subsumes
       (svex-mask-lookup y (svexlist-compute-masks x mask-al))
       (svex-mask-lookup y mask-al)))

Theorem: svexlist-compute-masks-lookup-when-all

(defthm svexlist-compute-masks-lookup-when-all
  (implies
       (sparseint-equal (svex-mask-lookup y mask-al)
                        -1)
       (sparseint-equal
            (svex-mask-lookup y (svexlist-compute-masks x mask-al))
            -1)))

Theorem: svexlist-compute-masks-lookup-when-neg1

(defthm svexlist-compute-masks-lookup-when-neg1
 (implies
      (equal (svex-mask-lookup y mask-al) -1)
      (equal (svex-mask-lookup y (svexlist-compute-masks x mask-al))
             -1)))

Theorem: svexlist-compute-masks-lookups-subsume-prev-lookups

(defthm svexlist-compute-masks-lookups-subsume-prev-lookups
  (4vmasklist-subsumes
       (svex-argmasks-lookup y (svexlist-compute-masks x mask-al))
       (svex-argmasks-lookup y mask-al)))

Theorem: svexlist-compute-masks-partly-complete

(defthm svexlist-compute-masks-partly-complete
  (implies (and (svex-mask-alist-partly-complete x mask-al)
                (svexlist-toposort-p x))
           (svex-mask-alist-partly-complete
                nil
                (svexlist-compute-masks x mask-al))))

Theorem: svexlist-compute-masks-of-svexlist-fix-x

(defthm svexlist-compute-masks-of-svexlist-fix-x
  (equal (svexlist-compute-masks (svexlist-fix x)
                                 mask-al)
         (svexlist-compute-masks x mask-al)))

Theorem: svexlist-compute-masks-svexlist-equiv-congruence-on-x

(defthm svexlist-compute-masks-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-compute-masks x mask-al)
                  (svexlist-compute-masks x-equiv mask-al)))
  :rule-classes :congruence)

Theorem: svexlist-compute-masks-of-svex-mask-alist-fix-mask-al

(defthm svexlist-compute-masks-of-svex-mask-alist-fix-mask-al
  (equal (svexlist-compute-masks x (svex-mask-alist-fix mask-al))
         (svexlist-compute-masks x mask-al)))

Theorem: svexlist-compute-masks-svex-mask-alist-equiv-congruence-on-mask-al

(defthm
 svexlist-compute-masks-svex-mask-alist-equiv-congruence-on-mask-al
 (implies (svex-mask-alist-equiv mask-al mask-al-equiv)
          (equal (svexlist-compute-masks x mask-al)
                 (svexlist-compute-masks x mask-al-equiv)))
 :rule-classes :congruence)