rulesets

(in-package "ACL2")

(program)

(defxdoc rulesets
  :parents (theories deftheory)
  :short "Table-based alternative to ACL2's named theories."
  :long "<p>Rulesets are like @(see theories), but can be extended with
additional rules after first being defined.  That is, you can build up a
ruleset incrementally, across many books, instead of having to define it all at
once and having it be forever fixed.</p>

<p>Basic usage of rulesets is just like theories.  You can:</p>

<ul>
<li>Introduce rulesets with @(see def-ruleset)</li>
<li>Extend existing rulesets with @(see add-to-ruleset).</li>
<li>Enable/disable rulesets with @(see enable*), @(see disable*), and @(see
e/d*)</li>
</ul>

<p>When we define a new package @('FOO'), we often set up @('FOO::enable') as
an alias for @('enable*'), to make using rulesets more convenient.</p>

<p>Advanced users can do some nifty things with rulesets, e.g., you can have a
superior ruleset that contains other rulesets, and it will grow as you add
rules to the contained rulesets.</p>

<p>A ruleset is actually a list of so-called <i>ruleset designators</i>.  All
ruleset operators, such as @(tsee e/d*) and @(tsee def-ruleset), take arguments
that are rulesets.  See @(see expand-ruleset) for a discussion of ruleset
designators and the corresponding @(see theories) that they represent.</p>")

(defsection get-ruleset
  :parents (rulesets)
  :short "The @(see ruleset) associated with a given name"
  :long "<p>Example usage:</p>

@({ (get-ruleset 'my-ruleset (w state)) })

<p>Also see @(see ruleset).  For a more powerful operator that recursively
expands ruleset names within a given ruleset, see @(see expand-ruleset).</p>"
  (defun get-ruleset
    (name world)
    (let* ((ruleset-alist (table-alist 'ruleset-table world)))
      (cdr (assoc name ruleset-alist)))))

(defsection ruleset
  :parents (rulesets)
  :short "The ruleset associated with a given name"
  :long "<p>See @(see rulesets) for an introduction to rulesets.</p>

<p>Examples of calls of @('ruleset'):</p>

@({
 (ruleset 'my-ruleset) ; assumes that WORLD is bound
 (ruleset 'my-ruleset (w state)) ; ruleset currently associated with MY-RULESET
})

<p>Also see @(see get-ruleset).  For a more powerful operator that recursively
expands ruleset names within a given ruleset, see @(see expand-ruleset).</p>"
  (defmacro ruleset
    (name &optional (world 'world))
    `(get-ruleset ,NAME ,WORLD)))

(defsection def-ruleset
  :parents (rulesets)
  :short "@(call def-ruleset) creates a new @(see ruleset)."
  :long "<p>Examples:</p>
@({
 (def-ruleset my-rules
   '(append reverse))

 (def-ruleset other-rules
   '(member-equal my-rules revappend))
})

<p>The first example creates a new ruleset, @('my-rules'), with only the
definitions of @('append') and @('reverse').</p>

<p>The section example creates a new ruleset, @('other-rules'), with the
definitions of @('member-equal') and @('revappend'), and also a link to
@('my-rules').  When rules are added to @('my-rules'), @('other-rules')
also grows.</p>

<p>See @(see def-ruleset!) for a version that's more friendly towards
redundant calls.</p>"
  (defmacro def-ruleset
    (name form)
    (declare (xargs :guard (symbolp name)))
    `(make-event (let ((world (w state)) (name ',NAME))
        (er-progn (check-not-ruleset name world state)
          (let ((rules ,(RULESET-FORM-PREPROCESS FORM)))
            (def-ruleset-core name rules world state)))))))

(defsection add-to-ruleset
  :parents (rulesets)
  :short "@(call add-to-ruleset) adds additional rules to an existing
@(see ruleset)."
  :long "<p>Examples:</p>
@({
 (add-to-ruleset my-rules
   '(foop))

 (add-to-ruleset other-rules
   '(car-cons cdr-cons (force)))
})"
  (defmacro add-to-ruleset
    (name form)
    (declare (xargs :guard (symbolp name)))
    `(make-event (let ((world (w state)) (name ',NAME))
        (er-progn (check-ruleset name world state)
          (let ((rules ,(RULESET-FORM-PREPROCESS FORM)))
            (add-to-ruleset-core name rules world state)))))))

(defsection def-ruleset!
  :parents (rulesets)
  :short "Same as @(see def-ruleset) except that it does not complain if the
@(see ruleset) already exists, instead acting like @('add-to-ruleset') in that
case."
  (defmacro def-ruleset!
    (name form)
    (declare (xargs :guard (symbolp name)))
    `(make-event (let* ((world (w state)) (name ',NAME)
          (rules ,(RULESET-FORM-PREPROCESS FORM)))
        (if (is-ruleset name world)
          (add-to-ruleset-core name rules world state)
          (def-ruleset-core name rules world state))))))

(defsection expand-ruleset
  :parents (rulesets)
  :short "Expand @(see rulesets) to @(see theories)."
  :long "<p>A @(see ruleset) is a list of so-called <i>ruleset designators</i>.
The @(see ruleset) operators, such as @(tsee e/d*) and @(tsee def-ruleset),
expect arguments that are (or evaluate to) rulesets.  Every ruleset represents
an ACL2 <i>theory</i>, called its ``expansion''.  Consider for example these
ruleset definitions.</p>

@({
 (def-ruleset my-rules
   '(append reverse))

 (def-ruleset other-rules
   '(member-equal my-rules revappend))
})

<p>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:</p>

@({
 ACL2 !>(expand-ruleset '(car-cons (:d nth) other-rules) (w state))
 (CAR-CONS (:D NTH)
           MEMBER-EQUAL APPEND REVERSE REVAPPEND)
 ACL2 !>
})

<p>We now list the valid ruleset designators and indicate the corresponding
expansion, a theory, for each.</p>

<ul>

<li>A symbol that names a rule (e.g., from a definition or a theorem) or names
a @(see theory) is a ruleset designator.  More generally, every <i>runic
designator</i> @('x') is also a ruleset designator, which expands to the theory
containing exactly @('x').  See @(see theories) for a discussion of runic
designators.</li>

<li>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').</li>

<li>The ruleset designators @('(:executable-counterpart-theory name)'),
@('(:current-theory name)'), and @('(:theory name)') expand to the values in
the current ACL2 @(see world) of the forms @('(executable-counterpart-theory
name)'), @('(current-theory name)'), and @('(theory name)'), respectively.</li>

<li>The ruleset designator @('(:rules-of-class class name)') represent the
runes of the indicated class (see @(see rule-classes)) in the value of
@('(universal-theory name)').</li>

</ul>"
  (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))))

(defsection enable*
  :parents (rulesets)
  :short "@(csee Ruleset)-aware version of @(see enable)."
  :long "<p>Examples:</p>

@({
 (in-theory (enable* my-rules append car-cons))

 (defthm ...
    :hints (("Goal" :in-theory (enable* foo ...))))
})"
  (defmacro enable*
    (&rest x)
    `(union-current-theory-fn (expand-ruleset ',X world)
      nil
      world)))

(defsection disable*
  :parents (rulesets)
  :short "@(csee Ruleset)-aware version of @(see disable)."
  :long "<p>Examples:</p>

@({
 (in-theory (disable* my-rules append car-cons))

 (defthm ...
    :hints (("Goal" :in-theory (disable* foo ...))))
})"
  (defmacro disable*
    (&rest x)
    `(set-difference-current-theory-fn (expand-ruleset ',X world)
      nil
      world)))

(defsection e/d*
  :parents (rulesets)
  :short "@(csee Ruleset)-aware version of @(see e/d)."
  :long "<p>Examples:</p>

@({
 (in-theory (e/d* (unusual-rules append)
                  (expensive-rules default-car default-cdr)))

 (defthm ...
    :hints (("Goal"
             :in-theory (e/d* (unusual-rules append)
                              (expensive-rules default-car
                               default-cdr)))))
})"
  (defun e/d*-fn
    (theory e/d-list enable-p)
    (declare (xargs :guard (and (true-list-listp e/d-list)
          (or (eq enable-p t) (eq enable-p nil)))))
    (cond ((atom e/d-list) theory)
      (enable-p (e/d*-fn `(union-theories ,THEORY
            (expand-ruleset ',(CAR E/D-LIST) world))
          (cdr e/d-list)
          nil))
      (t (e/d*-fn `(set-difference-theories ,THEORY
            (expand-ruleset ',(CAR E/D-LIST) world))
          (cdr e/d-list)
          t))))
  (defmacro e/d**
    (&rest theories)
    (declare (xargs :guard (true-list-listp theories)))
    (cond ((atom theories) nil) (t (e/d*-fn nil theories t))))
  (defmacro e/d*
    (&rest theories)
    (declare (xargs :guard (true-list-listp theories)))
    (cond ((atom theories) '(current-theory :here))
      (t (e/d*-fn '(current-theory :here) theories t)))))