		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fileset

Print a file set.

Signature
(print-fileset tunits options) → fileset
Arguments: tunits — Guard (transunit-ensemblep tunits).; options — Guard (prioptp options).
Returns: fileset — Type (filesetp fileset).

The input is a translation unit ensemble in the abstract syntax. We also pass the printer options as additional input. We go through each translation unit in the ensemble and print it, obtaining a file for each. We return a file set that corresponds to the translation unit ensemble. The file paths are the same for the translation unit ensemble and for the file set (they are the keys of the maps).

Definitions and Theorems

Function: print-fileset-loop

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

Theorem: filepath-filedata-mapp-of-print-fileset-loop

(defthm filepath-filedata-mapp-of-print-fileset-loop
  (b* ((filemap (print-fileset-loop tunitmap options)))
    (filepath-filedata-mapp filemap))
  :rule-classes :rewrite)

Theorem: keys-of-print-fileset-loop

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

Theorem: print-fileset-loop-of-priopt-fix-options

(defthm print-fileset-loop-of-priopt-fix-options
  (equal (print-fileset-loop tunitmap (priopt-fix options))
         (print-fileset-loop tunitmap options)))

Theorem: print-fileset-loop-priopt-equiv-congruence-on-options

(defthm print-fileset-loop-priopt-equiv-congruence-on-options
  (implies (priopt-equiv options options-equiv)
           (equal (print-fileset-loop tunitmap options)
                  (print-fileset-loop tunitmap options-equiv)))
  :rule-classes :congruence)

Function: print-fileset

(defun print-fileset (tunits options)
  (declare (xargs :guard (and (transunit-ensemblep tunits)
                              (prioptp options))))
  (declare (xargs :guard (transunit-ensemble-unambp tunits)))
  (let ((__function__ 'print-fileset))
    (declare (ignorable __function__))
    (fileset (print-fileset-loop (transunit-ensemble->unwrap tunits)
                                 options))))

Theorem: filesetp-of-print-fileset

(defthm filesetp-of-print-fileset
  (b* ((fileset (print-fileset tunits options)))
    (filesetp fileset))
  :rule-classes :rewrite)

Theorem: keys-of-print-fileset

(defthm keys-of-print-fileset
  (b* ((?fileset (print-fileset tunits options)))
    (equal (omap::keys (fileset->unwrap fileset))
           (omap::keys (transunit-ensemble->unwrap tunits)))))

Theorem: print-fileset-of-transunit-ensemble-fix-tunits

(defthm print-fileset-of-transunit-ensemble-fix-tunits
  (equal (print-fileset (transunit-ensemble-fix tunits)
                        options)
         (print-fileset tunits options)))

Theorem: print-fileset-transunit-ensemble-equiv-congruence-on-tunits

(defthm print-fileset-transunit-ensemble-equiv-congruence-on-tunits
  (implies (transunit-ensemble-equiv tunits tunits-equiv)
           (equal (print-fileset tunits options)
                  (print-fileset tunits-equiv options)))
  :rule-classes :congruence)

Theorem: print-fileset-of-priopt-fix-options

(defthm print-fileset-of-priopt-fix-options
  (equal (print-fileset tunits (priopt-fix options))
         (print-fileset tunits options)))

Theorem: print-fileset-priopt-equiv-congruence-on-options

(defthm print-fileset-priopt-equiv-congruence-on-options
  (implies (priopt-equiv options options-equiv)
           (equal (print-fileset tunits options)
                  (print-fileset tunits options-equiv)))
  :rule-classes :congruence)