		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-code-for-alternation

Generate code to parse an instance of an ABNF alternation.

Signature
(defdefparse-gen-code-for-alternation alt order prefix group-table option-table repetition-table) → code
Arguments: alt — Guard (alternationp alt).; order — Guard (pos-listp order).; prefix — Guard (common-lisp::symbolp prefix).; group-table — Guard (defdefparse-alt-symbol-alistp group-table).; option-table — Guard (defdefparse-alt-symbol-alistp option-table).; repetition-table — Guard (defdefparse-rep-symbol-alistp repetition-table).
Returns: code — Type (true-listp code).

After possibly reordering the alternatives, we generate code that tries every alternative. We use variables treess<index> to store either the resulting list of lists of trees or an error. For each alternative, we generate code for the concatenation and bind the result to treess<index>, returning as soon as we get a non-error. If all the alternatives give an error, we return an error that includes all the errors for the alternatives: this is the reason for using and incrementing indices, i.e. so that we can combine them in case of error, not because we want to combine them in case of success.

Note that for each attempt to parse an alternative we bind the variable input1 to the remaining input, not the variable input. This is because we need to backtrack in case of failure, discarding input1 and going back to the previous input.

Definitions and Theorems

Function: defdefparse-gen-code-for-alternation-aux

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

(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: symbol-listp-of-defdefparse-gen-code-for-alternation-aux.vars

(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: defdefparse-gen-code-for-alternation

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

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