Process the inputs.
(output-files-process-inputs args wrld) → (mv erp tunits/files process const-files)
The
The other results of this function are the homonymous inputs.
Function:
(defun output-files-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'output-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) (fileset nil) nil nil) ((mv erp extra options) (partition-rest-and-keyword-args args *output-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *output-files-allowed-options* args))) ((when extra) (reterr (msg "The only allowed inputs are the options ~&0, ~ but instead the extra inputs ~x1 were supplied." *output-files-allowed-options* extra))) (process-option (assoc-eq :process options)) (process (if process-option (cdr process-option) nil)) ((unless (output-files-process-inputp process)) (reterr (msg "The :PROCESS input must be NIL or :PRINT, ~ but it ~x0 instead." process))) (const-option (assoc-eq :const options)) ((unless const-option) (reterr (msg "The :CONST input must be supplied, ~ but it was not supplied."))) (const (cdr const-option)) ((unless (symbolp const)) (reterr (msg "The :CONST input must be a symbol, ~ but it is ~x0 instead." const))) (tunits/files (acl2::constant-value const wrld)) ((when (and (eq process nil) (not (filesetp tunits/files)))) (reterr (msg "Since the :PROCESS input is NIL (perhaps by default), ~ the value of the ~x0 named constant ~ specified by the :CONST input ~ must be a file set, ~ but instead its value is ~x1." const tunits/files))) ((when (and (eq process :print) (not (transunit-ensemblep tunits/files)))) (reterr (msg "Since the :PROCESS inpus is :PRINT, ~ the value of the ~x0 named constant ~ specified by the :CONST input ~ must be a translation unit ensemble, ~ but instead its value is ~x1." const tunits/files))) (const-files-option (assoc-eq :const-files options)) (const-files (if const-files-option (cdr const-files-option) nil)) ((unless (symbolp const-files)) (reterr (msg "The :CONST-FILES input must be a symbol, ~ but it is ~x0 instead." const-files))) ((when (and const-files (not process))) (reterr (msg "The :CONST-FILES input must be NIL ~ if the :PROCESS input is NIL, ~ which is the case in this call of OUTPUT-FILES.")))) (retok tunits/files process const-files))))
Theorem:
(defthm tunitens/fileset-p-of-output-files-process-inputs.tunits/files (b* (((mv acl2::?erp ?tunits/files ?process ?const-files) (output-files-process-inputs args wrld))) (tunitens/fileset-p tunits/files)) :rule-classes :rewrite)
Theorem:
(defthm output-files-process-inputp-of-output-files-process-inputs.process (b* (((mv acl2::?erp ?tunits/files ?process ?const-files) (output-files-process-inputs args wrld))) (output-files-process-inputp process)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-output-files-process-inputs.const-files (b* (((mv acl2::?erp ?tunits/files ?process ?const-files) (output-files-process-inputs args wrld))) (symbolp const-files)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemblep-of-output-files-process-inputs (b* (((mv acl2::?erp ?tunits/files ?process ?const-files) (output-files-process-inputs args wrld))) (implies (equal process :print) (transunit-ensemblep tunits/files))))
Theorem:
(defthm filesetp-of-output-files-process-inputs (b* (((mv acl2::?erp ?tunits/files ?process ?const-files) (output-files-process-inputs args wrld))) (implies (equal process nil) (filesetp tunits/files))))