Merge pull request #259 from LPCIC/fix-256

unification: fix simplification step

src/runtime.ml

@@ -758,8 +758,10 @@ let occurr_check r1 r2 =
         if !!r1 != C.dummy || r1 == r2 then raise RestrictionFailure
 
 let rec make_lambdas destdepth args =
- if args = 0 then let x = UVar(oref C.dummy,destdepth,0) in x,x
- else let x,y = make_lambdas (destdepth+1) (args-1) in Lam x, y
+ if args <= 0 then
+    UVar(oref C.dummy,destdepth,0)
+ else
+   Lam (make_lambdas (destdepth+1) (args-1))
 
 let rec mknLam n x = if n = 0 then x else Lam (mknLam (n-1) x)
 
@@ -809,6 +811,12 @@ let expand_appuv ~depth r ~lvl ~args =
           (uppterm lvl [] ~argsdepth:0 empty_env) t) ass];
   rc
 
+let deoptimize_uv_w_args = function
+  | UVar(r,lvl,args) when args > 0 ->
+      AppUVar(r,lvl,C.mkinterval lvl args 0)
+  | x -> x
+
+
 (* move performs at once:
    1) refreshing of the arguments into variables (heapifycation)
    2) restriction/occur-check
@@ -1633,7 +1641,7 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
    [%trace "unif" ~rid ("@[<hov 2>^%d:%a@ =%d%s= ^%d:%a@]%!"
        adepth (ppterm (adepth+depth) [] ~argsdepth empty_env) a
        depth (if matching then "m" else "")
-       bdepth (ppterm (bdepth+depth) [] ~argsdepth e) b)
+       bdepth (ppterm (bdepth+depth) [] ~argsdepth:bdepth e) b)
    begin
    let delta = adepth - bdepth in
 
@@ -1783,32 +1791,35 @@ let rec unif argsdepth matching depth adepth a bdepth b e =
           unif argsdepth matching depth adepth a adepth b e
        | RestrictionFailure -> false
        end
-   (* simplify *)
-   (* TODO: unif->deref_uv case. Rewrite the code to do the job directly? *)
-   | _, Arg (i,args) ->
-      let v = fst (make_lambdas adepth args) in
-      [%spy "user:assign" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
+
+   (* XXX simplify either generated UVar(_,_,0) or AppUVar XXX *)
+  | _, Arg (i,args) ->
+      let v = make_lambdas adepth (args - depth) in
+      [%spy "user:assign:simplify:stack:arg" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
         (uppterm depth [] ~argsdepth e) (Arg(i,0))
         (uppterm depth [] ~argsdepth e) v) ()];
       e.(i) <- v;
-      [%spy "user:assign" ~rid (fun fmt () -> ppterm depth [] ~argsdepth empty_env fmt (e.(i))) ()];
+      let bdepth = adepth in (* like in deref for arg *)
+      let b = deoptimize_uv_w_args @@ deref_uv ~from:argsdepth ~to_:(bdepth+depth) args v in
       unif argsdepth matching depth adepth a bdepth b e
    | UVar(r1,_,a1), UVar (r2,_,a2) when uvar_isnt_a_blocker r1 && uvar_is_a_blocker r2 && a1 + a2 > 0 -> unif argsdepth matching depth bdepth b adepth a e (* TODO argsdepth *)
    | AppUVar(r1,_,_), UVar (r2,_,a2) when uvar_isnt_a_blocker r1 && uvar_is_a_blocker r2 && a2 > 0 -> unif argsdepth matching depth bdepth b adepth a e
 
    | _, UVar (r,origdepth,args) when args > 0 && match a with UVar(r1,_,_) | AppUVar(r1,_,_) -> r != r1 | _ -> true ->
-      let v = fst (make_lambdas origdepth args) in
-      [%spy "user:assign:simplify" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
+      let v = make_lambdas origdepth (args - depth) in
+      [%spy "user:assign:simplify:stack:uvar" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
         (uppterm depth [] ~argsdepth e) (UVar(r,origdepth,0))
         (uppterm depth [] ~argsdepth e) v) ()];
       r @:= v;
+      let b = deoptimize_uv_w_args @@ deref_uv ~from:origdepth ~to_:(bdepth+depth) args v in
       unif argsdepth matching depth adepth a bdepth b e
    | UVar (r,origdepth,args), _ when args > 0 && match b with UVar(r1,_,_) | AppUVar(r1,_,_) -> r != r1 | _ -> true ->
