Process the
(deftreeops-process-grammar grammar wrld) → (mv erp grammar rules)
Function:
(defun deftreeops-process-grammar (grammar wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'deftreeops-process-grammar)) (declare (ignorable __function__)) (b* (((reterr) nil nil) ((unless (constant-namep grammar wrld)) (reterr (msg "The *GRAMMAR* input ~x0 must be the name of a constant." grammar))) (rules (constant-value grammar wrld)) ((unless (and (rulelistp rules) (consp rules))) (reterr (msg "The *GRAMMAR* input is the name of a constant, ~ but its value ~x0 is not a non-empty ABNF grammar." rules))) ((unless (rulelist-wfp rules)) (reterr (msg "The *GRAMMAR* input denotes and ABNF grammar, ~ but the grammar is not well-formed (see :DOC ABNF::WELL-FORMEDNESS)."))) ((unless (rulelist-closedp rules)) (reterr (msg "The *GRAMMAR* input denotes an ABNF grammar, ~ but the grammar is not closed (see :DOC ABNF::CLOSURE).")))) (retok grammar rules))))
Theorem:
(defthm symbolp-of-deftreeops-process-grammar.grammar (b* (((mv acl2::?erp ?grammar ?rules) (deftreeops-process-grammar grammar wrld))) (common-lisp::symbolp grammar)) :rule-classes :rewrite)
Theorem:
(defthm rulelistp-of-deftreeops-process-grammar.rules (b* (((mv acl2::?erp ?grammar ?rules) (deftreeops-process-grammar grammar wrld))) (rulelistp rules)) :rule-classes :rewrite)