		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Split-fn-filepath-transunit-map

Transform a filepath.

Signature
(split-fn-filepath-transunit-map target-fn new-fn-name map split-point) → (mv er? new-map)
Arguments: target-fn — Guard (identp target-fn).; new-fn-name — Guard (identp new-fn-name).; map — Guard (filepath-transunit-mapp map).; split-point — Guard (natp split-point).
Returns: er? — Type (maybe-msgp er?).; new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).

Definitions and Theorems

Function: split-fn-filepath-transunit-map

(defun split-fn-filepath-transunit-map
       (target-fn new-fn-name map split-point)
  (declare (xargs :guard (and (identp target-fn)
                              (identp new-fn-name)
                              (filepath-transunit-mapp map)
                              (natp split-point))))
  (b* (((reterr) nil)
       ((when (omap::emptyp map)) (retok nil))
       ((mv path tunit) (omap::head map))
       ((erp new-tunit)
        (split-fn-transunit target-fn
                            new-fn-name tunit split-point))
       ((erp new-map)
        (split-fn-filepath-transunit-map
             target-fn new-fn-name (omap::tail map)
             split-point)))
    (retok (omap::update (c$::filepath-fix path)
                         new-tunit new-map))))

Theorem: maybe-msgp-of-split-fn-filepath-transunit-map.er?

(defthm maybe-msgp-of-split-fn-filepath-transunit-map.er?
  (b* (((mv ?er? ?new-map)
        (split-fn-filepath-transunit-map
             target-fn new-fn-name map split-point)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: filepath-transunit-mapp-of-split-fn-filepath-transunit-map.new-map

(defthm
 filepath-transunit-mapp-of-split-fn-filepath-transunit-map.new-map
 (implies (filepath-transunit-mapp map)
          (b* (((mv ?er? ?new-map)
                (split-fn-filepath-transunit-map
                     target-fn new-fn-name map split-point)))
            (filepath-transunit-mapp new-map)))
 :rule-classes :rewrite)