-      let v = fst (make_lambdas origdepth args) in
-      [%spy "user:assign:simplify" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
+      let v = make_lambdas origdepth (args - depth) in
+      [%spy "user:assign:simplify:heap" ~rid (fun fmt () -> Fmt.fprintf fmt "%a := %a"
          (uppterm depth [] ~argsdepth e) (UVar(r,origdepth,0))
          (uppterm depth [] ~argsdepth e) v) ()];
       r @:= v;
+      let a = deoptimize_uv_w_args @@ deref_uv ~from:origdepth ~to_:(adepth+depth) args v in
       unif argsdepth matching depth adepth a bdepth b e
 
    (* HO *)

tests/sources/bug-256.elpi

@@ -0,0 +1,18 @@
+pred u o:(int -> int).
+u (y\y).
+
+main :-
+  print "-----------",
+  t1,
+  print "-----------",
+  t2,
+  t3,
+  true.
+
+t1 :- pi x\ u (y\ X x y), std.assert! (X 1 2 = 2) "bug".
+
+t2 :-
+  (pi X\ p ( a\f (X a))) => pi x y\ p ( a\f (g x y a)). 
+
+t3 :-
+  (pi X\ q ( a\b\c\d\f (X a))) => pi x y\ q ( a\b\c\d\f (g x y a)). 

tests/sources/llam.elpi

@@ -1,3 +1,4 @@
+pred spy i:prop.
 spy X :-  counter "run" N, print N "test " X, 
   not(not(X)).
 
@@ -19,6 +20,8 @@ prune_arg (r F).
 prune_arg2 (r (x\F x)).
 prune_arg3 (r (x\y\F y x)).
 
+type whatever A.
+
 main :-
   test (eq\F\        pi x\ pi y\ eq (F y x) x)             (a\b\b),
   test (eq\F\   not (pi x\ pi y\ eq (F x) y))              whatever,
@@ -27,9 +30,9 @@ main :-
   test (eq\F\   not (pi x\ pi y\ sigma R\ R = x, eq (F R) y))              whatever,
   test (eq\F\        pi x\ pi y\ sigma R\ R = x, eq (F y x) (r (w\h w R))) (a\b\r (x\h x b)),
   spy (pi dummy\ clause (x\y\x)),
-  (pi dummy\ clause1 (x\y\F y x), F = a\b\b),
-  (pi dummy\ clause2 (x\y\x,x)),
-  (clause3 (x\y\G y x) => pi dummy\ clause3 (x\y\x)), (G = a\b\b),
+  spy (pi dummy\ clause1 (x\y\F y x), F = a\b\b),
+  spy (pi dummy\ clause2 (x\y\x , x)),
+  spy (clause3 (x\y\G y x) => pi dummy\ clause3 (x\y\x)), (G = a\b\b),
   test (eq\F\        sigma H\pi x\ pi y\ eq (F y) (r (H y x)), H x x = x, H x y = x)   (a\r a),
 
   % this is hard because F<H but is applied to y that H can see, so H is restricted to the

tests/sources/trace_w.json

@@ -410,7 +410,7 @@
 {"step" : 33,"kind" : ["Info"],"goal_id" : 61,"runtime_id" : 1,"name" : "user:rule:backchain:candidates","payload" : ["File \"tests/sources/trace-w/main.elpi\", line 122, column 0, character 3232:"]}
 {"step" : 33,"kind" : ["Info"],"goal_id" : 61,"runtime_id" : 1,"name" : "user:rule:backchain:try","payload" : ["File \"tests/sources/trace-w/main.elpi\", line 122, column 0, character 3232:","(bind [] _ A0 (mono A1)) :- (copy A0 A1)."]}
 {"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["A0 := uvar frozen--539 [] ==> uvar frozen--539 []"]}
-{"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign:simplify","payload" : ["X13 := c0 \\\nX15 c0"]}
+{"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign:simplify:heap","payload" : ["X13 := c0 \\\nX15 c0"]}
 {"step" : 33,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 1,"name" : "user:assign","payload" : ["X15^1 := mono X16^1"]}
 {"step" : 33,"kind" : ["Info"],"goal_id" : 61,"runtime_id" : 1,"name" : "user:subgoal","payload" : ["62"]}
 {"step" : 33,"kind" : ["Info"],"goal_id" : 62,"runtime_id" : 1,"name" : "user:newgoal","payload" : ["copy (uvar frozen--539 [] ==> uvar frozen--539 []) X16^1"]}

tests/suite/correctness_HO.ml

@@ -348,3 +348,10 @@ let () = declare "chr_with_hypotheses"
   ~typecheck:true
   ~expectation:Success
   ()
+
+let () = declare "bug-256"
+  ~source_elpi:"bug-256.elpi"
+  ~description:"move/unif"
+  ~typecheck:true
+  ~expectation:Success
+  ()