		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) → (mv new-map gout)
Arguments: map — Guard (filepath-transunit-mapp map).; gin — Guard (ginp gin).
Returns: new-map — Type (filepath-transunit-mapp new-map), given (filepath-transunit-mapp map).; gout — Type (goutp gout).

We transform both the file paths and the translation units.

After each translation unit, we reset the vartys component of gin to nil, because each translation unit starts with no variables in scope. This component is initialized to nil in simpadd0-code-ensemble, so the first translation unit also has the right vartys.

Definitions and Theorems

Function: simpadd0-filepath-transunit-map

(defun simpadd0-filepath-transunit-map (map gin)
  (declare (xargs :guard (and (filepath-transunit-mapp map)
                              (ginp gin))))
  (declare (xargs :guard (and (filepath-transunit-map-unambp map)
                              (filepath-transunit-map-annop map))))
  (let ((__function__ 'simpadd0-filepath-transunit-map))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (omap::emptyp map))
          (mv nil (gout-no-thm gin)))
         ((mv path tunit) (omap::head map))
         ((mv new-tunit (gout gout-tunit))
          (simpadd0-transunit tunit gin))
         (gin (gin-update gin gout-tunit))
         (gin (change-gin gin :vartys nil))
         ((mv new-map (gout gout-map))
          (simpadd0-filepath-transunit-map (omap::tail map)
                                           gin))
         (gin (gin-update gin gout-map)))
      (mv (omap::update path new-tunit new-map)
          (gout-no-thm gin)))))

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)))
            (filepath-transunit-mapp new-map)))
 :rule-classes :rewrite)

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

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

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

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

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

(defthm simpadd0-filepath-transunit-map-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-filepath-transunit-map map gin)
                  (simpadd0-filepath-transunit-map map gin-equiv)))
  :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)))
             (filepath-transunit-map-unambp new-map))))

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

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

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

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