		Search-engine friendly clone of the ACL2 documentation.

Run-snippet-file-info

Make-run-snippet-file-info

Basic constructor macro for run-snippet-file-info structures.

Syntax

(make-run-snippet-file-info [:snip-info <snip-info>] 
                            [:input-addr <input-addr>] 
                            [:output-addr <output-addr>] 
                            [:input-channel <input-channel>] 
                            [:output-channel <output-channel>])

This is the usual way to construct run-snippet-file-info structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-run-snippet-file-info

(defmacro make-run-snippet-file-info (&rest args)
  (std::make-aggregate 'run-snippet-file-info
                       args
                       '((:snip-info)
                         (:input-addr)
                         (:output-addr)
                         (:input-channel)
                         (:output-channel))
                       'make-run-snippet-file-info
                       nil))

Function: run-snippet-file-info

(defun run-snippet-file-info
       (snip-info input-addr output-addr
                  input-channel output-channel)
 (declare (xargs :guard (and (run-snippet-info-p snip-info)
                             (canonical-address-p input-addr)
                             (canonical-address-p output-addr)
                             (symbolp input-channel)
                             (symbolp output-channel))))
 (declare (xargs :guard t))
 (let ((__function__ 'run-snippet-file-info))
  (declare (ignorable __function__))
  (b* ((snip-info (mbe :logic (run-snippet-info-fix snip-info)
                       :exec snip-info))
       (input-addr (mbe :logic (canonical-address-fix input-addr)
                        :exec input-addr))
       (output-addr (mbe :logic (canonical-address-fix output-addr)
                         :exec output-addr))
       (input-channel (mbe :logic (acl2::symbol-fix input-channel)
                           :exec input-channel))
       (output-channel (mbe :logic (acl2::symbol-fix output-channel)
                            :exec output-channel)))
    (list (cons 'snip-info snip-info)
          (cons 'input-addr input-addr)
          (cons 'output-addr output-addr)
          (cons 'input-channel input-channel)
          (cons 'output-channel
                output-channel)))))