		Search-engine friendly clone of the ACL2 documentation.

Machine-statep

Make-machine-state

Constructor macro for machine-statep structures.

Syntax:

(make-machine-state [:gas-available <gas-available>] 
                    [:pc <pc>] 
                    [:memory <memory>] 
                    [:active-words <active-words>] 
                    [:stack <stack>])

This is our preferred way to construct machine-statep structures. It simply conses together a structure with the specified fields.

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

The machine-statep structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-machine-state instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-machine-state

(defmacro make-machine-state (&rest args)
  (std::make-aggregate 'machine-state
                       args
                       '((:gas-available)
                         (:pc)
                         (:memory)
                         (:active-words)
                         (:stack))
                       'make-machine-state
                       nil))