		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 unwrap the translation unit ensemble obtainining a map, we print the translation units of the map to files into a file map, and we wrap the file map into a file set.

Definitions and Theorems

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-filepath-transunit-map (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)