		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-fileset

Print a file set.

Signature
(print-fileset tunits options gcc) → fileset
Arguments: tunits — Guard (transunit-ensemblep tunits).; options — Guard (prioptp options).; gcc — Guard (booleanp gcc).
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 gcc)
 (declare (xargs :guard (and (transunit-ensemblep tunits)
                             (prioptp options)
                             (booleanp gcc))))
 (declare (xargs :guard (transunit-ensemble-unambp tunits)))
 (let ((__function__ 'print-fileset))
  (declare (ignorable __function__))
  (fileset
   (print-filepath-transunit-map (transunit-ensemble->unwrap tunits)
                                 options gcc))))

Theorem: filesetp-of-print-fileset

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

Theorem: keys-of-print-fileset

(defthm keys-of-print-fileset
  (b* ((?fileset (print-fileset tunits options gcc)))
    (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 gcc)
         (print-fileset tunits options gcc)))

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 gcc)
                  (print-fileset tunits-equiv options gcc)))
  :rule-classes :congruence)

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

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

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 gcc)
                  (print-fileset tunits options-equiv gcc)))
  :rule-classes :congruence)

Theorem: print-fileset-of-bool-fix-gcc

(defthm print-fileset-of-bool-fix-gcc
  (equal (print-fileset tunits options (bool-fix gcc))
         (print-fileset tunits options gcc)))

Theorem: print-fileset-iff-congruence-on-gcc

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