Generate the terms to discriminate among two or more concatenations that form the alternation that defines a rule name.
(deftreeops-gen-discriminant-terms alt) → (mv terms alt-kind)
These are the terms used in
the
For now we only support alternations of the forms
listed in the description of
If the alternation does not have a supported form,
we return
If the alternation is a singleton,
we return a singleton list consisting of the term
Function:
(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:
(defthm true-listp-of-deftreeops-gen-discriminant-terms-aux1 (b* ((terms (deftreeops-gen-discriminant-terms-aux1 alt))) (true-listp terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-deftreeops-gen-discriminant-terms-aux1 (b* ((?terms (deftreeops-gen-discriminant-terms-aux1 alt))) (implies terms (equal (len terms) (len alt)))))
Function:
(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:
(defthm true-listp-of-deftreeops-gen-discriminant-terms-aux2 (b* ((terms (deftreeops-gen-discriminant-terms-aux2 alt))) (true-listp terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-deftreeops-gen-discriminant-terms-aux2 (b* ((?terms (deftreeops-gen-discriminant-terms-aux2 alt))) (implies terms (equal (len terms) (len alt)))))
Function:
(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:
(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:
(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:
(defthm len-of-deftreeops-gen-discriminant-terms (b* (((mv ?terms ?alt-kind) (deftreeops-gen-discriminant-terms alt))) (implies terms (equal (len terms) (len alt)))))