]> matita.cs.unibo.it Git - helm.git/commit
1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 12 Oct 2009 17:38:50 +0000 (17:38 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 12 Oct 2009 17:38:50 +0000 (17:38 +0000)
commit30f0cf11c54154787e259c01bb99595c4a92ab1c
tree74e2c596070a15b13eb743ad36991e939e536856
parent34c2ba63c8eb5fccfd9a1fb8ac1df5895c8b58b3
1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
   but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was
   not. As a result, a tempeted self assegniment yielded strange errors.
   Fixed by more aggressively unwinding the subst during fo_unif.
2) Major re-organization of the code to gain some speed in Oliboni's stuff.
   The idea is that of introducing a new internal exception KeepReducing
   used to signal that, after a fo_unif, it still makes sense to fall back
   to machines. Only if it does not it makes sense to distinguish between
   Failures and Uncertain and the latter test can now be implemented more
   lazily w.r.t. the old version that used to call metas_of_term on the
   unwinded machines (that are potentially HUGE).
   With this modification, all Oliboni's tests terminate, even if they are
   still very slow compared to the height=0 strategy. Moreover, the tests
   show that unification on closed terms can still be 4x slower than conversion,
   which is partially unexpected.
helm/software/components/ng_refiner/nCicUnification.ml