Generate the events for a rule name.
(deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos) → (mv nonleaf-thm-event rulename-thm-event match-thm-event concs-thm-event conc-equivs-thm-event? check-conc-fn-event? get-tree-list-list-fn-events conc-matching-thm-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist)
Function:
(defun deftreeops-gen-rulename-events-aux1 (alt conc-matchp) (declare (xargs :guard (and (alternationp alt) (common-lisp::symbolp conc-matchp)))) (let ((__function__ 'deftreeops-gen-rulename-events-aux1)) (declare (ignorable __function__)) (cond ((endp alt) nil) (t (cons (cons conc-matchp (cons 'cstss (cons (pretty-print-concatenation (car alt)) 'nil))) (deftreeops-gen-rulename-events-aux1 (cdr alt) conc-matchp))))))
Theorem:
(defthm true-listp-of-deftreeops-gen-rulename-events-aux1 (b* ((disjuncts (deftreeops-gen-rulename-events-aux1 alt conc-matchp))) (true-listp disjuncts)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-rulename-events-aux2 (alt alt-kind conc-infos rulename-infos charval-infos conc-matchp) (declare (xargs :guard (and (alternationp alt) (natp alt-kind) (deftreeops-conc-info-listp conc-infos) (deftreeops-rulename-info-alistp rulename-infos) (deftreeops-charval-info-alistp charval-infos) (common-lisp::symbolp conc-matchp)))) (declare (xargs :guard (equal (len conc-infos) (len alt)))) (let ((__function__ 'deftreeops-gen-rulename-events-aux2)) (declare (ignorable __function__)) (b* (((when (endp alt)) (mv nil nil nil)) (conc (car alt)) ((deftreeops-conc-info conc-info) (car conc-infos)) ((unless (and (consp conc) (endp (cdr conc)))) (raise "Internal error: non-singleton concatenation ~x0." conc) (mv nil nil nil)) (rep (car conc)) ((unless (equal (repetition->range rep) (make-repeat-range :min 1 :max (nati-finite 1)))) (raise "Internal error: non-singleton repetition ~x0." rep) (mv nil nil nil)) (elem (repetition->element rep)) (conjunct (cons 'iff (cons (cons conc-matchp (cons '(tree-nonleaf->branches cst) (cons (pretty-print-element elem) 'nil))) (cons conc-info.discriminant-term 'nil)))) ((unless (and (consp conc-info.rep-infos) (endp (cdr conc-info.rep-infos)))) (raise "Internal error: non-singleton list of repetition information ~x0." conc-info.rep-infos) (mv nil nil nil)) ((deftreeops-rep-info rep-info) (car conc-info.rep-infos)) (rules (list conc-info.matching-thm rep-info.matching-thm)) (lemma-instance (cond ((element-case elem :rulename) (b* ((rulename (element-rulename->get elem)) (rulename-info (cdr (assoc-equal rulename rulename-infos))) ((unless rulename-info) (raise "Internal error: no information for rule name ~x0." rulename))) (if (= alt-kind 1) (cons ':instance (cons (deftreeops-rulename-info->rulename-thm rulename-info) '((cst (nth 0 (nth 0 (tree-nonleaf->branches cst))))))) (cons ':instance (cons (deftreeops-rulename-info->nonleaf-thm rulename-info) '((cst (nth 0 (nth 0 (tree-nonleaf->branches cst)))))))))) ((element-case elem :char-val) (b* ((charval (element-char-val->get elem)) (charval-info (cdr (assoc-equal charval charval-infos))) ((unless charval-info) (raise "Internal error: no information for ~ character value notation ~x0." charval))) (cons ':instance (cons (deftreeops-charval-info->leafterm-thm charval-info) '((cst (nth 0 (nth 0 (tree-nonleaf->branches cst))))))))) (t (raise "Internal error: found element ~x0." elem)))) ((mv more-conjuncts more-rules more-lemma-instances) (deftreeops-gen-rulename-events-aux2 (cdr alt) alt-kind (cdr conc-infos) rulename-infos charval-infos conc-matchp))) (mv (cons conjunct more-conjuncts) (append rules more-rules) (cons lemma-instance more-lemma-instances)))))
Theorem:
(defthm true-listp-of-deftreeops-gen-rulename-events-aux2.conjuncts (b* (((mv ?conjuncts ?rules ?lemma-instances) (deftreeops-gen-rulename-events-aux2 alt alt-kind conc-infos rulename-infos charval-infos conc-matchp))) (true-listp conjuncts)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-deftreeops-gen-rulename-events-aux2.rules (b* (((mv ?conjuncts ?rules ?lemma-instances) (deftreeops-gen-rulename-events-aux2 alt alt-kind conc-infos rulename-infos charval-infos conc-matchp))) (symbol-listp rules)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-deftreeops-gen-rulename-events-aux2.lemma-instances (b* (((mv ?conjuncts ?rules ?lemma-instances) (deftreeops-gen-rulename-events-aux2 alt alt-kind conc-infos rulename-infos charval-infos conc-matchp))) (true-listp lemma-instances)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-rulename-events-aux3 (alt conc-infos i rulename-infos) (declare (xargs :guard (and (alternationp alt) (deftreeops-conc-info-listp conc-infos) (posp i) (deftreeops-rulename-info-alistp rulename-infos)))) (declare (xargs :guard (equal (len conc-infos) (len alt)))) (let ((__function__ 'deftreeops-gen-rulename-events-aux3)) (declare (ignorable __function__)) (b* (((when (endp alt)) (mv nil nil nil)) (conc (car alt)) ((deftreeops-conc-info conc-info) (car conc-infos)) ((unless (and (consp conc) (endp (cdr conc)))) (raise "Internal error: non-singleton concatenation ~x0." conc) (mv nil nil nil)) (rep (car conc)) ((unless (equal (repetition->range rep) (make-repeat-range :min 1 :max (nati-finite 1)))) (raise "Internal error: non-singleton repetition ~x0." rep) (mv nil nil nil)) (elem (repetition->element rep)) ((unless (element-case elem :rulename)) (raise "Internal error: element ~x0 is not a rule name." elem) (mv nil nil nil)) (rulename (element-rulename->get elem)) (cond-arm (cons conc-info.discriminant-term (cons i 'nil))) (disjunct (cons 'equal (cons 'number (cons i 'nil)))) (rep-infos (deftreeops-conc-info->rep-infos conc-info)) ((unless (and (consp rep-infos) (endp (cdr rep-infos)))) (raise "Internal error: non-singleton list of repetition information ~x0." rep-infos) (mv nil nil nil)) ((deftreeops-rep-info rep-info) (car rep-infos)) (rulename-info (cdr (assoc-equal rulename rulename-infos))) ((unless rulename-info) (raise "Internal error: no information for rule name ~x0." rulename) (mv nil nil nil)) (rules (list (deftreeops-rulename-info->nonleaf-thm rulename-info) (deftreeops-rulename-info->rulename-thm rulename-info) conc-info.matching-thm rep-info.matching-thm)) ((mv more-cond-arms more-disjuncts more-rules) (deftreeops-gen-rulename-events-aux3 (cdr alt) (cdr conc-infos) (1+ i) rulename-infos))) (mv (cons cond-arm more-cond-arms) (cons disjunct more-disjuncts) (append rules more-rules)))))
Theorem:
(defthm true-listp-of-deftreeops-gen-rulename-events-aux3.cond-arms (b* (((mv ?cond-arms ?disjuncts ?rules) (deftreeops-gen-rulename-events-aux3 alt conc-infos i rulename-infos))) (true-listp cond-arms)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-deftreeops-gen-rulename-events-aux3.disjuncts (b* (((mv ?cond-arms ?disjuncts ?rules) (deftreeops-gen-rulename-events-aux3 alt conc-infos i rulename-infos))) (true-listp disjuncts)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-deftreeops-gen-rulename-events-aux3.rules (b* (((mv ?cond-arms ?disjuncts ?rules) (deftreeops-gen-rulename-events-aux3 alt conc-infos i rulename-infos))) (symbol-listp rules)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-rulename-events (rulename alt info prefix rulename-infos charval-infos) (declare (xargs :guard (and (rulenamep rulename) (alternationp alt) (deftreeops-rulename-infop info) (common-lisp::symbolp prefix) (deftreeops-rulename-info-alistp rulename-infos) (deftreeops-charval-info-alistp charval-infos)))) (let ((__function__ 'deftreeops-gen-rulename-events)) (declare (ignorable __function__)) (b* (((deftreeops-rulename-info info) info) (rulename-string (rulename->get rulename)) (alt-string (pretty-print-alternation alt)) (matchp (deftreeops-match-pred prefix)) (alt-matchp (deftreeops-alt-match-pred prefix)) (conc-matchp (deftreeops-conc-match-pred prefix)) ((unless (equal (len info.conc-infos) (len alt))) (raise "Internal error: ~x0 and ~x1 have different lengths." info.conc-infos alt) (mv '(_) '(_) '(_) '(_) nil nil nil nil nil nil nil nil)) (alt-singletonp (and (consp alt) (endp (cdr alt)))) ((mv conc-matching-thm-events check-conc-fn-equiv-thm-events get-tree-list-list-fn-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist) (deftreeops-gen-conc-list-events alt info.conc-infos info.conc-equivs-thm info.check-conc-fn info.nonleaf-thm info.match-thm alt-singletonp rulename prefix)) (nonleaf-thm-event (cons 'defruled (cons info.nonleaf-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) '((equal (tree-kind cst) :nonleaf)))) (cons ':in-theory (cons (cons 'quote (cons (cons matchp '(tree-nonleaf-when-match-rulename/group/option (:e element-kind) (:e member-equal))) 'nil)) 'nil)))))) (rulename-thm-event (cons 'defruled (cons info.rulename-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'equal (cons '(tree-nonleaf->rulename? cst) (cons (cons 'rulename (cons rulename-string 'nil)) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons matchp '(tree-rulename-when-match-rulename (:e element-kind) (:e element-rulename->get) (:e rulename))) 'nil)) 'nil)))))) (match-thm-event (cons 'defruled (cons info.match-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons alt-matchp (cons '(tree-nonleaf->branches cst) (cons alt-string 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons matchp (cons alt-matchp '(tree-branches-match-alt-when-match-rulename tree-terminatedp (:e element-kind) (:e element-rulename->get) (:e lookup-rulename)))) 'nil)) (cons ':use (cons info.nonleaf-thm 'nil)))))))) (concs-thm-event (cons 'defruled (cons info.concs-thm (cons (cons 'implies (cons (cons alt-matchp (cons 'cstss (cons alt-string 'nil))) (cons (cons 'or (deftreeops-gen-rulename-events-aux1 alt conc-matchp)) 'nil))) (cons ':do-not (cons ''(preprocess) (cons ':in-theory (cons (cons 'quote (cons (cons alt-matchp (cons conc-matchp '(tree-list-list-match-alternation-p-when-atom-alternation tree-list-list-match-alternation-p-of-cons-alternation))) 'nil)) 'nil)))))))) (conc-equivs-thm-event? (and info.conc-equivs-thm (b* (((mv conjuncts rules lemma-instances) (deftreeops-gen-rulename-events-aux2 alt info.alt-kind info.conc-infos rulename-infos charval-infos conc-matchp))) (cons (cons 'defruled (cons info.conc-equivs-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'and conjuncts) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (append (if (= info.alt-kind 1) '((:e rulename)) nil) (cons info.match-thm rules)) 'nil)) (cons ':use (cons (cons (cons ':instance (cons info.concs-thm '((cstss (tree-nonleaf->branches cst))))) lemma-instances) 'nil))))))) 'nil)))) (check-conc-fn-event? (and info.check-conc-fn (b* (((mv cond-arms disjuncts rules) (deftreeops-gen-rulename-events-aux3 alt info.conc-infos 1 rulename-infos))) (cons (cons 'define (cons info.check-conc-fn (cons '((cst treep)) (cons ':guard (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons ':returns (cons (cons 'number (cons 'posp (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.check-conc-fn '((:e posp))) 'nil)) 'nil))) 'nil) 'nil)))) (cons (cons 'cond (append cond-arms '((t (prog2$ (acl2::impossible) 1))))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'acl2::true-listp-of-nth-when-true-list-listp (cons '(:t tree-nonleaf->branches) (cons 'true-list-listp-of-tree-nonleaf->branches (cons 'treep-of-nth-when-tree-listp (cons 'tree-listp-of-nth-when-tree-list-listp (cons 'tree-list-listp-of-tree-nonleaf->branches (cons '(:e rulename) (cons '(:e nfix) (cons info.nonleaf-thm (cons info.match-thm rules)))))))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons info.concs-thm '((cstss (tree-nonleaf->branches cst))))) 'nil) 'nil))))) 'nil) (cons '/// (cons (cons 'more-returns (cons (cons 'number (cons (cons 'or disjuncts) (cons ':name (cons (packn-pos (list info.check-conc-fn '-possibilities) info.check-conc-fn) (cons ':rule-classes (cons (cons (cons ':forward-chaining (cons ':trigger-terms (cons (cons (cons info.check-conc-fn '(cst)) 'nil) 'nil))) 'nil) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.check-conc-fn 'nil) 'nil)) 'nil))) 'nil) 'nil)))))))) 'nil)) (cons (cons 'fty::deffixequiv (cons info.check-conc-fn (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.check-conc-fn '(tree-nonleaf->branches$inline-tree-equiv-congruence-on-x tree-fix-under-tree-equiv)) 'nil)) 'nil))) 'nil) 'nil)))) check-conc-fn-equiv-thm-events))))))))))))) 'nil))))) (mv nonleaf-thm-event rulename-thm-event match-thm-event concs-thm-event conc-equivs-thm-event? check-conc-fn-event? get-tree-list-list-fn-events conc-matching-thm-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events (append event-alist (list (cons info.nonleaf-thm nonleaf-thm-event)) (list (cons info.rulename-thm rulename-thm-event)) (list (cons info.match-thm match-thm-event)) (list (cons info.concs-thm concs-thm-event)) (and conc-equivs-thm-event? (list (cons info.conc-equivs-thm (car conc-equivs-thm-event?)))) (and check-conc-fn-event? (list (cons info.check-conc-fn (car check-conc-fn-event?)))))))))
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-rulename-events.nonleaf-thm-event (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-formp nonleaf-thm-event)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-rulename-events.rulename-thm-event (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-formp rulename-thm-event)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-rulename-events.match-thm-event (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-formp match-thm-event)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-deftreeops-gen-rulename-events.concs-thm-event (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-formp concs-thm-event)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.conc-equivs-thm-event? (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp conc-equivs-thm-event?)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.check-conc-fn-event? (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp check-conc-fn-event?)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.get-tree-list-list-fn-events (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.conc-matching-thm-events (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp conc-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.rep-matching-thm-events (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp rep-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.get-tree-list-fn-events (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rulename-events.get-tree-fn-events (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-rulename-events.event-alist (b* (((mv ?nonleaf-thm-event ?rulename-thm-event ?match-thm-event ?concs-thm-event ?conc-equivs-thm-event? ?check-conc-fn-event? ?get-tree-list-list-fn-events ?conc-matching-thm-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-rulename-events rulename alt info prefix rulename-infos charval-infos))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)