Generate code to parse an instance of an ABNF alternation.
(defdefparse-gen-code-for-alternation alt order prefix group-table option-table repetition-table) → code
After possibly reordering the alternatives,
we generate code that tries every alternative.
We use variables
Note that for each attempt to parse an alternative
we bind the variable
Function:
(defun defdefparse-gen-code-for-alternation-aux (alt index prefix group-table option-table repetition-table) (declare (xargs :guard (and (alternationp alt) (natp index) (common-lisp::symbolp prefix) (defdefparse-alt-symbol-alistp group-table) (defdefparse-alt-symbol-alistp option-table) (defdefparse-rep-symbol-alistp repetition-table)))) (let ((__function__ 'defdefparse-gen-code-for-alternation-aux)) (declare (ignorable __function__)) (b* (((when (endp alt)) (mv nil nil)) (treess-index (add-suffix 'treess (str::nat-to-dec-string index))) (code (cons (cons (cons 'mv (cons treess-index '(input1))) (cons (cons 'b* (cons (defdefparse-gen-code-for-concatenation (car alt) prefix group-table option-table repetition-table) '((mv treess input)))) 'nil)) (cons (cons (cons 'when (cons (cons 'not (cons (cons 'reserrp (cons treess-index 'nil)) 'nil)) 'nil)) (cons (cons 'mv (cons treess-index '(input1))) 'nil)) 'nil))) ((mv more-code vars) (defdefparse-gen-code-for-alternation-aux (cdr alt) (1+ index) prefix group-table option-table repetition-table))) (mv (append code more-code) (cons treess-index vars)))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-alternation-aux.code (b* (((mv ?code ?vars) (defdefparse-gen-code-for-alternation-aux alt index prefix group-table option-table repetition-table))) (true-listp code)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-defdefparse-gen-code-for-alternation-aux.vars (b* (((mv ?code ?vars) (defdefparse-gen-code-for-alternation-aux alt index prefix group-table option-table repetition-table))) (symbol-listp vars)) :rule-classes :rewrite)
Function:
(defun defdefparse-gen-code-for-alternation (alt order prefix group-table option-table repetition-table) (declare (xargs :guard (and (alternationp alt) (pos-listp order) (common-lisp::symbolp prefix) (defdefparse-alt-symbol-alistp group-table) (defdefparse-alt-symbol-alistp option-table) (defdefparse-rep-symbol-alistp repetition-table)))) (let ((__function__ 'defdefparse-gen-code-for-alternation)) (declare (ignorable __function__)) (b* (((when (endp alt)) (raise "Empty alternation.")) ((unless (and (= (len order) (len alt)) (defdefparse-order-permutationp order))) (raise "Bad permutation ~x0." order)) (alt (defdefparse-reorder-alternation alt order)) ((mv code vars) (defdefparse-gen-code-for-alternation-aux alt 1 prefix group-table option-table repetition-table))) (cons 'b* (cons code (cons (cons 'mv (cons (cons 'reserrf (cons (cons 'list (cons ':found (cons (cons 'list vars) (cons ':required (cons (cons 'quote (cons alt 'nil)) 'nil))))) 'nil)) '(input))) 'nil))))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-alternation (b* ((code (defdefparse-gen-code-for-alternation alt order prefix group-table option-table repetition-table))) (true-listp code)) :rule-classes :rewrite)