Process the inputs.
(parse-files-process-inputs args wrld) → (mv erp const-transunits value-fileset gcc)
For the file set constant name input, we retrieve and return the file set.
Function:
(defun parse-files-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'parse-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) nil (fileset nil) nil) ((mv erp extra options) (partition-rest-and-keyword-args args *parse-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *parse-files-allowed-options* args))) ((when extra) (reterr (msg "The only allowed inputs are the options ~&0, ~ but instead the extra inputs ~x1 were supplied." *parse-files-allowed-options* extra))) (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))) (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))) (value-fileset (acl2::constant-value const-fileset wrld)) ((unless (filesetp value-fileset)) (reterr (msg "The value of the ~x0 named constant ~ specified by the :CONST-FILESET input ~ must satisfy FILESETP, ~ but instead its value is ~x1." const-fileset value-fileset))) (gcc-option (assoc-eq :gcc options)) (gcc (if gcc-option (cdr gcc-option) nil)) ((unless (booleanp gcc)) (reterr (msg "The :GCC input must be a boolean, ~ but it is ~x0 instead." gcc)))) (retok const-transunits value-fileset gcc))))
Theorem:
(defthm symbolp-of-parse-files-process-inputs.const-transunits (b* (((mv acl2::?erp ?const-transunits ?value-fileset ?gcc) (parse-files-process-inputs args wrld))) (symbolp const-transunits)) :rule-classes :rewrite)
Theorem:
(defthm filesetp-of-parse-files-process-inputs.value-fileset (b* (((mv acl2::?erp ?const-transunits ?value-fileset ?gcc) (parse-files-process-inputs args wrld))) (filesetp value-fileset)) :rule-classes :rewrite)
Theorem:
(defthm booleanp-of-parse-files-process-inputs.gcc (b* (((mv acl2::?erp ?const-transunits ?value-fileset ?gcc) (parse-files-process-inputs args wrld))) (booleanp gcc)) :rule-classes :rewrite)