		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Abstract-fn

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

Signature
(abstract-fn new-fn-name spec pointers items decls) → (mv er idents new-fn)
Arguments: new-fn-name — Guard (identp new-fn-name).; spec — Guard (decl-spec-listp spec).; pointers — Guard (typequal/attribspec-list-listp pointers).; items — Guard (block-item-listp items).; decls — Guard (ident-paramdecl-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-paramdecls-map-filter

(defun ident-paramdecls-map-filter (map idents)
 (declare (xargs :guard (and (ident-paramdecl-mapp map)
                             (ident-setp idents))))
 (let ((__function__ 'ident-paramdecls-map-filter))
   (declare (ignorable __function__))
   (b* ((map (ident-paramdecl-map-fix map))
        ((when (omap::emptyp map)) nil)
        ((mv key val) (omap::head map)))
     (if (in key idents)
         (omap::update key val
                       (ident-paramdecls-map-filter (omap::tail map)
                                                    idents))
       (ident-paramdecls-map-filter (omap::tail map)
                                    idents)))))

Theorem: ident-paramdecl-mapp-of-ident-paramdecls-map-filter

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

Function: abstract-fn

(defun abstract-fn (new-fn-name spec pointers items decls)
 (declare
      (xargs :guard (and (identp new-fn-name)
                         (decl-spec-listp spec)
                         (typequal/attribspec-list-listp pointers)
                         (block-item-listp items)
                         (ident-paramdecl-mapp decls))))
 (let ((__function__ 'abstract-fn))
  (declare (ignorable __function__))
  (b* (((reterr) nil (c$::irr-fundef))
       (idents (free-vars-block-item-list items nil))
       (decls (ident-paramdecls-map-filter decls idents))
       (idents (omap::keys decls))
       (params (strip-cdrs decls)))
   (retok
    idents
    (make-fundef
       :spec spec
       :declor
       (make-declor :pointers pointers
                    :direct (make-dirdeclor-function-params
                                 :decl (dirdeclor-ident new-fn-name)
                                 :params params))
       :body (stmt-compound items))))))

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

(defthm ident-listp-of-abstract-fn.idents
  (b* (((mv acl2::?er ?idents ?new-fn)
        (abstract-fn new-fn-name spec 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 acl2::?er ?idents ?new-fn)
        (abstract-fn new-fn-name spec pointers items decls)))
    (fundefp new-fn))
  :rule-classes :rewrite)