		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rulename-info-alist

Generate the alist from rule names to rule name information, from a list of rules.

Signature
(deftreeops-gen-rulename-info-alist rules prefix) → info
Arguments: rules — Guard (rulelistp rules).; prefix — Guard (common-lisp::symbolp prefix).
Returns: info — Type (deftreeops-rulename-info-alistp 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.

Definitions and Theorems

Function: deftreeops-gen-rulename-info-alist-aux

(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: deftreeops-rulename-info-alistp-of-deftreeops-gen-rulename-info-alist-aux

(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: deftreeops-gen-rulename-info-alist

(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: deftreeops-rulename-info-alistp-of-deftreeops-gen-rulename-info-alist

(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)