		Search-engine friendly clone of the ACL2 documentation.

Closure

Calc-trans-rules-of-names

Calculate the rules from a list of rules that transitively define names in a list of rule names, collecting them into an accumulator (list of rules).

Signature
(calc-trans-rules-of-names workset accumulator rules) → result
Arguments: workset — Guard (rulename-setp workset).; accumulator — Guard (rulelistp accumulator).; rules — Guard (rulelistp rules).
Returns: result — Type (rulelistp result).

This is a work set algorithm. When the work set is empty, we are done and we return the rules collected so far. Otherwise, we remove one rule name from the work set and take out of rules the rules that define it. If no rules in rules define the rule name, we make a recursive call to examine the next rule name in the work set. Otherwise, we add these rules to the current result, extend the work set with the rule names referenced by these rules, and make a recursive call to re-examine the work set.

The algorithm makes progress either by reducing the length of rules (if rules are taken out of rules), or by reducing the size of the work set (if no rules are taken out of rules), in which case the length of rules stays the same.

Definitions and Theorems

Function: calc-trans-rules-of-names

(defun calc-trans-rules-of-names (workset accumulator rules)
  (declare (xargs :guard (and (rulename-setp workset)
                              (rulelistp accumulator)
                              (rulelistp rules))))
  (b* (((when (emptyp workset))
        (rulelist-fix accumulator))
       (rulename (head workset))
       (workset (tail workset))
       ((mv rulename-rules other-rules)
        (rules-of-name rulename rules))
       ((when (not rulename-rules))
        (calc-trans-rules-of-names workset accumulator rules))
       (workset (union workset
                       (rulelist-called-rules rulename-rules)))
       (accumulator (append accumulator rulename-rules)))
    (calc-trans-rules-of-names workset accumulator other-rules)))

Theorem: rulelistp-of-calc-trans-rules-of-names

(defthm rulelistp-of-calc-trans-rules-of-names
  (b*
    ((result (calc-trans-rules-of-names workset accumulator rules)))
    (rulelistp result))
  :rule-classes :rewrite)