The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

In a single autorewrite db, if there are two or more rewrite hints that 
can be applied to a particular term, does autorewrite do any kind of 
ordering to decide which one to use (first)?  Or, does it base the 
selection on the order in which the hints were registered in the db?  
Or, is it just random?

I am writing a system of rewrite rules, and some of them have specific 
applicability while others are default rules - and I would prefer the 
specific rules to fire if possible before the defaults (just for 
efficiency reasons - it should be a confluent system regardless).  For 
instance, a specific rule that rewrites Foo(a::as) to Bar and a default 
that rewrites Foo(l) to Baz, where l is any list.  I could put them into 
separate autorewrite dbs and chain them with autorewrite with DB1 DB2 
... DBN, but then it looks like I would also need to wrap the whole 
thing in a repeat/progress loop, like so:

  repeat progress (autorewrite with DB1 DB2 ... DBN)

at least if I am understanding the description in refman section 8.8.4.  
Or, does autorewrite automatically loop back to try DB1 itself when it 
has exhausted DBN and the subgoal has progressed?

-- Jonathan