|
|
|---|
|
|
|
|---|
Basic constructor macro for ext-declon-asm structures.
(make-ext-declon-asm [:stmt <stmt>])
This is the usual way to construct ext-declon-asm structures. It simply conses together a structure with the specified fields.
This macro generates a new ext-declon-asm structure from scratch. See also change-ext-declon-asm, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-ext-declon-asm (&rest args) (std::make-aggregate 'ext-declon-asm args '((:stmt)) 'make-ext-declon-asm nil))
Function:
(defun ext-declon-asm (stmt) (declare (xargs :guard (asm-stmtp stmt))) (declare (xargs :guard t)) (b* ((stmt (mbe :logic (asm-stmt-fix stmt) :exec stmt))) (cons :asm stmt)))