		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-param-declon-list

Generate a list of C parameter declarations from a list of ACL2 formal parameters.

Signature
(atc-gen-param-declon-list typed-formals fn prec-objs) → (mv erp params)
Arguments: typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; fn — Guard (symbolp fn).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).
Returns: params — Type (param-declon-listp params).

The ACL2 formal parameters are actually passed as an alist, from the formals to their information, as calculated by atc-typed-formals.

We check that the name of each parameter is a portable C identifier, and distinct from the names of the other parameters.

If a parameter represents an access to an external object, we skip it, i.e. we do not generate a declaration for it.

Definitions and Theorems

Function: atc-gen-param-declon-list

(defun atc-gen-param-declon-list (typed-formals fn prec-objs)
 (declare
      (xargs :guard (and (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp fn)
                         (atc-string-objinfo-alistp prec-objs))))
 (let ((__function__ 'atc-gen-param-declon-list))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when (endp typed-formals))
     (retok nil))
    ((cons formal info) (car typed-formals))
    (type (atc-var-info->type info))
    (name (symbol-name formal))
    ((unless (paident-stringp name))
     (reterr
      (msg
       "The symbol name ~s0 of ~
               the formal parameter ~x1 of the function ~x2 ~
               must be a portable ASCII C identifier, but it is not."
       name formal fn)))
    (cdr-formals (strip-cars (cdr typed-formals)))
    ((when (member-equal name (symbol-name-lst cdr-formals)))
     (reterr
      (msg
       "The formal parameter ~x0 of the function ~x1 ~
               has the same symbol name as ~
               another formal parameter among ~x2; ~
               this is disallowed, even if the package names differ."
       formal fn cdr-formals)))
    ((when
      (b*
       ((info (cdr (assoc-equal (symbol-name formal)
                                prec-objs)))
        ((unless info) nil)
        ((unless (atc-obj-infop info))
         (raise
          "Internal error: ~
                            malformed ATC-OBJ-INFO ~x0."
          info))
        (info (atc-obj-info->defobject info)))
       (eq (defobject-info->name-symbol info)
           formal)))
     (atc-gen-param-declon-list (cdr typed-formals)
                                fn prec-objs))
    ((mv tyspec declor)
     (ident+type-to-tyspec+declor (make-ident :name name)
                                  type))
    (param (make-param-declon :tyspec tyspec
                              :declor declor))
    ((erp params)
     (atc-gen-param-declon-list (cdr typed-formals)
                                fn prec-objs)))
   (retok (cons param params)))))

Theorem: param-declon-listp-of-atc-gen-param-declon-list.params

(defthm param-declon-listp-of-atc-gen-param-declon-list.params
  (b* (((mv acl2::?erp ?params)
        (atc-gen-param-declon-list typed-formals fn prec-objs)))
    (param-declon-listp params))
  :rule-classes :rewrite)