		Search-engine friendly clone of the ACL2 documentation.

Closure

Make-closure

Basic constructor macro for closure structures.

Syntax

(make-closure [:name <name>] 
              [:inputs <inputs>] 
              [:instrs <instrs>] 
              [:outputs <outputs>])

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

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

Definition

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

Macro: make-closure

(defmacro make-closure (&rest args)
  (std::make-aggregate 'closure
                       args
                       '((:name) (:inputs) (:instrs) (:outputs))
                       'make-closure
                       nil))

Function: closure

(defun closure (name inputs instrs outputs)
  (declare (xargs :guard (and (identifierp name)
                              (closure-input-listp inputs)
                              (instruction-listp instrs)
                              (closure-output-listp outputs))))
  (declare (xargs :guard t))
  (let ((__function__ 'closure))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (identifier-fix name)
                    :exec name))
         (inputs (mbe :logic (closure-input-list-fix inputs)
                      :exec inputs))
         (instrs (mbe :logic (instruction-list-fix instrs)
                      :exec instrs))
         (outputs (mbe :logic (closure-output-list-fix outputs)
                       :exec outputs)))
      (cons :closure (list (cons 'name name)
                           (cons 'inputs inputs)
                           (cons 'instrs instrs)
                           (cons 'outputs outputs))))))