issue with portray_clause/2 to output a copied term

[josd]

The issue can be reproduced with:

cd /tmp
git clone https://github.com/eyereasoner/eye2
cd eye2
git checkout tags/v1.2.11
tpl -g main eye3.pl etc/sdcoding.pl

which is giving

:- op(1150,xfx,=>).

'urn:example:sdcoding'(1,1)=>true.
'urn:example:sdcoding'(3,3)=>true.
'urn:example:sdcoding'(0,0)=>true.
'urn:example:sdcoding'(2,2)=>true.

%
% Explain the reasoning
%

ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(0,1),'urn:example:sdconot'(0,1)).
ether(('urn:example:sdc'('urn:example:sdconot'(0,3),A)=>'urn:example:sdconot'('urn:example:sdconot'(0,3),A)),'urn:example:sdc'(0,3),'urn:example:sdconot'(0,3)).
ether(('urn:example:sdc'(true,false)=>'urn:example:sdconot'(true,false)),'urn:example:sdc'(1,0),'urn:example:sdconot'(1,0)).
ether(('urn:example:sdc'('urn:example:sdconot'(1,1),A)=>'urn:example:sdconot'('urn:example:sdconot'(1,1),A)),'urn:example:sdc'(1,1),'urn:example:sdconot'(1,1)).
ether(('urn:example:sdc'('urn:example:sdconot'(1,2),A)=>'urn:example:sdconot'('urn:example:sdconot'(1,2),A)),'urn:example:sdc'(1,2),'urn:example:sdconot'(1,2)).
ether(('urn:example:sdc'('urn:example:sdconot'(2,1),A)=>'urn:example:sdconot'('urn:example:sdconot'(2,1),A)),'urn:example:sdc'(2,1),'urn:example:sdconot'(2,1)).
ether(('urn:example:sdc'('urn:example:sdconot'(2,3),A)=>'urn:example:sdconot'('urn:example:sdconot'(2,3),A)),'urn:example:sdc'(2,3),'urn:example:sdconot'(2,3)).
ether(('urn:example:sdc'(false,true)=>'urn:example:sdconot'(false,true)),'urn:example:sdc'(3,1),'urn:example:sdconot'(3,1)).
ether(('urn:example:sdc'(false,true)=>'urn:example:sdconot'(false,true)),'urn:example:sdc'(3,3),'urn:example:sdconot'(3,3)).
ether(('urn:example:sdc'(false,true)=>'urn:example:sdconot'(false,true)),'urn:example:sdc'(3,0),'urn:example:sdconot'(3,0)).
ether(('urn:example:sdc'(false,true)=>'urn:example:sdconot'(false,true)),'urn:example:sdc'(3,2),'urn:example:sdconot'(3,2)).
ether(('urn:example:sdc'(true,true)=>'urn:example:sdconot'(true,true)),'urn:example:sdc'(0,0),'urn:example:sdconot'(0,0)).
ether(('urn:example:sdc'(false,true)=>'urn:example:sdconot'(false,true)),'urn:example:sdc'(2,0),'urn:example:sdconot'(2,0)).
ether(('urn:example:sdc'('urn:example:sdconot'(2,2),A)=>'urn:example:sdconot'('urn:example:sdconot'(2,2),A)),'urn:example:sdc'(2,2),'urn:example:sdconot'(2,2)).

but we expect it to give

:- op(1150,xfx,=>).

'urn:example:sdcoding'(1,1)=>true.
'urn:example:sdcoding'(3,3)=>true.
'urn:example:sdcoding'(0,0)=>true.
'urn:example:sdcoding'(2,2)=>true.

%
% Explain the reasoning
%

ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(0,1),'urn:example:sdconot'(0,1)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(0,3),'urn:example:sdconot'(0,3)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(1,0),'urn:example:sdconot'(1,0)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(1,1),'urn:example:sdconot'(1,1)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(1,2),'urn:example:sdconot'(1,2)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(2,1),'urn:example:sdconot'(2,1)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(2,3),'urn:example:sdconot'(2,3)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(3,1),'urn:example:sdconot'(3,1)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(3,3),'urn:example:sdconot'(3,3)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(3,0),'urn:example:sdconot'(3,0)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(3,2),'urn:example:sdconot'(3,2)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(0,0),'urn:example:sdconot'(0,0)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(2,0),'urn:example:sdconot'(2,0)).
ether(('urn:example:sdc'(A,B)=>'urn:example:sdconot'(A,B)),'urn:example:sdc'(2,2),'urn:example:sdconot'(2,2)).

So somehow the copied Rule in https://github.com/eyereasoner/eye3/blob/21f142195db9b5967d7710514c4d7aa2c9180636/eye3.pl#L65 seems to get corrupted.

[josd]

It seems related with #634 where we also used library(format).
It all seems to be fine when we use write & co.

[infradig]

Scryer doesn't do portray_clause/2 as it's non-standard so maybe best avoided.

[infradig]

Sorry, take that back. I though you meant format ~p to call a user-defined portray.

[infradig]

I've never used portray_clause/2 and am not at all familiar with it.

[josd]

The issue remains after replacing portray_clause(X) with format("~q.~n",[X].
Also valgrind is happy ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)

[josd]

It works fine when using copy_term/3 instead of copy_term/2 eyereasoner/eye2@c47dc10
How is that explainable?

[infradig]

It works fine when using copy_term/3 instead of copy_term/2 eyereasoner/eye3@c47dc10 How is that explainable?

Since you are not using attributes (I assume) it is indeed odd. It should work using copy_term_nat/2 instead of copy_term/2 as well.

[josd]

I also tried with copy_term_nat/2 and it also gave the unexpected unifications in the copied term.

[josd]

and yes, we are not using attributes, the 3rd arg of copy_term((Prem => Conc),Rule,X) is indeed X = [].

[josd]

and earlier versions like https://github.com/eyereasoner/eye2/blob/2dc50874fedc39c3cf2e200484e72b6432ccdaa1/eye3.pl were using copy_term/2 and worked fine🤷

[infradig]

Sorry, problem not fixed it seems.

[josd]

Indeed, still in https://github.com/eyereasoner/eye2/blob/67f87bdb3278d767ae06b7399de736b0f74b3183/etc/output/sdcoding.pl

[josd]

Indeed, still in https://github.com/eyereasoner/eye2/blob/67f87bdb3278d767ae06b7399de736b0f74b3183/etc/output/sdcoding.pl

and still working fine when using copy_term/3 instead of copy_term/2 in https://github.com/eyereasoner/eye2-trealla/blob/68a8219f5a3a34db530527135a94c393e6ca8234/eye2-trealla.pl#L61