Basic constructor macro for sd-key structures.
(make-sd-key [:pat <pat>] [:index <index>] [:orig <orig>])
This is the usual way to construct sd-key structures. It simply conses together a structure with the specified fields.
This macro generates a new sd-key structure from scratch. See also change-sd-key, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-sd-key (&rest args) (std::make-aggregate 'sd-key args '((:pat) (:index) (:orig)) 'make-sd-key nil))
Function:
(defun sd-key (pat index orig) (declare (xargs :guard (and (stringp pat) (maybe-natp index) (stringp orig)))) (declare (xargs :guard t)) (let ((__function__ 'sd-key)) (declare (ignorable __function__)) (b* ((pat (mbe :logic (str-fix pat) :exec pat)) (index (mbe :logic (maybe-natp-fix index) :exec index)) (orig (mbe :logic (str-fix orig) :exec orig))) (cons :sd-key (cons pat (cons index orig))))))