Generate the alist from rule names to rule name information, from a list of rules.
(deftreeops-gen-rulename-info-alist rules prefix) → info
Note that we generate an alist entry for each rule name, not rule: each rule name may be defined by multiple rules (the ones after the first incremental ones, in well-formed grammars), so we keep track of which rule names we have encountered already, so we can skip them when encountered again; when encountered the first time, we obtain its defining alternation (via lookup-rulename) and use it to generate the alist entry.
The generated alist has unique keys.
Function:
(defun deftreeops-gen-rulename-info-alist-aux (rules done prefix) (declare (xargs :guard (and (rulelistp rules) (rulename-listp done) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-rulename-info-alist-aux)) (declare (ignorable __function__)) (b* (((when (endp rules)) nil) (rule (car rules)) (rulename (rule->name rule)) ((when (member-equal rulename done)) (deftreeops-gen-rulename-info-alist-aux (cdr rules) done prefix)) (alt (lookup-rulename rulename rules)) (info (deftreeops-gen-rulename-info rulename alt prefix)) (more-info (deftreeops-gen-rulename-info-alist-aux (cdr rules) (cons rulename done) prefix))) (acons rulename info more-info))))
Theorem:
(defthm deftreeops-rulename-info-alistp-of-deftreeops-gen-rulename-info-alist-aux (b* ((info (deftreeops-gen-rulename-info-alist-aux rules done prefix))) (deftreeops-rulename-info-alistp info)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-rulename-info-alist (rules prefix) (declare (xargs :guard (and (rulelistp rules) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-rulename-info-alist)) (declare (ignorable __function__)) (deftreeops-gen-rulename-info-alist-aux rules nil prefix)))
Theorem:
(defthm deftreeops-rulename-info-alistp-of-deftreeops-gen-rulename-info-alist (b* ((info (deftreeops-gen-rulename-info-alist rules prefix))) (deftreeops-rulename-info-alistp info)) :rule-classes :rewrite)