		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-code-for-element

Generate code to parse an instance of an ABNF element.

Signature
(defdefparse-gen-code-for-element elem check-error-p prefix group-table option-table) → code
Arguments: elem — Guard (elementp elem).; check-error-p — Guard (booleanp check-error-p).; prefix — Guard (common-lisp::symbolp prefix).; group-table — Guard (defdefparse-alt-symbol-alistp group-table).; option-table — Guard (defdefparse-alt-symbol-alistp option-table).
Returns: code — Type (true-listp 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 tree (for a tree or error) and input (for the remaining input). If the check-error-p flag is set, we also generate a b* to propagate the error, if tree is an error.

Definitions and Theorems

Function: defdefparse-gen-code-for-element

(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: true-listp-of-defdefparse-gen-code-for-element

(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)