		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-filepath-transunit-map

Print the files in a file set.

Signature
(print-filepath-transunit-map tunitmap options gcc) → filemap
Arguments: tunitmap — Guard (filepath-transunit-mapp tunitmap).; options — Guard (prioptp options).; gcc — Guard (booleanp gcc).
Returns: filemap — Type (filepath-filedata-mapp filemap).

The input is a map from file paths to translation units, i.e. the core content of a translation unit ensemble. We also pass the printer options as additional input. We go through each translation unit in the map and print it, obtaining a file for each. We return a map from file paths to files that corresponds to the map from file paths to translation units. The two maps have the same keys.

Definitions and Theorems

Function: print-filepath-transunit-map

(defun print-filepath-transunit-map (tunitmap options gcc)
 (declare (xargs :guard (and (filepath-transunit-mapp tunitmap)
                             (prioptp options)
                             (booleanp gcc))))
 (declare
   (xargs
        :guard (and (filepath-transunit-map-unambp tunitmap)
                    (filepath-transunit-map-aidentp tunitmap gcc))))
 (let ((__function__ 'print-filepath-transunit-map))
   (declare (ignorable __function__))
   (b* (((when (omap::emptyp tunitmap)) nil)
        ((mv filepath tunit)
         (omap::head tunitmap))
        (data (print-file tunit options gcc))
        (filemap (print-filepath-transunit-map (omap::tail tunitmap)
                                               options gcc)))
     (omap::update (filepath-fix filepath)
                   (filedata data)
                   filemap))))

Theorem: filepath-filedata-mapp-of-print-filepath-transunit-map

(defthm filepath-filedata-mapp-of-print-filepath-transunit-map
 (b* ((filemap (print-filepath-transunit-map tunitmap options gcc)))
   (filepath-filedata-mapp filemap))
 :rule-classes :rewrite)

Theorem: keys-of-print-filepath-transunit-map

(defthm keys-of-print-filepath-transunit-map
 (implies
   (filepath-transunit-mapp tunitmap)
   (b*
    ((?filemap (print-filepath-transunit-map tunitmap options gcc)))
    (equal (omap::keys filemap)
           (omap::keys tunitmap)))))

Theorem: print-filepath-transunit-map-of-priopt-fix-options

(defthm print-filepath-transunit-map-of-priopt-fix-options
  (equal (print-filepath-transunit-map tunitmap (priopt-fix options)
                                       gcc)
         (print-filepath-transunit-map tunitmap options gcc)))

Theorem: print-filepath-transunit-map-priopt-equiv-congruence-on-options

(defthm
    print-filepath-transunit-map-priopt-equiv-congruence-on-options
 (implies
  (priopt-equiv options options-equiv)
  (equal (print-filepath-transunit-map tunitmap options gcc)
         (print-filepath-transunit-map tunitmap options-equiv gcc)))
 :rule-classes :congruence)

Theorem: print-filepath-transunit-map-of-bool-fix-gcc

(defthm print-filepath-transunit-map-of-bool-fix-gcc
 (equal
      (print-filepath-transunit-map tunitmap options (bool-fix gcc))
      (print-filepath-transunit-map tunitmap options gcc)))

Theorem: print-filepath-transunit-map-iff-congruence-on-gcc

(defthm print-filepath-transunit-map-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal (print-filepath-transunit-map tunitmap options gcc)
         (print-filepath-transunit-map tunitmap options gcc-equiv)))
 :rule-classes :congruence)