		Search-engine friendly clone of the ACL2 documentation.

Fundecl

Make-fundecl

Basic constructor macro for fundecl structures.

Syntax

(make-fundecl [:annotations <annotations>] 
              [:sort <sort>] 
              [:name <name>] 
              [:inputs <inputs>] 
              [:output <output>] 
              [:body <body>] 
              [:finalizer <finalizer>])

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

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

Definition

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

Macro: make-fundecl

(defmacro make-fundecl (&rest args)
  (std::make-aggregate 'fundecl
                       args
                       '((:annotations)
                         (:sort)
                         (:name)
                         (:inputs)
                         (:output)
                         (:body)
                         (:finalizer))
                       'make-fundecl
                       nil))

Function: fundecl

(defun fundecl (annotations sort name inputs output body finalizer)
  (declare (xargs :guard (and (annotation-listp annotations)
                              (fun-sortp sort)
                              (identifierp name)
                              (funparam-listp inputs)
                              (typep output)
                              (statement-listp body)
                              (finalizer-optionp finalizer))))
  (declare (xargs :guard t))
  (let ((__function__ 'fundecl))
    (declare (ignorable __function__))
    (b* ((annotations (mbe :logic (annotation-list-fix annotations)
                           :exec annotations))
         (sort (mbe :logic (fun-sort-fix sort)
                    :exec sort))
         (name (mbe :logic (identifier-fix name)
                    :exec name))
         (inputs (mbe :logic (funparam-list-fix inputs)
                      :exec inputs))
         (output (mbe :logic (type-fix output)
                      :exec output))
         (body (mbe :logic (statement-list-fix body)
                    :exec body))
         (finalizer (mbe :logic (finalizer-option-fix finalizer)
                         :exec finalizer)))
      (cons :fundecl (list (cons 'annotations annotations)
                           (cons 'sort sort)
                           (cons 'name name)
                           (cons 'inputs inputs)
                           (cons 'output output)
                           (cons 'body body)
                           (cons 'finalizer finalizer))))))