Process the inputs.
(print-files-process-inputs args wrld) → (mv erp const-fileset value-transunits)
For the translation unit ensemble constant name input, we retrieve and return the translation unit ensemble.
Function:
(defun print-files-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'print-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) nil (fileset nil)) ((mv erp extra options) (partition-rest-and-keyword-args args *print-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *print-files-allowed-options* args))) ((when extra) (reterr (msg "The only allowed inputs are the options ~&0, ~ but instead the extra inputs ~x1 were supplied." *print-files-allowed-options* extra))) (const-fileset-option (assoc-eq :const-fileset options)) ((unless const-fileset-option) (reterr (msg "The :CONST-FILESET input must be supplied, ~ but it was not supplied."))) (const-fileset (cdr const-fileset-option)) ((unless (symbolp const-fileset)) (reterr (msg "The :CONST-FILESET input must be a symbol, ~ but it is ~x0 instead." const-fileset))) (const-transunits-option (assoc-eq :const-transunits options)) ((unless const-transunits-option) (reterr (msg "The :CONST-TRANSUNITS input must be supplied, ~ but it was not supplied."))) (const-transunits (cdr const-transunits-option)) ((unless (symbolp const-transunits)) (reterr (msg "The :CONST-TRANSUNITS input must be a symbol, ~ but it is ~x0 instead." const-transunits))) (value-transunits (acl2::constant-value const-transunits wrld)) ((unless (transunit-ensemblep value-transunits)) (reterr (msg "The value of the ~x0 named constant ~ specified by the :CONST-TRANSUNITS input ~ must satisfy TRANSUNIT-ENSEMBLEP, ~ but instead its value is ~x1." const-transunits value-transunits)))) (retok const-fileset value-transunits))))
Theorem:
(defthm symbolp-of-print-files-process-inputs.const-fileset (b* (((mv acl2::?erp ?const-fileset ?value-transunits) (print-files-process-inputs args wrld))) (symbolp const-fileset)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemblep-of-print-files-process-inputs.value-transunits (b* (((mv acl2::?erp ?const-fileset ?value-transunits) (print-files-process-inputs args wrld))) (transunit-ensemblep value-transunits)) :rule-classes :rewrite)