Generate the terms to discriminate among two or more concatenations that form the alternation that defines a rule name.
(deftreeops-gen-discriminant-terms alt) → terms
These are the terms used in
the
For now we only support alternations of certain forms.
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-aux (alt) (declare (xargs :guard (alternationp alt))) (declare (xargs :guard (consp alt))) (let ((__function__ 'deftreeops-gen-discriminant-terms-aux)) (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-aux alt)) ((unless terms) nil)) (cons term terms))))
Theorem:
(defthm true-listp-of-deftreeops-gen-discriminant-terms-aux (b* ((terms (deftreeops-gen-discriminant-terms-aux alt))) (true-listp terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-deftreeops-gen-discriminant-terms-aux (b* ((?terms (deftreeops-gen-discriminant-terms-aux 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)) nil) ((when (endp (cdr alt))) (list t))) (deftreeops-gen-discriminant-terms-aux alt))))
Theorem:
(defthm true-listp-of-deftreeops-gen-discriminant-terms (b* ((terms (deftreeops-gen-discriminant-terms alt))) (true-listp terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-deftreeops-gen-discriminant-terms (b* ((?terms (deftreeops-gen-discriminant-terms alt))) (implies terms (equal (len terms) (len alt)))))