Elaboration.Unification: clean support for valueMatch on functions

[GoogleCodeExporter]

This is related to the recbug.pig test.

We have committed a patch "Fix(?) to recbug" that alleviates the issue but is 
clearly motivated by pure hatred. A clean fix still needs to be provided.

The situation is as follow: we are seeking for a label <foo (f x) : ...> while 
we have a function (s : S) -> <foo (f s) : ...>  in the context. The seekLabel 
machinery will introduce s as a hoping hole and try to |matchValue| |f s| and 
|f x|. However, the current unifier is too weak to unify this thing. 

So, we have abused several functions to do our job, and just our job. Miller 
and Adam surely have something better to say.

Original issue reported on code.google.com by pedag...@gmail.com on 1 Sep 2010 at 3:24

[GoogleCodeExporter]

Perhaps recursive call search should not use the same unification machinery as 
normal equations. Rather, |seekIn| could accumulate a list of fresh references, 
then the matching code could solve for those references (only). That would 
ensure we match all user-visible programming problem arguments as expected. We 
could potentially hope for missing references, in case the recursive call 
justification required some extra arguments (e.g. proofs) not present in the 
programming problem.

Original comment by adamgundry on 3 Sep 2010 at 3:43

[GoogleCodeExporter]

I have pushed a quick hack to higherMatch that ensures the values in the 
substitution it generates are fully applied. My plan is to review and refactor 
the recursive call search and matching code, so this is more principled and 
robust.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100906114428-e29d1-9
a6aa6dd0283cad36727f5a8f681c986506355fc.gz

Original comment by adamgundry on 6 Sep 2010 at 11:58

• Changed state: Accepted

[GoogleCodeExporter]

My new version has now been committed, and seems to handle all the test cases. 
There are a few outstanding issues which I need to address, but they are 
documented in the source and should not arise in normal use, so I am closing 
this bug. Feel free to open another if matching fails for your favourite 
recursive call.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100907122415-e29d1-d
d02f291c265fb47af7ec8759bfa04a470e051bc.gz

Original comment by adamgundry on 8 Sep 2010 at 8:12

• Changed state: Fixed