		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Split-fn-block-item-list

Transform a list of block items.

Signature
(split-fn-block-item-list new-fn-name items specs pointers decls split-point) → (mv er? new-fn truncated-items)
Arguments: new-fn-name — Guard (identp new-fn-name).; items — Guard (block-item-listp items).; specs — Guard (decl-spec-listp specs).; pointers — Guard (typequal/attribspec-list-listp pointers).; decls — Guard (ident-param-declon-mapp decls).; split-point — Guard (natp split-point).
Returns: er? — Type (maybe-msgp er?).; new-fn — Type (fundefp new-fn).; truncated-items — Type (block-item-listp truncated-items).

This function will walk over a list of block items until it reaches the designated split point. Until then, it processes each declaration, associating locally introduced identifers to parameter declarations compatible with their original declaration. When the split point is reached, abstract-fn is invoked to generate the new function with parameters derived from this parameter declaration map. The previous function is truncated at this point, and a return statement added calling the newly split-out function.

Definitions and Theorems

Function: split-fn-block-item-list

(defun split-fn-block-item-list
       (new-fn-name items specs pointers decls split-point)
 (declare
      (xargs :guard (and (identp new-fn-name)
                         (block-item-listp items)
                         (decl-spec-listp specs)
                         (typequal/attribspec-list-listp pointers)
                         (ident-param-declon-mapp decls)
                         (natp split-point))))
 (b*
  ((items (block-item-list-fix items))
   ((reterr) (irr-fundef) items)
   ((when (zp split-point))
    (b* (((mv idents new-fn)
          (abstract-fn new-fn-name
                       specs pointers items decls)))
     (retok
      new-fn
      (list
       (make-block-item-stmt
        :stmt
        (make-stmt-return
         :expr?
         (make-expr-funcall :fun (make-expr-ident :ident new-fn-name
                                                  :info nil)
                            :args (map-address-ident-list idents))
         :info nil)
        :info nil)))))
   ((when (endp items))
    (retmsg$ "Bad split point specifier"))
   (item (first items))
   (decls
    (block-item-case
       item
       :declon
       (omap::update* (declon-to-ident-param-declon-map item.declon)
                      (ident-param-declon-map-fix decls))
       :otherwise decls))
   ((erp new-fn truncated-items)
    (split-fn-block-item-list new-fn-name (rest items)
                              specs
                              pointers decls (- split-point 1))))
  (retok new-fn
         (cons (first items) truncated-items))))

Theorem: maybe-msgp-of-split-fn-block-item-list.er?

(defthm maybe-msgp-of-split-fn-block-item-list.er?
 (b* (((mv ?er? ?new-fn ?truncated-items)
       (split-fn-block-item-list new-fn-name items
                                 specs pointers decls split-point)))
   (maybe-msgp er?))
 :rule-classes :rewrite)

Theorem: fundefp-of-split-fn-block-item-list.new-fn

(defthm fundefp-of-split-fn-block-item-list.new-fn
 (b* (((mv ?er? ?new-fn ?truncated-items)
       (split-fn-block-item-list new-fn-name items
                                 specs pointers decls split-point)))
   (fundefp new-fn))
 :rule-classes :rewrite)

Theorem: block-item-listp-of-split-fn-block-item-list.truncated-items

(defthm block-item-listp-of-split-fn-block-item-list.truncated-items
 (b* (((mv ?er? ?new-fn ?truncated-items)
       (split-fn-block-item-list new-fn-name items
                                 specs pointers decls split-point)))
   (block-item-listp truncated-items))
 :rule-classes :rewrite)