		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-discriminant-terms

Generate the terms to discriminate among two or more concatenations that form the alternation that defines a rule name.

Signature
(deftreeops-gen-discriminant-terms alt) → (mv terms alt-kind)
Arguments: alt — Guard (alternationp alt).
Returns: terms — Type (true-listp terms).; alt-kind — Type (natp alt-kind).

These are the terms used in the <prefix>-<rulename>-conc-equivs theorem described in deftreeops.

For now we only support alternations of the forms listed in the description of <prefix>-<rulename>-conc-equivs in deftreeops. The alt-kind result of this function indicates which one, as a positive integer in the same order as listed, or it is 0 if the alternation is a singleton or does not have a supported form, i.e. if there is no need to indicate the supported form.

If the alternation does not have a supported form, we return nil as the terms result; otherwise, we return a list of terms, of the same length as the alternation. Recall that deftreeops requires the grammar to be well-formed, and that well-formed grammars have non-empty alternations: so the terms result cannot be nil if the alternation is supported.

If the alternation is a singleton, we return a singleton list consisting of the term t, which makes sense since the concatenation must be always that only one. Otherwise, we check for different forms of the two or more alternatives:

If the alternation consists of two or more concatenations each of which is a singleton, each consisting of a repetition with range 1 whose element is a rule name: then we return two or more terms, each of which checks whether the one subtree has the corresponding rule name as root.
If the alternation consists of exactly two concatenations, one of which is a singleton of a repetition with range 1 whose element is numeric or character value notation, and the other is a singleton of a repetition with range 1 whose element is a rule name: then we return two terms, one that checks whether the one subtree is a terminal leaf (for the numeric or character value notation case), and the other that checks whether the one subtree is a non-leaf (for the other case).

Definitions and Theorems

Function: deftreeops-gen-discriminant-terms-aux1

(defun deftreeops-gen-discriminant-terms-aux1 (alt)
 (declare (xargs :guard (alternationp alt)))
 (declare (xargs :guard (consp alt)))
 (let ((__function__ 'deftreeops-gen-discriminant-terms-aux1))
  (declare (ignorable __function__))
  (b*
   ((conc (car alt))
    ((unless (and (consp conc) (endp (cdr conc))))
     nil)
    (rep (car conc))
    ((unless (equal (repetition->range rep)
                    (make-repeat-range :min 1
                                       :max (nati-finite 1))))
     nil)
    (elem (repetition->element rep))
    ((unless (element-case elem :rulename))
     nil)
    (rulename (element-rulename->get elem))
    (term
     (cons 'equal
           (cons '(tree-nonleaf->rulename?
                       (nth 0 (nth 0 (tree-nonleaf->branches cst))))
                 (cons (cons 'rulename
                             (cons (rulename->get rulename) 'nil))
                       'nil))))
    (alt (cdr alt))
    ((when (endp alt)) (list term))
    (terms (deftreeops-gen-discriminant-terms-aux1 alt))
    ((unless terms) nil))
   (cons term terms))))

Theorem: true-listp-of-deftreeops-gen-discriminant-terms-aux1

(defthm true-listp-of-deftreeops-gen-discriminant-terms-aux1
  (b* ((terms (deftreeops-gen-discriminant-terms-aux1 alt)))
    (true-listp terms))
  :rule-classes :rewrite)

Theorem: len-of-deftreeops-gen-discriminant-terms-aux1

(defthm len-of-deftreeops-gen-discriminant-terms-aux1
  (b* ((?terms (deftreeops-gen-discriminant-terms-aux1 alt)))
    (implies terms (equal (len terms) (len alt)))))

Function: deftreeops-gen-discriminant-terms-aux2

(defun deftreeops-gen-discriminant-terms-aux2 (alt)
 (declare (xargs :guard (alternationp alt)))
 (declare (xargs :guard (and (consp alt) (consp (cdr alt)))))
 (let ((__function__ 'deftreeops-gen-discriminant-terms-aux2))
  (declare (ignorable __function__))
  (b*
   (((unless (endp (cddr alt))) nil)
    (conc1 (car alt))
    (conc2 (cadr alt))
    ((unless (and (consp conc1)
                  (consp conc2)
                  (endp (cdr conc1))
                  (endp (cdr conc2))))
     nil)
    (rep1 (car conc1))
    (rep2 (car conc2))
    ((unless (and (equal (repetition->range rep1)
                         (make-repeat-range :min 1
                                            :max (nati-finite 1)))
                  (equal (repetition->range rep2)
                         (make-repeat-range :min 1
                                            :max (nati-finite 1)))))
     nil)
    (elem1 (repetition->element rep1))
    (elem2 (repetition->element rep2)))
   (cond
     ((and (element-case elem1 :rulename)
           (element-case elem2 :char-val))
      (list '(tree-case (nth 0 (nth 0 (tree-nonleaf->branches cst)))
                        :nonleaf)
            '(tree-case (nth 0 (nth 0 (tree-nonleaf->branches cst)))
                        :leafterm)))
     ((and (element-case elem1 :char-val)
           (element-case elem2 :rulename))
      (list '(tree-case (nth 0 (nth 0 (tree-nonleaf->branches cst)))
                        :leafterm)
            '(tree-case (nth 0 (nth 0 (tree-nonleaf->branches cst)))
                        :nonleaf)))
     (t nil)))))

Theorem: true-listp-of-deftreeops-gen-discriminant-terms-aux2

(defthm true-listp-of-deftreeops-gen-discriminant-terms-aux2
  (b* ((terms (deftreeops-gen-discriminant-terms-aux2 alt)))
    (true-listp terms))
  :rule-classes :rewrite)

Theorem: len-of-deftreeops-gen-discriminant-terms-aux2

(defthm len-of-deftreeops-gen-discriminant-terms-aux2
  (b* ((?terms (deftreeops-gen-discriminant-terms-aux2 alt)))
    (implies terms (equal (len terms) (len alt)))))

Function: deftreeops-gen-discriminant-terms

(defun deftreeops-gen-discriminant-terms (alt)
  (declare (xargs :guard (alternationp alt)))
  (let ((__function__ 'deftreeops-gen-discriminant-terms))
    (declare (ignorable __function__))
    (b* (((when (endp alt)) (mv nil 0))
         ((when (endp (cdr alt)))
          (mv (list t) 0))
         (terms? (deftreeops-gen-discriminant-terms-aux1 alt))
         ((when terms?) (mv terms? 1))
         (terms? (deftreeops-gen-discriminant-terms-aux2 alt))
         ((when terms?) (mv terms? 2)))
      (mv nil 0))))

Theorem: true-listp-of-deftreeops-gen-discriminant-terms.terms

(defthm true-listp-of-deftreeops-gen-discriminant-terms.terms
  (b* (((mv ?terms ?alt-kind)
        (deftreeops-gen-discriminant-terms alt)))
    (true-listp terms))
  :rule-classes :rewrite)

Theorem: natp-of-deftreeops-gen-discriminant-terms.alt-kind

(defthm natp-of-deftreeops-gen-discriminant-terms.alt-kind
  (b* (((mv ?terms ?alt-kind)
        (deftreeops-gen-discriminant-terms alt)))
    (natp alt-kind))
  :rule-classes :rewrite)

Theorem: len-of-deftreeops-gen-discriminant-terms

(defthm len-of-deftreeops-gen-discriminant-terms
  (b* (((mv ?terms ?alt-kind)
        (deftreeops-gen-discriminant-terms alt)))
    (implies terms (equal (len terms) (len alt)))))