		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Filepath-transunit-map-try-split-fn-when

Signature
(filepath-transunit-map-try-split-fn-when map triggers transunits) → (mv er? found map$)
Arguments: map — Guard (filepath-transunit-mapp map).; triggers — Guard (ident-setp triggers).; transunits — Guard (transunit-ensemblep transunits).
Returns: er? — Type (maybe-msgp er?).; found — Type (booleanp found).; map$ — Type (filepath-transunit-mapp map$).

Definitions and Theorems

Function: filepath-transunit-map-try-split-fn-when

(defun filepath-transunit-map-try-split-fn-when
       (map triggers transunits)
 (declare (xargs :guard (and (filepath-transunit-mapp map)
                             (ident-setp triggers)
                             (transunit-ensemblep transunits))))
 (b*
  (((reterr) nil nil)
   (map (c$::filepath-transunit-map-fix map))
   ((when (omap::emptyp map))
    (retok nil nil))
   ((mv path tunit) (omap::head map))
   ((erp found tunit$)
    (transunit-try-split-fn-when tunit triggers transunits))
   ((when found)
    (retok found
           (omap::update path tunit$ (omap::tail map))))
   ((erp found map$)
    (filepath-transunit-map-try-split-fn-when (omap::tail map)
                                              triggers transunits)))
  (retok found (omap::update path tunit$ map$))))

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

(defthm maybe-msgp-of-filepath-transunit-map-try-split-fn-when.er?
  (b* (((mv ?er? ?found ?map$)
        (filepath-transunit-map-try-split-fn-when
             map triggers transunits)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: booleanp-of-filepath-transunit-map-try-split-fn-when.found

(defthm booleanp-of-filepath-transunit-map-try-split-fn-when.found
  (b* (((mv ?er? ?found ?map$)
        (filepath-transunit-map-try-split-fn-when
             map triggers transunits)))
    (booleanp found))
  :rule-classes :type-prescription)

Theorem: filepath-transunit-mapp-of-filepath-transunit-map-try-split-fn-when.map$

(defthm
 filepath-transunit-mapp-of-filepath-transunit-map-try-split-fn-when.map$
 (b* (((mv ?er? ?found ?map$)
       (filepath-transunit-map-try-split-fn-when
            map triggers transunits)))
   (filepath-transunit-mapp map$))
 :rule-classes :rewrite)