		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Declon-to-ident-param-declon-map

Convert a regular declaration into an omap of identifiers to parameter declarations.

Signature
(declon-to-ident-param-declon-map declon) → map
Arguments: declon — Guard (declonp declon).
Returns: map — Type (ident-param-declon-mapp map).

The resulting parameter declarations represent the same variables, with the same types and qualifiers. The keys to the omap are the identifiers bound by each parameter declaration.

A declaration which introduces multiple variables is converted to an omap of equal length to the number of identifiers. For instance, the declaration int x = 0, y = 0; is converted to the omap associating x to parameter declaration int x, and y to int y.

Only variable declarations are converted. Static assertions result in nil.

This is used by split-fn to track declared variables and to create parameters for the newly generated function (with the subset of declared variables which are used).

Definitions and Theorems

Function: declon-to-ident-param-declon-map0

(defun declon-to-ident-param-declon-map0 (declspecs initdeclors)
 (declare (xargs :guard (and (decl-spec-listp declspecs)
                             (init-declor-listp initdeclors))))
 (b* (((when (endp initdeclors)) nil)
      ((init-declor initdeclor)
       (first initdeclors))
      (ident (declor->ident initdeclor.declor)))
  (omap::update
   ident
   (make-param-declon
    :specs declspecs
    :declor (make-param-declor-nonabstract :declor initdeclor.declor
                                           :info nil)
    :attribs nil)
   (declon-to-ident-param-declon-map0
        declspecs (rest initdeclors)))))

Theorem: ident-param-declon-mapp-of-declon-to-ident-param-declon-map0

(defthm ident-param-declon-mapp-of-declon-to-ident-param-declon-map0
  (b*
   ((map (declon-to-ident-param-declon-map0 declspecs initdeclors)))
   (ident-param-declon-mapp map))
  :rule-classes :rewrite)

Function: declon-to-ident-param-declon-map

(defun declon-to-ident-param-declon-map (declon)
 (declare (xargs :guard (declonp declon)))
 (declon-case
     declon
     :declon
     (declon-to-ident-param-declon-map0 declon.specs declon.declors)
     :statassert nil))

Theorem: ident-param-declon-mapp-of-declon-to-ident-param-declon-map

(defthm ident-param-declon-mapp-of-declon-to-ident-param-declon-map
  (b* ((map (declon-to-ident-param-declon-map declon)))
    (ident-param-declon-mapp map))
  :rule-classes :rewrite)