Process all the inputs.
(deftreeops-process-inputs args wrld) → (mv erp grammar rules prefix)
Function:
(defun deftreeops-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'deftreeops-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) 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 grammar rules) (deftreeops-process-grammar grammar wrld)) (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 grammar rules prefix))))
Theorem:
(defthm symbolp-of-deftreeops-process-inputs.grammar (b* (((mv acl2::?erp ?grammar ?rules ?prefix) (deftreeops-process-inputs args wrld))) (common-lisp::symbolp grammar)) :rule-classes :rewrite)
Theorem:
(defthm rulelistp-of-deftreeops-process-inputs.rules (b* (((mv acl2::?erp ?grammar ?rules ?prefix) (deftreeops-process-inputs args wrld))) (rulelistp rules)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-deftreeops-process-inputs.prefix (b* (((mv acl2::?erp ?grammar ?rules ?prefix) (deftreeops-process-inputs args wrld))) (common-lisp::symbolp prefix)) :rule-classes :rewrite)