Generate code to parse an instance of an ABNF element.
(defdefparse-gen-code-for-element elem check-error-p prefix group-table option-table) → code
Numeric and character value notations are parsed directly. Rule names are parsed by calling the corresponding functions, whose names is derived from the rule names. Groups and options are parsed by calling the corresponding functions, whose names are looked up in the alists.
We generate a b* binder that binds the parsing results
to variables
Function:
(defun defdefparse-gen-code-for-element (elem check-error-p prefix group-table option-table) (declare (xargs :guard (and (elementp elem) (booleanp check-error-p) (common-lisp::symbolp prefix) (defdefparse-alt-symbol-alistp group-table) (defdefparse-alt-symbol-alistp option-table)))) (let ((__function__ 'defdefparse-gen-code-for-element)) (declare (ignorable __function__)) (element-case elem :num-val (num-val-case elem.get :direct (cons (cons '(mv tree input) (cons (cons 'parse-direct (cons (cons 'list (num-val-direct->get elem.get)) '(input))) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input))))) :range (cons (cons '(mv tree input) (cons (cons 'parse-range (cons (num-val-range->min elem.get) (cons (num-val-range->max elem.get) '(input)))) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input)))))) :char-val (char-val-case elem.get :insensitive (cons (cons '(mv tree input) (cons (cons 'parse-ichars (cons (char-val-insensitive->get elem.get) '(input))) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input))))) :sensitive (cons (cons '(mv tree input) (cons (cons 'parse-schars (cons (char-val-sensitive->get elem.get) '(input))) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input)))))) :rulename (b* ((parse-rulename-fn (packn-pos (list prefix '- (str::upcase-string (rulename->get elem.get))) prefix))) (cons (cons '(mv tree input) (cons (cons parse-rulename-fn '(input)) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input)))))) :group (b* ((parse-group-fn (cdr (assoc-equal elem.get group-table)))) (cons (cons '(mv tree input) (cons (cons parse-group-fn '(input)) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input)))))) :option (b* ((parse-option-fn (cdr (assoc-equal elem.get option-table)))) (cons (cons '(mv tree input) (cons (cons parse-option-fn '(input)) 'nil)) (and check-error-p '(((when (reserrp tree)) (mv (reserrf-push tree) input)))))) :prose-val (raise "Prose value ~x0 not supported." elem.get))))
Theorem:
(defthm true-listp-of-defdefparse-gen-code-for-element (b* ((code (defdefparse-gen-code-for-element elem check-error-p prefix group-table option-table))) (true-listp code)) :rule-classes :rewrite)