[Matita] Hints and KAM

[Enrico Tassi]

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
-- 
Enrico Tassi
-------------- next part --------------
A non-text attachment was scrubbed...
Name: a.diff
Type: text/x-diff
Size: 3556 bytes
Desc: not available
URL: <http://www.cs.unibo.it/pipermail/matita/attachments/20100923/13047fe7/attachment.diff>