Generate code to parse an instance of an ABNF repetition.
(defdefparse-gen-code-for-repetition rep index prefix group-table option-table repetition-table) → (mv code var)
A repetition is part of a concatenation,
and a concatenation (see defdefparse-gen-code-for-concatenation)
is parsed by parsing each of its repetitions;
the results of parsing the repetitions must be put together
to yield the result of parsing the concatenation.
The result of parsing each repetition is bound to a different variable,
called
If the repetition is in the alist,
its parsing function is retrieved from there
and we generate code to bind its result to
If the repetition is not in the alist,
it must be a singleton repetition (this is what we support for now),
in which case we generate code to parse the element,
and we put the resulting tree into a singleton list if successful.
Note that we propagate the error when parsing the element,
i.e. we pass
Function:
(defun defdefparse-gen-code-for-repetition (rep index prefix group-table option-table repetition-table) (declare (xargs :guard (and (repetitionp rep) (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-repetition)) (declare (ignorable __function__)) (b* ((trees-index (add-suffix 'trees (str::nat-to-dec-string index))) (parse-repetition-fn? (cdr (assoc-equal rep repetition-table))) ((when parse-repetition-fn?) (mv (cons (cons (cons 'mv (cons trees-index '(input))) (cons (cons parse-repetition-fn? '(input)) 'nil)) (cons (cons (cons 'when (cons (cons 'reserrp (cons trees-index 'nil)) 'nil)) (cons (cons 'mv (cons (cons 'reserrf-push (cons trees-index 'nil)) '(input))) 'nil)) 'nil)) trees-index)) ((repetition rep) rep) ((when (equal rep.range (make-repeat-range :min 1 :max (nati-finite 1)))) (mv (append (defdefparse-gen-code-for-element rep.element t prefix group-table option-table) (cons (cons trees-index '((list tree))) 'nil)) trees-index))) (prog2$ (raise "Repetition ~x0 not supported yet." rep) (mv nil nil)))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-repetition.code (b* (((mv ?code ?var) (defdefparse-gen-code-for-repetition rep index prefix group-table option-table repetition-table))) (true-listp code)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-defdefparse-gen-code-for-repetition.var (b* (((mv ?code ?var) (defdefparse-gen-code-for-repetition rep index prefix group-table option-table repetition-table))) (common-lisp::symbolp var)) :rule-classes :rewrite)