		Search-engine friendly clone of the ACL2 documentation.

Asm-input

Make-asm-input

Basic constructor macro for asm-input structures.

Syntax

(make-asm-input [:name <name>] 
                [:constraint <constraint>] 
                [:rvalue <rvalue>])

This is the usual way to construct asm-input structures. It simply conses together a structure with the specified fields.

This macro generates a new asm-input structure from scratch. See also change-asm-input, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-asm-input

(defmacro make-asm-input (&rest args)
  (std::make-aggregate 'asm-input
                       args '((:name) (:constraint) (:rvalue))
                       'make-asm-input
                       nil))

Function: asm-input

(defun asm-input (name constraint rvalue)
  (declare (xargs :guard (and (ident-optionp name)
                              (stringlit-listp constraint)
                              (exprp rvalue))))
  (declare (xargs :guard t))
  (b* ((name (mbe :logic (ident-option-fix name)
                  :exec name))
       (constraint (mbe :logic (stringlit-list-fix constraint)
                        :exec constraint))
       (rvalue (mbe :logic (expr-fix rvalue)
                    :exec rvalue)))
    (cons name (cons constraint rvalue))))