Basic constructor macro for prof-entry structures.
(make-prof-entry [:name <name>] [:tries-succ <tries-succ>] [:tries-fail <tries-fail>] [:frames-succ <frames-succ>] [:frames-fail <frames-fail>])
This is the usual way to construct prof-entry structures. It simply conses together a structure with the specified fields.
This macro generates a new prof-entry structure from scratch. See also change-prof-entry, which can "change" an existing structure, instead.
This is an ordinary
(defmacro make-prof-entry (&rest args) (std::make-aggregate 'prof-entry args '((:name) (:tries-succ) (:tries-fail) (:frames-succ) (:frames-fail)) 'make-prof-entry nil))
(defun prof-entry (name tries-succ tries-fail frames-succ frames-fail) (declare (xargs :guard (and (natp tries-succ) (natp tries-fail) (natp frames-succ) (natp frames-fail)))) (declare (xargs :guard t)) (let ((__function__ 'prof-entry)) (declare (ignorable __function__)) (b* ((tries-succ (mbe :logic (nfix tries-succ) :exec tries-succ)) (tries-fail (mbe :logic (nfix tries-fail) :exec tries-fail)) (frames-succ (mbe :logic (nfix frames-succ) :exec frames-succ)) (frames-fail (mbe :logic (nfix frames-fail) :exec frames-fail))) (list name tries-succ tries-fail frames-succ frames-fail))))