		Search-engine friendly clone of the ACL2 documentation.

Wrap-fn-implementation

Filepath-transunit-map-wrap-fn

Transform an omap of file paths to translation units.

Signature
(filepath-transunit-map-wrap-fn map target-name wrapper-name? blacklist) → (mv er? any-foundp map$)
Arguments: map — Guard (filepath-transunit-mapp map).; target-name — Guard (identp target-name).; wrapper-name? — Guard (ident-optionp wrapper-name?).; blacklist — Guard (ident-setp blacklist).
Returns: er? — Type (maybe-msgp er?).; any-foundp — Type (booleanp any-foundp).; map$ — Type (filepath-transunit-mapp map$).

Definitions and Theorems

Function: filepath-transunit-map-wrap-fn

(defun filepath-transunit-map-wrap-fn
       (map target-name wrapper-name? blacklist)
  (declare (xargs :guard (and (filepath-transunit-mapp map)
                              (identp target-name)
                              (ident-optionp wrapper-name?)
                              (ident-setp blacklist))))
  (declare (xargs :guard (filepath-transunit-map-annop map)))
  (b* ((map (c$::filepath-transunit-map-fix map))
       ((reterr) nil map)
       ((when (omap::emptyp map))
        (retok nil nil))
       ((erp warnings? foundp transunit)
        (transunit-wrap-fn (omap::head-val map)
                           target-name wrapper-name? blacklist))
       (- (if warnings? (cw "Warning in ~x0: ~@1~%"
                            (filepath->unwrap (omap::head-key map))
                            warnings?)
            nil))
       ((erp any-foundp map$)
        (filepath-transunit-map-wrap-fn
             (omap::tail map)
             target-name wrapper-name? blacklist)))
    (retok (or foundp any-foundp)
           (omap::update (omap::head-key map)
                         transunit map$))))

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

(defthm maybe-msgp-of-filepath-transunit-map-wrap-fn.er?
  (b* (((mv ?er? ?any-foundp ?map$)
        (filepath-transunit-map-wrap-fn
             map
             target-name wrapper-name? blacklist)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: booleanp-of-filepath-transunit-map-wrap-fn.any-foundp

(defthm booleanp-of-filepath-transunit-map-wrap-fn.any-foundp
  (b* (((mv ?er? ?any-foundp ?map$)
        (filepath-transunit-map-wrap-fn
             map
             target-name wrapper-name? blacklist)))
    (booleanp any-foundp))
  :rule-classes :type-prescription)

Theorem: filepath-transunit-mapp-of-filepath-transunit-map-wrap-fn.map$

(defthm
     filepath-transunit-mapp-of-filepath-transunit-map-wrap-fn.map$
  (b* (((mv ?er? ?any-foundp ?map$)
        (filepath-transunit-map-wrap-fn
             map
             target-name wrapper-name? blacklist)))
    (filepath-transunit-mapp map$))
  :rule-classes :rewrite)

Theorem: filepath-transunit-map-wrap-fn-of-filepath-transunit-map-fix-map

(defthm
   filepath-transunit-map-wrap-fn-of-filepath-transunit-map-fix-map
  (equal (filepath-transunit-map-wrap-fn
              (c$::filepath-transunit-map-fix map)
              target-name wrapper-name? blacklist)
         (filepath-transunit-map-wrap-fn
              map
              target-name wrapper-name? blacklist)))

Theorem: filepath-transunit-map-wrap-fn-filepath-transunit-map-equiv-congruence-on-map

(defthm
 filepath-transunit-map-wrap-fn-filepath-transunit-map-equiv-congruence-on-map
 (implies (c$::filepath-transunit-map-equiv map map-equiv)
          (equal (filepath-transunit-map-wrap-fn
                      map target-name wrapper-name? blacklist)
                 (filepath-transunit-map-wrap-fn
                      map-equiv
                      target-name wrapper-name? blacklist)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-wrap-fn-of-ident-fix-target-name

(defthm filepath-transunit-map-wrap-fn-of-ident-fix-target-name
  (equal (filepath-transunit-map-wrap-fn map (ident-fix target-name)
                                         wrapper-name? blacklist)
         (filepath-transunit-map-wrap-fn
              map
              target-name wrapper-name? blacklist)))

Theorem: filepath-transunit-map-wrap-fn-ident-equiv-congruence-on-target-name

(defthm
 filepath-transunit-map-wrap-fn-ident-equiv-congruence-on-target-name
 (implies
   (c$::ident-equiv target-name target-name-equiv)
   (equal (filepath-transunit-map-wrap-fn
               map target-name wrapper-name? blacklist)
          (filepath-transunit-map-wrap-fn map target-name-equiv
                                          wrapper-name? blacklist)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-wrap-fn-of-ident-option-fix-wrapper-name?

(defthm
   filepath-transunit-map-wrap-fn-of-ident-option-fix-wrapper-name?
 (equal
    (filepath-transunit-map-wrap-fn map target-name
                                    (ident-option-fix wrapper-name?)
                                    blacklist)
    (filepath-transunit-map-wrap-fn
         map
         target-name wrapper-name? blacklist)))

Theorem: filepath-transunit-map-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?

(defthm
 filepath-transunit-map-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?
 (implies
  (c$::ident-option-equiv wrapper-name? wrapper-name?-equiv)
  (equal
    (filepath-transunit-map-wrap-fn
         map target-name wrapper-name? blacklist)
    (filepath-transunit-map-wrap-fn map target-name
                                    wrapper-name?-equiv blacklist)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-wrap-fn-of-ident-set-fix-blacklist

(defthm filepath-transunit-map-wrap-fn-of-ident-set-fix-blacklist
  (equal (filepath-transunit-map-wrap-fn
              map target-name
              wrapper-name? (ident-set-fix blacklist))
         (filepath-transunit-map-wrap-fn
              map
              target-name wrapper-name? blacklist)))

Theorem: filepath-transunit-map-wrap-fn-ident-set-equiv-congruence-on-blacklist

(defthm
 filepath-transunit-map-wrap-fn-ident-set-equiv-congruence-on-blacklist
 (implies
  (c$::ident-set-equiv blacklist blacklist-equiv)
  (equal
    (filepath-transunit-map-wrap-fn
         map target-name wrapper-name? blacklist)
    (filepath-transunit-map-wrap-fn map target-name
                                    wrapper-name? blacklist-equiv)))
 :rule-classes :congruence)