Transform a list of block items.
(split-fn-block-item-list new-fn-name items spec pointers decls split-point) → (mv er new-fn 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.
Function:
(defun split-fn-block-item-list (new-fn-name items spec pointers decls split-point) (declare (xargs :guard (and (identp new-fn-name) (block-item-listp items) (declspec-listp spec) (type-qual-list-listp pointers) (ident-paramdecl-mapp decls) (natp split-point)))) (let ((__function__ 'split-fn-block-item-list)) (declare (ignorable __function__)) (b* ((items (block-item-list-fix items)) ((reterr) (c$::irr-fundef) items) ((when (zp split-point)) (b* (((erp idents new-fn) (abstract-fn new-fn-name spec pointers items decls))) (retok new-fn (list (block-item-stmt (stmt-return (make-expr-funcall :fun (expr-ident new-fn-name) :args (expr-ident-list idents)))))))) ((when (endp items)) (reterr (msg "Bad split point specifier"))) (item (first items)) (decls (block-item-case item :decl (omap::update* (decl-to-ident-paramdecl-map item.unwrap) (ident-paramdecl-map-fix decls)) :otherwise decls)) ((erp new-fn truncated-items) (split-fn-block-item-list new-fn-name (rest items) spec pointers decls (- split-point 1)))) (retok new-fn (cons (first items) truncated-items)))))
Theorem:
(defthm fundefp-of-split-fn-block-item-list.new-fn (b* (((mv acl2::?er ?new-fn ?truncated-items) (split-fn-block-item-list new-fn-name items spec pointers decls split-point))) (fundefp new-fn)) :rule-classes :rewrite)
Theorem:
(defthm block-item-listp-of-split-fn-block-item-list.truncated-items (b* (((mv acl2::?er ?new-fn ?truncated-items) (split-fn-block-item-list new-fn-name items spec pointers decls split-point))) (block-item-listp truncated-items)) :rule-classes :rewrite)