Date: Mon, 21 Aug 2006 14:57:55 -0500
From: Sol Swords

Hi everyone,

J has volunteered to talk this Wednesday about the new hints he's 
working on.  ACES 3.116, 4:00 PM as always.  See you there.

 - Sol

Disjunctive Hints and Custom Keyword Hints

J Moore

I will present my summer's work on adding two new kinds of hints to
ACL2.  The first allows you to give "disjunctive hints" like:

 ("Subgoal 3" :OR ((:in-theory foo :do-not '(generalize))
                   (:in-theory bar :use lemma23)))

When you give a disjunction of n hints ACL2 splits the goal
into n copies and applies a hint to each copy.  Each such
branch results in the waterfall pushing a set of subgoals.
When the last branch has been processed the waterfall
gathers up all the alternative sets of subgoals and choose
one set to pursue by subsequent inductions.

The second new kind of hint is called a "custom keyword hint".
A custom keyword hint is to hints what macros are to functions.
If :my-use were introduced as a custom keyword hint you could
write

 ("Subgoal 3" :my-use foo :do-not '(generalize))

and a function associated with my-use will run and produce
the real hint.  Like computed hints, custom keyword hints
are not necessarily evaluated until the goal in question
arises, so you can compute goal-sensitive hints.  While
custom keyword hints add no power to the system -- computed
hints can mimic them -- they are much more convenient and
attractive.