		Search-engine friendly clone of the ACL2 documentation.

Func

Make-func

Basic constructor macro for func structures.

Syntax

(make-func [:name <name>] 
           [:formals <formals>] 
           [:guard <guard>] 
           [:returns <returns>] 
           [:more-returns <more-returns>] 
           [:expansion-depth <expansion-depth>] 
           [:flattened-formals <flattened-formals>] 
           [:flattened-returns <flattened-returns>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-func

(defmacro make-func (&rest args)
  (std::make-aggregate 'func
                       args
                       '((:name)
                         (:formals)
                         (:guard make-hint-pair)
                         (:returns)
                         (:more-returns)
                         (:expansion-depth . 1)
                         (:flattened-formals)
                         (:flattened-returns))
                       'make-func
                       nil))

Function: func

(defun func (name formals guard
                  returns more-returns expansion-depth
                  flattened-formals flattened-returns)
  (declare (xargs :guard (and (symbolp name)
                              (decl-listp formals)
                              (hint-pair-p guard)
                              (decl-listp returns)
                              (hint-pair-listp more-returns)
                              (natp expansion-depth)
                              (symbol-listp flattened-formals)
                              (symbol-listp flattened-returns))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'func))
    (declare (ignorable acl2::__function__))
    (b* ((name (mbe :logic (symbol-fix name)
                    :exec name))
         (formals (mbe :logic (decl-list-fix formals)
                       :exec formals))
         (guard (mbe :logic (hint-pair-fix guard)
                     :exec guard))
         (returns (mbe :logic (decl-list-fix returns)
                       :exec returns))
         (more-returns (mbe :logic (hint-pair-list-fix more-returns)
                            :exec more-returns))
         (expansion-depth (mbe :logic (nfix expansion-depth)
                               :exec expansion-depth))
         (flattened-formals
              (mbe :logic (symbol-list-fix flattened-formals)
                   :exec flattened-formals))
         (flattened-returns
              (mbe :logic (symbol-list-fix flattened-returns)
                   :exec flattened-returns)))
      (list (cons 'name name)
            (cons 'formals formals)
            (cons 'guard guard)
            (cons 'returns returns)
            (cons 'more-returns more-returns)
            (cons 'expansion-depth expansion-depth)
            (cons 'flattened-formals
                  flattened-formals)
            (cons 'flattened-returns
                  flattened-returns)))))