normalize the result of case_rwlist and cache it. #1662
Conversation
|
This significantly speedups my benchmark of word_to_stackProof in CakeML and is pretty much the main calls of SPEC_ALL in that file. |
|
Could you be more precise about what "significantly speedup" means quantitatively? |
|
Seems very plausible; I'm not sure I realised that this is what EVERY_CASE_TAC was doing (because “no-one should ever use that tactic” :) ; maybe with this change it won't be so egregious. (Exact numbers would be good.) |
src/basicProof/BasicProvers.sml
Outdated
| tot TypeBasePure.distinct_of tyi, | ||
| tot TypeBasePure.one_one_of tyi] | ||
|
|
||
| fun decompose (th::res) = |
There was a problem hiding this comment.
This code is simple enough that it's not a huge deal, but I was wondering why not just call Cond_rewr.mk_cond_rewrs or similar?
There was a problem hiding this comment.
It's being called by the REWRITE_TAC and the simplifier which have different behavior and only the SPEC_ALL call is expensive.
There was a problem hiding this comment.
Wait I just realized BODY_CONJUNCTS does what I want will change to using it
edit: done
src/basicProof/BasicProvers.sml
Outdated
| fun case_rwlist () = | ||
| itlist (fn tyi => fn rws => case_rws tyi @ rws) | ||
| (TypeBase.elts()) []; | ||
| case (!cache) of |
There was a problem hiding this comment.
You should use the TypeBase's listener API (register_update_fn) so that you can see the new types arrive and add them to your cache rather than having to rebuild it every time. The stateful simpset does the same. (The ability to actually change the tyinfo value before it gets incorporated is interesting; but I'm not sure it's used, and if we dropped it, we could make the TypeBase code just use Listener.)
There was a problem hiding this comment.
Is there a way to listen for when a type is deleted?
There was a problem hiding this comment.
If we made this an actual listener, the listener would be on a change type that included addition and deletion of info values. I don’t think there are many deletions in non-interactive uses, and having out-dated stuff in a cache isn’t likely to be much of a problem.
ordinarymath
force-pushed
the
cache_case_rwlist
branch
from
2097b77 to
8e87752
Compare
ordinarymath
force-pushed
the
cache_case_rwlist
branch
from
8e87752 to
07545ad
Compare
A huge amount of time is spent calling SPEC_ALL when adding the results of case_rwlist to the rewrites or simpset. By caching this expensive operation is now only done whenever the TypeBase is updated.
ordinarymath
force-pushed
the
cache_case_rwlist
branch
from
07545ad to
0cf9bdb
Compare
|
@mn200 another ping on this? |
3 participants
A huge amount of time is spent calling SPEC_ALL when adding the results of case_rwlist to the rewrites or simpset. By caching this expensive operation is now only done whenever the TypeBase is updated.