Expand-ruleset
Expand rulesets to theories.
A ruleset is a list of so-called ruleset designators.
The ruleset operators, such as e/d* and def-ruleset,
expect arguments that are (or evaluate to) rulesets. Every ruleset represents
an ACL2 theory, called its ``expansion''. Consider for example these
ruleset definitions.
(def-ruleset my-rules
'(append reverse))
(def-ruleset other-rules
'(member-equal my-rules revappend))
Then the symbol my-rules is a ruleset designator, which represents the
theory containing append and reverse. The symbol other-rules is
a ruleset designator, which represents the theory containing member-equal,
append, reverse, and revappend. The function
expand-ruleset returns the theory obtained by expanding every ruleset
designator in a given ruleset, for example:
ACL2 !>(expand-ruleset '(car-cons (:d nth) other-rules) (w state))
(CAR-CONS (:D NTH)
MEMBER-EQUAL APPEND REVERSE REVAPPEND)
ACL2 !>
We now list the valid ruleset designators and indicate the corresponding
expansion, a theory, for each.
- A symbol that names a rule (e.g., from a definition or a theorem) or names
a theory is a ruleset designator. More generally, every runic
designator x is also a ruleset designator, which expands to the theory
containing exactly x. See theories for a discussion of runic
designators.
- If N is a symbol that is the name of a ruleset S, then N and
(:ruleset N) are ruleset designators. They expand to the union of the
expansions of the ruleset designators in S.
- The ruleset designators (:executable-counterpart-theory name),
(:current-theory name), and (:theory name) expand to the values in
the current ACL2 world of the forms (executable-counterpart-theory
name), (current-theory name), and (theory name), respectively.
- The ruleset designator (:rules-of-class class name) represent the
runes of the indicated class (see rule-classes) in the value of
(universal-theory name).
Definitions and Theorems
Function: expand-ruleset
(defun expand-ruleset (x world)
(if (ruleset-designator-listp x world)
(expand-ruleset1 x world)
(er hard 'expand-ruleset
"~x0 is not a valid ruleset.~%" x)))
