		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-reorder-alternation

Reorder the alternatives of an alternation.

Signature
(defdefparse-reorder-alternation alt order) → new-alt
Arguments: alt — Guard (alternationp alt).; order — Guard (pos-listp order).
Returns: new-alt — Type (alternationp new-alt).

The order list must be a permutation of the list (1 ... n), where n is the number of alternatives in alt. We return the alternative, permuted according to the list.

This serves to try an alternative before another one, in order to satisfy extra-grammatical requirements.

Definitions and Theorems

Function: defdefparse-reorder-alternation

(defun defdefparse-reorder-alternation (alt order)
  (declare (xargs :guard (and (alternationp alt)
                              (pos-listp order))))
  (let ((__function__ 'defdefparse-reorder-alternation))
    (declare (ignorable __function__))
    (b* (((when (endp order)) nil)
         (index (1- (car order)))
         ((unless (< index (len alt)))
          (raise "Bad position ~x0 in ~x1." (car order)
                 alt)))
      (cons (concatenation-fix (nth index alt))
            (defdefparse-reorder-alternation alt (cdr order))))))

Theorem: alternationp-of-defdefparse-reorder-alternation

(defthm alternationp-of-defdefparse-reorder-alternation
  (b* ((new-alt (defdefparse-reorder-alternation alt order)))
    (alternationp new-alt))
  :rule-classes :rewrite)