		Search-engine friendly clone of the ACL2 documentation.

Function

Make-function

Basic constructor macro for function structures.

Syntax

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

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

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

Definition

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

Macro: make-function

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

Function: function

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