Process all the inputs.
(deftreeops-process-inputs args call wrld) → (mv erp redundantp grammar rules prefix)
If the
Function:
(defun deftreeops-process-inputs (args call wrld) (declare (xargs :guard (and (true-listp args) (pseudo-event-formp call) (plist-worldp wrld)))) (let ((__function__ 'deftreeops-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil nil) ((mv erp grammar options) (partition-rest-and-keyword-args args *deftreeops-allowed-options*)) ((when (or erp (not (consp grammar)) (not (endp (cdr grammar))))) (reterr (msg "The inputs must be the constant name for the grammar ~ followed by the options ~&0." *deftreeops-allowed-options*))) (grammar (car grammar)) ((erp redundantp grammar rules) (deftreeops-process-grammar grammar call wrld)) ((when redundantp) (retok t nil nil nil)) (prefix-option (assoc-eq :prefix options)) ((unless (consp prefix-option)) (reterr (msg "The :PREFIX input must be supplied."))) (prefix (cdr prefix-option)) ((erp prefix) (deftreeops-process-prefix prefix))) (retok nil grammar rules prefix))))
Theorem:
(defthm booleanp-of-deftreeops-process-inputs.redundantp (b* (((mv acl2::?erp ?redundantp ?grammar ?rules ?prefix) (deftreeops-process-inputs args call wrld))) (booleanp redundantp)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-deftreeops-process-inputs.grammar (b* (((mv acl2::?erp ?redundantp ?grammar ?rules ?prefix) (deftreeops-process-inputs args call wrld))) (common-lisp::symbolp grammar)) :rule-classes :rewrite)
Theorem:
(defthm rulelistp-of-deftreeops-process-inputs.rules (b* (((mv acl2::?erp ?redundantp ?grammar ?rules ?prefix) (deftreeops-process-inputs args call wrld))) (rulelistp rules)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-deftreeops-process-inputs.prefix (b* (((mv acl2::?erp ?redundantp ?grammar ?rules ?prefix) (deftreeops-process-inputs args call wrld))) (common-lisp::symbolp prefix)) :rule-classes :rewrite)