unification of (lam t1) (lam t2) moves t1 and t2 at same level + test

[FissoreD]

Attempt to solve #256:

When unifying two terms t1 and t2 starting with the lam constructor. Let d1 (resp d2) the level of t1 (resp t2). Before unifying the body of t1 and t2, we want to put the two terms at the same level.

[!WARNING]
To make two terms at the same level, a call to move is done. This means that if the term is not in the PF the error Non deterministic pruning, delay to be implemented is raised

For example, the term pi dummy\ clause2 (x\y\x,x) raise the error when trying to unify with the rule clause2 (x\y\X x, F y (X x)) :- F = a\b\b. This is due to the call to move is done before the assignement of X to the identity function. This means that no deref can be done on X and F y (X x) which is not in $\mathcal{L}_\lambda$

[gares]

It may fix the problem but it is not a desired fix. The unification works on terms that are not at the same level exactly to avoid the costly move... So IMO the bug occurs after, when the terms under the lambda are unified. Sorry but I don't have the time to look into it right now, but you can work with this patch temporarily

[FissoreD]

No problem, we will discuss about it next month. Have a nice holiday ! :wave:

[gares]

Closing this one since the bug is fixed