		Search-engine friendly clone of the ACL2 documentation.

Pipeline-setup

Make-pipeline-setup

Basic constructor macro for pipeline-setup structures.

Syntax

(make-pipeline-setup [:probes <probes>] 
                     [:inputs <inputs>] 
                     [:override-vals <override-vals>] 
                     [:override-tests <override-tests>] 
                     [:initst <initst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-pipeline-setup

(defmacro make-pipeline-setup (&rest args)
  (std::make-aggregate 'pipeline-setup
                       args
                       '((:probes)
                         (:inputs)
                         (:override-vals)
                         (:override-tests)
                         (:initst))
                       'make-pipeline-setup
                       nil))

Function: pipeline-setup

(defun pipeline-setup (probes inputs
                              override-vals override-tests initst)
 (declare (xargs :guard (and (svtv-probealist-p probes)
                             (svex-alistlist-p inputs)
                             (svex-alistlist-p override-vals)
                             (svex-alistlist-p override-tests)
                             (svex-alist-p initst))))
 (declare (xargs :guard t))
 (let ((__function__ 'pipeline-setup))
   (declare (ignorable __function__))
   (b*
    ((probes (mbe :logic (svtv-probealist-fix probes)
                  :exec probes))
     (inputs (mbe :logic (svex-alistlist-fix inputs)
                  :exec inputs))
     (override-vals (mbe :logic (svex-alistlist-fix override-vals)
                         :exec override-vals))
     (override-tests (mbe :logic (svex-alistlist-fix override-tests)
                          :exec override-tests))
     (initst (mbe :logic (svex-alist-fix initst)
                  :exec initst)))
    (list (cons 'probes probes)
          (cons 'inputs inputs)
          (cons 'override-vals override-vals)
          (cons 'override-tests override-tests)
          (cons 'initst initst)))))