		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
                                  :vars 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
               :vars (union gout-tunit.vars gout-map.vars)
               :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))))