		Search-engine friendly clone of the ACL2 documentation.

Inst

Make-inst

Basic constructor macro for inst structures.

Syntax

(make-inst [:mnemonic <mnemonic>] 
           [:opcode <opcode>] 
           [:operands <operands>] 
           [:fn <fn>] 
           [:excep <excep>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-inst

(defmacro make-inst (&rest args)
  (std::make-aggregate 'inst
                       args
                       '((:mnemonic)
                         (:opcode)
                         (:operands quote nil)
                         (:fn quote nil)
                         (:excep quote nil))
                       'make-inst
                       nil))

Function: inst

(defun inst (mnemonic opcode operands fn excep)
  (declare (xargs :guard (and (mnemonic-p mnemonic)
                              (strict-opcode-p opcode)
                              (maybe-operands-p operands)
                              (fn-desc-p fn)
                              (exception-desc-p excep))))
  (declare (xargs :guard t))
  (let ((__function__ 'inst))
    (declare (ignorable __function__))
    (b* ((mnemonic (mbe :logic (mnemonic-fix mnemonic)
                        :exec mnemonic))
         (opcode (mbe :logic (strict-opcode-fix opcode)
                      :exec opcode))
         (operands (mbe :logic (maybe-operands-fix operands)
                        :exec operands))
         (fn (mbe :logic (fn-desc-fix fn) :exec fn))
         (excep (mbe :logic (exception-desc-fix excep)
                     :exec excep)))
      (std::prod-cons
           (std::prod-cons mnemonic opcode)
           (std::prod-cons operands (std::prod-cons fn excep))))))