		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Abstract-fn

Create a new function from the block items following the split-fn split point.

Signature
(abstract-fn new-fn-name specs pointers items decls) → (mv idents new-fn)
Arguments: new-fn-name — Guard (identp new-fn-name).; specs — Guard (decl-spec-listp specs).; pointers — Guard (typequal/attribspec-list-listp pointers).; items — Guard (block-item-listp items).; decls — Guard (ident-param-declon-mapp decls).
Returns: idents — The identifiers appearing in argument decls corresponding to the function parameters (in the same order).
Type (ident-listp idents).; new-fn — The new function definition.
Type (fundefp new-fn).

The new function will be created with same return type as the original.

Arguments to the function are determined by taking the variable declarations of the original function which appear free in the block items, which will constitute the body of the new function. (Note that arguments are not currently taken by reference, but this may be necessary for general equivalence. It may be sufficient to take an argument by reference when its address is taken in an expression of the new function body.)

Definitions and Theorems

Function: ident-param-declon-map-filter

(defun ident-param-declon-map-filter (map idents)
 (declare (xargs :guard (and (ident-param-declon-mapp map)
                             (ident-setp idents))))
 (b* ((map (ident-param-declon-map-fix map))
      ((when (omap::emptyp map)) nil)
      ((mv key val) (omap::head map)))
   (if (in key idents)
       (omap::update key val
                     (ident-param-declon-map-filter (omap::tail map)
                                                    idents))
     (ident-param-declon-map-filter (omap::tail map)
                                    idents))))

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

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

Function: abstract-fn

(defun abstract-fn (new-fn-name specs pointers items decls)
 (declare
      (xargs :guard (and (identp new-fn-name)
                         (decl-spec-listp specs)
                         (typequal/attribspec-list-listp pointers)
                         (block-item-listp items)
                         (ident-param-declon-mapp decls))))
 (b* (((mv idents -)
       (free-vars-block-item-list items nil))
      (decls (ident-param-declon-map-filter decls idents))
      (idents (omap::keys decls))
      (params (strip-cdrs decls))
      (deref-subst (make-deref-subst idents))
      ((mv items -)
       (block-item-list-subst-free items deref-subst nil)))
  (mv
   idents
   (make-fundef
    :specs specs
    :declor
    (make-declor
        :pointers pointers
        :direct (make-dirdeclor-function-params
                     :declor (dirdeclor-ident new-fn-name)
                     :params (map-add-pointer-param-declon params)))
    :body (make-comp-stmt :labels nil
                          :items items)
    :info nil))))

Theorem: ident-listp-of-abstract-fn.idents

(defthm ident-listp-of-abstract-fn.idents
  (b* (((mv ?idents ?new-fn)
        (abstract-fn new-fn-name
                     specs pointers items decls)))
    (ident-listp idents))
  :rule-classes :rewrite)

Theorem: fundefp-of-abstract-fn.new-fn

(defthm fundefp-of-abstract-fn.new-fn
  (b* (((mv ?idents ?new-fn)
        (abstract-fn new-fn-name
                     specs pointers items decls)))
    (fundefp new-fn))
  :rule-classes :rewrite)