[Matita] Hints and KAM
tassi at cs.unibo.it
Thu Sep 23 15:37:40 CEST 2010
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example
Hint: And A B === fun_of_morph And_morphism A B
If the problem
And A B =?= fun_of_morph ? A B
is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve
And =?= fun_of_morph ?
While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.
Patch attached (cumulated with the previous one). I'm asking for
comments, and I'm waiting for an ack before committing these patches,
since I don't want to (potentially) break some CerCo code.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 3556 bytes
Desc: not available
More information about the Matita