Basic constructor macro for svtv*-phase structures.
(make-svtv*-phase [:label <label>] [:inputs <inputs>] [:overrides <overrides>] [:outputs <outputs>])
This is the usual way to construct svtv*-phase structures. It simply conses together a structure with the specified fields.
This macro generates a new svtv*-phase structure from scratch. See also change-svtv*-phase, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-svtv*-phase (&rest args) (std::make-aggregate 'svtv*-phase args '((:label quote acl2::?) (:inputs) (:overrides) (:outputs)) 'make-svtv*-phase nil))
Function:
(defun svtv*-phase (label inputs overrides outputs) (declare (xargs :guard (and (symbolp label) (svtv*-input-alist-p inputs) (svtv*-input-alist-p overrides) (svtv*-output-alist-p outputs)))) (declare (xargs :guard t)) (let ((__function__ 'svtv*-phase)) (declare (ignorable __function__)) (b* ((label (mbe :logic (acl2::symbol-fix label) :exec label)) (inputs (mbe :logic (svtv*-input-alist-fix inputs) :exec inputs)) (overrides (mbe :logic (svtv*-input-alist-fix overrides) :exec overrides)) (outputs (mbe :logic (svtv*-output-alist-fix outputs) :exec outputs))) (list label inputs overrides outputs))))