[Matita] Hints and KAM

[Andrea Asperti]

Enrico, sembra che tu stia dialogando con qualcuno, ma io ricevo solo le
tue di email.
-- Grazie.


Enrico Tassi wrote:
> 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.
>
> Cheers
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> Matita mailing list
> Matita at cs.unibo.it
> http://www.cs.unibo.it/cgi-bin/mailman/listinfo/matita