		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-modulelist-edgesynth

Synthesize edge-triggered always blocks in a module list, perhaps adding some new, supporting modules.

Signature
(vl-modulelist-edgesynth x &key vecp) → new-x
Arguments: x — Guard (vl-modulelist-p x).
Returns: new-x — Type (and (vl-modulelist-p new-x) (no-duplicatesp-equal (vl-modulelist->names new-x))) , given the guard.

Definitions and Theorems

Function: vl-modulelist-edgesynth-fn

(defun vl-modulelist-edgesynth-fn (x vecp)
 (declare (xargs :guard (vl-modulelist-p x)))
 (let ((__function__ 'vl-modulelist-edgesynth))
  (declare (ignorable __function__))
  (b*
   ((dupes (duplicated-members (vl-modulelist->names x)))
    ((when dupes)
     (raise
      "Module names must be unique, but found multiple definitions ~
                of ~&0."
      dupes))
    ((mv new-x addmods)
     (vl-modulelist-edgesynth-aux x
                                  :vecp vecp))
    (all-mods (union (mergesort new-x)
                     (mergesort addmods)))
    (dupes (duplicated-members (vl-modulelist->names all-mods)))
    ((when dupes)
     (raise "Edgesynth caused a name collision: ~&0."
            dupes)))
   all-mods)))

Theorem: return-type-of-vl-modulelist-edgesynth

(defthm return-type-of-vl-modulelist-edgesynth
  (implies
       (and (force (vl-modulelist-p x)))
       (b* ((new-x (vl-modulelist-edgesynth-fn x vecp)))
         (and (vl-modulelist-p new-x)
              (no-duplicatesp-equal (vl-modulelist->names new-x)))))
  :rule-classes :rewrite)