		Search-engine friendly clone of the ACL2 documentation.

Compustate

Make-compustate

Basic constructor macro for compustate structures.

Syntax

(make-compustate [:static <static>] 
                 [:frames <frames>] 
                 [:heap <heap>])

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

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

Definition

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

Macro: make-compustate

(defmacro make-compustate (&rest args)
  (std::make-aggregate 'compustate
                       args '((:static) (:frames) (:heap))
                       'make-compustate
                       nil))

Function: compustate

(defun compustate (static frames heap)
  (declare (xargs :guard (and (scopep static)
                              (frame-listp frames)
                              (heapp heap))))
  (declare (xargs :guard t))
  (let ((__function__ 'compustate))
    (declare (ignorable __function__))
    (b* ((static (mbe :logic (scope-fix static)
                      :exec static))
         (frames (mbe :logic (frame-list-fix frames)
                      :exec frames))
         (heap (mbe :logic (heap-fix heap)
                    :exec heap)))
      (list (cons 'static static)
            (cons 'frames frames)
            (cons 'heap heap)))))