[Cfp-interest] Berkeley feedback - substitution

[David Hough CFP]

Ian gives a good rundown on the costs of various ways of implementing
presubstitution on PowerPC.     There are minor variations on other
platforms but it still is quite involved.     Exactly how you'd want
a particular loop to be implemented depends on how much time the normal
case of the loop takes (compared to trap setup/teardown time) and how often
the exceptional case is expected to arise.     In realistic applications
the number of iterations of the loop isn't known at compile time.
Ideally one might want to have additional pragmas, or clauses in pragmas,
that indicate normal expected number of iterations and normal expected
incidence of exceptional cases.      But of course the programmer might not
know that, so the compiler has to guess.      However we can expect the
compiler to know whether setting up traps is an exceptionally bad idea
on this particular implementations, or checking flags is, or checking
operands and results is, and generate code accordingly.      That's
why I like the specification to application programmers to be in terms 
of exceptions rather than flags or traps.     Exceptions are portable,
but flags and traps performance characteristics are not.      He who is
so inclined can always optimize for a particular platform by
doing the platform-specific bit manipulations, but most
application programmers don't want to know any more about that than 
necessary.

Aside from that, I'm not sure automated theorem-proving systems can 
benefit from presubstitution declarations (with their implicit branch
on exception) vs. explicit tests and branches.     But somebody else more
knowledgeable should weigh in on that.