Plug-rules
Plug a list of rules into another list of rules.
- Signature
(plug-rules rules1 rules2) → rules
- Arguments
- rules1 — Guard (rulelistp rules1).
- rules2 — Guard (rulelistp rules2).
- Returns
- rules — Type (rulelistp rules).
This plugs rules2 into rules1, not vice versa.
This choice is motivated by the fact that grammar rules
are usually presented in a top-down manner,
and so it seems more natural to have
the ``plugged'' rules (e.g. HTTP)
appear before the ``plugging'' rules (e.g. URI).
After removing from rules1 the prose rules
whose names have definitions in rules2,
we find the rules in rules2 that transitively define
rule names referenced but not defined
in the remaining rules of rules1.
We append the rules found after the remaining rules of rules1.
Thus, prose rules in rules1 are effectively replaced
by corresponding rules in rules
(assuming that each prose rule removed from rules1
is the only rule in rules1 that defines its rule name).
Besides replacing prose-rules like this,
the plugging operation may also provide definitions
for rule names that are only referenced in rules1.
Prose rules in rules1
whose names do not have definitions in rules2
are not removed from rules1 and thus appear in the resulting rules.
Similarly, rules referenced in rules1
but defined neither in rules1 nor in rules2
remain referenced but not defined in the resulting rules.
These features allow multi-step plugging,
i.e. rules2 is plugged into rules1,
then rules3 is plugged into the result of the previous operation,
and so on.
Definitions and Theorems
Function: plug-rules
(defun plug-rules (rules1 rules2)
(declare (xargs :guard (and (rulelistp rules1)
(rulelistp rules2))))
(b* ((rules1 (remove-prose-rules rules1 rules2))
(rules2 (trans-rules-of-names
(difference (rulelist-called-rules rules1)
(rulelist-defined-rules rules1))
rules2)))
(append rules1 rules2)))
Theorem: rulelistp-of-plug-rules
(defthm rulelistp-of-plug-rules
(b* ((rules (plug-rules rules1 rules2)))
(rulelistp rules))
:rule-classes :rewrite)
