Generate code to parse an instance of an ABNF concatenation.
(defdefparse-gen-code-for-concatenation conc prefix group-table option-table repetition-table) → code
A concatenation is parsed by parsing each repetition in order. We also generate a final b* binder that puts all the lists of trees from the repetiitons into a list of lists of trees for the concatenation.
Function:
(defun defdefparse-gen-code-for-concatenation-aux (conc index prefix group-table option-table repetition-table) (declare (xargs :guard (and (concatenationp conc) (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-concatenation-aux)) (declare (ignorable __function__)) (b* (((when (endp conc)) (mv nil nil)) ((mv code1 var) (defdefparse-gen-code-for-repetition (car conc) index prefix group-table option-table repetition-table)) ((mv code2 vars) (defdefparse-gen-code-for-concatenation-aux (cdr conc) (1+ index) prefix group-table option-table repetition-table))) (mv (append code1 code2) (cons var vars)))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-concatenation-aux.code (b* (((mv ?code ?vars) (defdefparse-gen-code-for-concatenation-aux conc index prefix group-table option-table repetition-table))) (true-listp code)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-defdefparse-gen-code-for-concatenation-aux.vars (b* (((mv ?code ?vars) (defdefparse-gen-code-for-concatenation-aux conc index prefix group-table option-table repetition-table))) (symbol-listp vars)) :rule-classes :rewrite)
Function:
(defun defdefparse-gen-code-for-concatenation (conc prefix group-table option-table repetition-table) (declare (xargs :guard (and (concatenationp conc) (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-concatenation)) (declare (ignorable __function__)) (b* (((when (endp conc)) (raise "Empty concatenation.")) ((mv code vars) (defdefparse-gen-code-for-concatenation-aux conc 1 prefix group-table option-table repetition-table))) (append code (cons (cons 'treess (cons (cons 'list vars) 'nil)) 'nil)))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-concatenation (b* ((code (defdefparse-gen-code-for-concatenation conc prefix group-table option-table repetition-table))) (true-listp code)) :rule-classes :rewrite)