unification: fix simplification step

[gares]

The simplification step turns X c0 c1 (that is UVar(r,0,2)) into Y^2 via X := a\b\Y^2. In #256 the query pi x\ u (y\ X x y) goes against u (x\x). The simplification step was eating both arguments generating X := a\ b\ Y^1 a. Now it instead generates X := a\ Y^1, so that we have u (y\ Y^1 y) = u (y\y) so Y := x\x and hence X := a\b\b that is correct.

The old code was confusing locally bound variables and pi generated ones in the simplification step that seems wrong. By doing so, the old code was always eating all arguments, the 2 in UVar(r,0,2), and the rest of the unification code was assuming that, after the simplification step, the term was either UVar(_,_,0) or AppUVar. The current patch restores that "a posteriori", but we should pre compute it or fix make_lambdas.

deref_uv was also doing some confusion in the (back then untested) case in which and UVar is simplified without eating all arguments, fixed in #260.

In short the old code was trying to keep into the fast fragment terms that don't belong. The new code calls full pattern fragment unification in a few more cases. Perf wise I see no visible effect.

[FissoreD]

I do not fully understand all the code, but seems to work :+1: Just for curiosity, I did the following patch on the master for the same issue

~/.../github/ELPI_DEV/elpi git [elpi ⎇  remotes/enrico/master] > git diff
diff --git a/src/runtime.ml b/src/runtime.ml
index f1e45a9f..a700d2d3 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -1767,7 +1767,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
              move ~avoid:r ~argsdepth ~from:bdepth ~to_:origdepth e b
            else
              (* First step: we lift the r.h.s. to the l.h.s. level *)
-             let b = move ~avoid:r ~argsdepth ~from:(bdepth+depth) ~to_:(adepth+depth) e b in
+             let b = move ~avoid:r ~argsdepth ~from:bdepth ~to_:adepth e b in
              (* Second step: we restrict the r.h.s. *)
              hmove ~from:(adepth+depth) ~to_:origdepth b in
          [%spy "user:assign" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
~/.../github/ELPI_DEV/elpi git [elpi ⎇  remotes/enrico/master] > 

My idea was to move the term from bdepth to adepth instead of depth+bdepth (resp. depth+adepth) this way the move does not skip the local names quantified from bdepth to bdepth+depth while doing the lifting of the rhs. It seems to me that, when unif is called, bdepth allows to partition free vars from local one in rhs, i.e. bdepth is the number of free variables. The move should lift only the local vars with delta = adepth - bdepth (the delta computed in the master is (adepth + depth) - (bdepth + adepth) giving the same result as adepth - bdepth) This should justify the call to move without the +depth, i.e. I only move the local vars, am I right?

PS: I do not have tests for the AppUvar case :thinking:

[gares]

Hum, I think I need to see a trace for your patch, but also think more about this PR. Apparently it breaks a client so the tests are not covering enough code paths and I broke some.

[gares]

I've clean up a little the code, hopefully it works also for you. Please give it a try. We can look at your patch up there next time we meet.

[gares]

relevant, buggy trace

unif 6 {{{ ^1:c1 \ .X0 c0 c1 =0= ^0:c0 \ c0 
unif 7 {{{ ^1:.X0 c0 c1 =1= ^0:c0 

  rid:0 step:5 gid:0 user:assign:simplify = X0 := c1 \ c2 \ X1^1 c1 

unif 8 {{{ ^1:.<c0 \ c1 \ .X1^2>_0 c0 c1 =1= ^0:c0 

deref_uv 4 {{{ from:0 to:2 c0 \c1 \.X1^2 @ 2 
deref_uv 5 {{{ from:2 to:2 .X1^2 @ 0 

unif 9 {{{ ^1:.X1^2 =1= ^0:c0 

move 20 {{{ adepth:1 depth:0 from:1 to:2 x:c0 

  rid:0 step:5 gid:0 user:assign = X1^2 := c0 

new trace

unif 6 {{{ ^1:c1 \ .X0 c0 c1 =0= ^0:c0 \ c0 
unif 7 {{{ ^1:.X0 c0 c1 =1= ^0:c0 

  rid:0 step:5 gid:0 user:assign:simplify:heap = X0 := c1 \  X1^1 

deref_uv 4 {{{ from:0 to:2 c0 \   .X1^1 @ 2 
deref_uv 5 {{{ from:1 to:2 .X1^1 @ 0 

move 20 {{{ adepth:0 depth:0 from:1 to:2 x:.X1^1 

unif 8 {{{ ^1:X1^1 c1 =1= ^0:c0 

  rid:0 step:5 gid:0 user:assign:HO = X1^1 := c1 \ c1 

[FissoreD]

I've clean up a little the code, hopefully it works also for you. Please give it a try. We can look at your patch up there next time we meet.

Just tested and it works!

[gares]

great, releasing