On Tue, 28 May 2013, Makarius wrote:
* No change to unify.ML (and especially pattern.ML, which was not really
covered so far). My 3b9c31867707 is backed-out.
* Instead Thm.bicompose_aux in the non-lifted case (i.e. the "compose"
variants) ensures that the types of all Vars are unified
beforehand. So mentioning some ?x::?'a here and some ?x::nat=>bool
there means they become both ?x::nat=>bool before entering
Unify.unifiers (and Pattern.unify as well).
Thus we acknowledge the observation that the old code from 25 years ago
does not work with Vars of different type: Stefan's check from 2005
raises suitable exceptions, and the above pre-stage avoids that this
happens.
I've done this now in c4264f71dc3b .. 568b2cd65d50. The main thing is
0fa3b456a267 to "unify types of schematic variables in non-lifted case".
This was rather trivial, but there were some surprises nonetheless: Metis
proof reconstruction seems to require the non-unification of types of
Vars, despite having a separate workaround for exactly that problem
(see resolve_inc_tyvars in 568b2cd65d50).
Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at
the very end, due to divergence of types of certain Vars, types that
cannot be unified. This is very odd, but should not be a problem at the
moment: Metis should work as before.
If any of the experts on Metis proof reconstruction want to clean that up:
Thm.bicompose {incremented = false, ...} means types get unified, while
{incremented = true, ...} means there is no need for it since variables
have been incremented as for resolution. If it works one day without the
extra toggle, we can simplify the low-level Thm.bicompose once again. (And
all these "compose" variants are definitely outside normal user space.)
Anyway, apart from having seen a lot of boundary cases of the unification
code -- things we've seen more often in distant past -- the conclusion is
inconclusive. The system cannot be changed substantially at its very
bottom, but we knew that already.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
