Raw constructor for machine-statep structures.
Syntax:
(machine-state gas-available pc memory active-words stack)
This is the lowest-level constructor for machine-statep structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-machine-state or change-machine-state instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The machine-statep structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-machine-state instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun machine-state (gas-available pc memory active-words stack) (declare (xargs :guard (and (natp gas-available) (natp pc) (memoryp memory) (stackp stack)))) (cons (cons 'gas-available gas-available) (cons (cons 'pc pc) (cons (cons 'memory memory) (cons (cons 'active-words active-words) (cons (cons 'stack stack) nil))))))