		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) → filemap
Arguments: tunitmap — Guard (filepath-transunit-mapp tunitmap).; options — Guard (prioptp options).
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)
 (declare (xargs :guard (and (filepath-transunit-mapp tunitmap)
                             (prioptp options))))
 (declare (xargs :guard (filepath-transunit-map-unambp tunitmap)))
 (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))
        (filemap (print-filepath-transunit-map (omap::tail tunitmap)
                                               options)))
     (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)))
    (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)))
      (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))
        (print-filepath-transunit-map tunitmap options)))

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)
             (print-filepath-transunit-map tunitmap options-equiv)))
 :rule-classes :congruence)