Process the inputs.
(read-files-process-inputs args) → (mv erp const paths preprocessor)
Function:
(defun read-files-process-inputs (args) (declare (xargs :guard (true-listp args))) (let ((__function__ 'read-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil) ((mv erp extra options) (partition-rest-and-keyword-args args *read-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *read-files-allowed-options* args))) ((when extra) (reterr (msg "The only allowed inputs are the options ~&0, ~ but instead the extra inputs ~x1 were supplied." *read-files-allowed-options* extra))) (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))) (files-option (assoc-eq :files options)) ((unless files-option) (reterr (msg "The :FILES input must be supplied, ~ but it was not supplied."))) (files (cdr files-option)) ((unless (string-listp files)) (reterr (msg "The :FILES input must be a list of strings, ~ but it is ~x0 instead." files))) ((unless (no-duplicatesp-equal files)) (reterr (msg "The :FILES input must be a list without duplicates, ~ but the supplied ~x0 has duplicates." files))) (paths (read-files-strings-to-paths files)) (preprocessor-option (assoc-eq :preprocessor options)) (preprocessor (if preprocessor-option (cdr preprocessor-option) nil)) ((unless (or (not preprocessor) (eq :auto preprocessor) (stringp preprocessor))) (reterr (msg "The :PREPROCESSOR input must be NIL, :AUTO, or a string, ~ but it is ~x0 instead." preprocessor)))) (retok const paths preprocessor))))
Theorem:
(defthm symbolp-of-read-files-process-inputs.const (b* (((mv acl2::?erp ?const ?paths ?preprocessor) (read-files-process-inputs args))) (symbolp const)) :rule-classes :rewrite)
Theorem:
(defthm filepath-setp-of-read-files-process-inputs.paths (b* (((mv acl2::?erp ?const ?paths ?preprocessor) (read-files-process-inputs args))) (filepath-setp paths)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-read-files-process-inputs.preprocessor (b* (((mv acl2::?erp ?const ?paths ?preprocessor) (read-files-process-inputs args))) (or (not preprocessor) (equal :auto preprocessor) (stringp preprocessor))) :rule-classes :rewrite)
Theorem:
(defthm stringp-of-read-files-process-inputs.preprocessor (b* (((mv acl2::?erp ?const ?paths ?preprocessor) (read-files-process-inputs args))) (equal (stringp preprocessor) (and preprocessor (not (equal :auto preprocessor))))))