		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-filter-merges

Group up occurrences into those to be merged (into a merge alist) and those not to be merged (into a regular list).

Signature
(vl-lucid-filter-merges x merge regular) → (mv merge regular)
Arguments: x — Occurrences to filter.
Guard (vl-lucidocclist-p x).; merge — Accumulator for occs to merge (always blocks, function decls, tasks.).
Guard (vl-lucidmergealist-p merge).; regular — Accumulator for occs not to merge (continuous assigns, instances).
Guard (vl-lucidocclist-p regular).
Returns: merge — Type (vl-lucidmergealist-p merge).; regular — Type (vl-lucidocclist-p regular).

Definitions and Theorems

Function: vl-lucid-filter-merges

(defun vl-lucid-filter-merges (x merge regular)
  (declare (xargs :guard (and (vl-lucidocclist-p x)
                              (vl-lucidmergealist-p merge)
                              (vl-lucidocclist-p regular))))
  (let ((__function__ 'vl-lucid-filter-merges))
    (declare (ignorable __function__))
    (b* ((x (vl-lucidocclist-fix x))
         (merge (vl-lucidmergealist-fix merge))
         (regular (vl-lucidocclist-fix regular))
         ((when (atom x)) (mv merge regular))
         (occ1 (car x))
         (ctx1 (vl-lucidocc->ctx occ1))
         (elem1 (vl-lucidctx->elem ctx1))
         (mergep (or (mbe :logic (vl-fundecl-p elem1)
                          :exec (eq (tag elem1) :vl-fundecl))
                     (mbe :logic (vl-taskdecl-p elem1)
                          :exec (eq (tag elem1) :vl-taskdecl))
                     (mbe :logic (vl-always-p elem1)
                          :exec (eq (tag elem1) :vl-always))))
         ((unless mergep)
          (vl-lucid-filter-merges (cdr x)
                                  merge (cons (car x) regular)))
         (others (cdr (hons-get ctx1 merge)))
         (merge (hons-acons ctx1 (cons occ1 others)
                            merge)))
      (vl-lucid-filter-merges (cdr x)
                              merge regular))))

Theorem: vl-lucidmergealist-p-of-vl-lucid-filter-merges.merge

(defthm vl-lucidmergealist-p-of-vl-lucid-filter-merges.merge
  (b* (((mv common-lisp::?merge ?regular)
        (vl-lucid-filter-merges x merge regular)))
    (vl-lucidmergealist-p merge))
  :rule-classes :rewrite)

Theorem: vl-lucidocclist-p-of-vl-lucid-filter-merges.regular

(defthm vl-lucidocclist-p-of-vl-lucid-filter-merges.regular
  (b* (((mv common-lisp::?merge ?regular)
        (vl-lucid-filter-merges x merge regular)))
    (vl-lucidocclist-p regular))
  :rule-classes :rewrite)

Theorem: vl-lucid-filter-merges-of-vl-lucidocclist-fix-x

(defthm vl-lucid-filter-merges-of-vl-lucidocclist-fix-x
  (equal (vl-lucid-filter-merges (vl-lucidocclist-fix x)
                                 merge regular)
         (vl-lucid-filter-merges x merge regular)))

Theorem: vl-lucid-filter-merges-vl-lucidocclist-equiv-congruence-on-x

(defthm vl-lucid-filter-merges-vl-lucidocclist-equiv-congruence-on-x
  (implies (vl-lucidocclist-equiv x x-equiv)
           (equal (vl-lucid-filter-merges x merge regular)
                  (vl-lucid-filter-merges x-equiv merge regular)))
  :rule-classes :congruence)

Theorem: vl-lucid-filter-merges-of-vl-lucidmergealist-fix-merge

(defthm vl-lucid-filter-merges-of-vl-lucidmergealist-fix-merge
  (equal (vl-lucid-filter-merges x (vl-lucidmergealist-fix merge)
                                 regular)
         (vl-lucid-filter-merges x merge regular)))

Theorem: vl-lucid-filter-merges-vl-lucidmergealist-equiv-congruence-on-merge

(defthm
 vl-lucid-filter-merges-vl-lucidmergealist-equiv-congruence-on-merge
 (implies (vl-lucidmergealist-equiv merge merge-equiv)
          (equal (vl-lucid-filter-merges x merge regular)
                 (vl-lucid-filter-merges x merge-equiv regular)))
 :rule-classes :congruence)

Theorem: vl-lucid-filter-merges-of-vl-lucidocclist-fix-regular

(defthm vl-lucid-filter-merges-of-vl-lucidocclist-fix-regular
 (equal
      (vl-lucid-filter-merges x merge (vl-lucidocclist-fix regular))
      (vl-lucid-filter-merges x merge regular)))

Theorem: vl-lucid-filter-merges-vl-lucidocclist-equiv-congruence-on-regular

(defthm
 vl-lucid-filter-merges-vl-lucidocclist-equiv-congruence-on-regular
 (implies (vl-lucidocclist-equiv regular regular-equiv)
          (equal (vl-lucid-filter-merges x merge regular)
                 (vl-lucid-filter-merges x merge regular-equiv)))
 :rule-classes :congruence)