Closed gares closed 2 months ago
pred f o:(term -> term) o:term. f R (fun d\ R d). % BUGGY % f R N :- N = (fun d\ R d). % OK pred foo o:(term -> term) o:term. foo R N :- pi d\ f R N. main :- foo R N, print R, print N.
Trace:
$ elpi -test bug.elpi -trace-on -trace-at run 4 4 -no-tc Parsing time: 0.000 Compilation time: 0.001 run 4 {{{ rid:0 step:4 gid:9 user:curgoal = f f X0 X1 rid:0 step:4 gid:0 dev:get_clauses = f 1 rid:0 step:4 gid:9 user:rule = backchain rid:0 step:4 gid:9 user:rule:backchain:candidates = File "/home/tassi/LPCIC/coq-elpi/bug.elpi", line 3, column 0, character 33: }}} -> (0.000s) select 4 {{{ rid:0 step:4 gid:9 user:rule:backchain:try = File "/home/tassi/LPCIC/coq-elpi/bug.elpi", line 3, column 0, character 33: (f A0 (fun (c0 \ (A0 c0)))) :- . unif 5 {{{ ^1:.X0 =0= ^0:A0 hmove 8 {{{ from:1 to:1 X0 rid:0 step:4 gid:0 dev:move:out = .X0 }}} ok (0.000s) rid:0 step:4 gid:0 user:assign = A0 := X0 }}} ok (0.000s) rid:0 step:4 gid:0 dev:unif:out = true unif 6 {{{ ^1:.X1 =0= ^0:fun (c0 \ ≪.X0≫_1 c1) move 16 {{{ adepth:1 depth:0 from:0 to:0 x:fun (c0 \ ≪.X0≫_1 c1) move 17 {{{ adepth:1 depth:0 from:0 to:0 x:c0 \ ≪.X0≫_1 c1 move 18 {{{ adepth:1 depth:1 from:0 to:0 x:≪.X0≫_1 c1 deref_uv 6 {{{ from:1 to:1 .X0 @ 1 deref_uv 7 {{{ from:1 to:1 .X0 @ 0 hmove 9 {{{ from:1 to:1 X0 move 19 {{{ adepth:0 depth:0 from:1 to:1 x:.X0 }}} ok (0.000s) rid:0 step:4 gid:0 dev:move:out = .X0 }}} ok (0.000s) }}} ok (0.000s) }}} ok (0.000s) }}} ok (0.000s) }}} ok (0.000s) }}} ok (0.000s) rid:0 step:4 gid:0 dev:move:out = fun (c0 \ X0 c1) rid:0 step:4 gid:0 user:assign = X1 := fun c0 \ X0 c1 rid:0 step:4 gid:0 dev:trail:assign = true (Runtime.ConstraintStoreAndTrail.Assignement { Data.Term.contents = please extend this printer; uid_private = 2 }) }}} ok (0.000s) rid:0 step:4 gid:0 dev:unif:out = true rid:0 step:4 gid:9 user:rule:backchain = success }}} -> (0.000s) X0 fun c0 \ X0 c1
Trace: