		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-filepath-transunit-map

Transform a map from file paths to translation units.

Signature
(simpadd0-filepath-transunit-map map gin state) → (mv new-map gout)
Arguments: map — Guard (filepath-transunit-mapp map).; gin — Guard (simpadd0-ginp gin).
Returns: new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).; gout — Type (simpadd0-goutp gout).

We transform both the file paths and the translation units.

Definitions and Theorems

Function: simpadd0-filepath-transunit-map

(defun simpadd0-filepath-transunit-map (map gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (filepath-transunit-mapp map)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (filepath-transunit-map-unambp map)))
 (let ((__function__ 'simpadd0-filepath-transunit-map))
  (declare (ignorable __function__))
  (b* (((simpadd0-gin gin) gin)
       ((when (omap::emptyp map))
        (mv nil
            (make-simpadd0-gout :events nil
                                :thm-name nil
                                :thm-index gin.thm-index
                                :names-to-avoid gin.names-to-avoid
                                :vartys nil
                                :diffp nil)))
       ((mv path tunit) (omap::head map))
       ((mv new-tunit (simpadd0-gout gout-tunit))
        (simpadd0-transunit tunit gin state))
       (gin (simpadd0-gin-update gin gout-tunit))
       ((mv new-map (simpadd0-gout gout-map))
        (simpadd0-filepath-transunit-map (omap::tail map)
                                         gin state)))
   (mv
      (omap::update path new-tunit new-map)
      (make-simpadd0-gout
           :events (append gout-tunit.events gout-map.events)
           :thm-name nil
           :thm-index gout-map.thm-index
           :names-to-avoid gout-map.names-to-avoid
           :vartys (omap::update* gout-tunit.vartys gout-map.vartys)
           :diffp (or gout-tunit.diffp gout-map.diffp))))))

Theorem: filepath-transunit-mapp-of-simpadd0-filepath-transunit-map.new-map

(defthm
 filepath-transunit-mapp-of-simpadd0-filepath-transunit-map.new-map
 (implies (filepath-transunit-mapp map)
          (b* (((mv ?new-map ?gout)
                (simpadd0-filepath-transunit-map map gin state)))
            (filepath-transunit-mapp new-map)))
 :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-filepath-transunit-map.gout

(defthm simpadd0-goutp-of-simpadd0-filepath-transunit-map.gout
  (b* (((mv ?new-map ?gout)
        (simpadd0-filepath-transunit-map map gin state)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: simpadd0-filepath-transunit-map-of-simpadd0-gin-fix-gin

(defthm simpadd0-filepath-transunit-map-of-simpadd0-gin-fix-gin
  (equal (simpadd0-filepath-transunit-map map (simpadd0-gin-fix gin)
                                          state)
         (simpadd0-filepath-transunit-map map gin state)))

Theorem: simpadd0-filepath-transunit-map-simpadd0-gin-equiv-congruence-on-gin

(defthm
 simpadd0-filepath-transunit-map-simpadd0-gin-equiv-congruence-on-gin
 (implies
      (simpadd0-gin-equiv gin gin-equiv)
      (equal (simpadd0-filepath-transunit-map map gin state)
             (simpadd0-filepath-transunit-map map gin-equiv state)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-unambp-of-simpadd0-filepath-transunit-map

(defthm
   filepath-transunit-map-unambp-of-simpadd0-filepath-transunit-map
  (implies (filepath-transunit-mapp map)
           (b* (((mv ?new-map ?gout)
                 (simpadd0-filepath-transunit-map map gin state)))
             (filepath-transunit-map-unambp new-map))))