Thanks. This is a bug. Pushed a fix. Your example is very complicated. This illustrates the issue:
v(f(X,X)).
?- v(_A).
_A = f(_A,_A).
The issues is triggered by two flags: toplevel_name_variables, which is by default true and causes the toplevel to name variables in the answer _A, _B, etc. rather than using _NNNN and toplevel_print_anon which is by default false (I set to true in my init.pl), which causes SWI-Prolog to not print the binding of variables that start with an underscore. If it prints _A, (default) it must check that the new variable is not already in use. That check was there, but broken.
I wonder whether we should enable hiding the bindings for “named anonymous” variables by default. I find it a very useful feature if I do not want some variable in a conjunction printed, typically because it is a huge term. So, you have q/1 that produces a long list and you only want the length. With toplevel_print_anon set to true, we can do
I suppose that’s likely to be a bug in the person’s code, so hiding that _X deserves to be a separate option if anything, with the default being to show them.
Not sure why you say that, residual goals can be part of a valid answer (and very common when using clpBNR real arithmetic). It’s also likely that using a top level named variable starting with _ is usually motivated by the objective of not having them included in the printed answer.
So my question was whether the same convention for printing bound variables at the top level should be also be applied to unbound variables with attributes. I think it would be a nice feature addition.
I don’t know. I have the impression there are at least two types of attributed variables. Those that are intended to lead to some delayed execution to achieve a full answer (coroutining) and those that represent some valid answer in themselves (like an interval in your case).
Some people from the constraint world have advocated to enable the Prolog flag toplevel_residue_vars by default. This causes constraints to be printed even if they are not related to the answer. That is (I think) related to the first type: if we add a constraint that must be satisfied eventually to some variable and the variable is not related to the answer and the constraint was never resolved, the user should be made aware of this. I disagree making this the default because it requires wrapping toplevel goals in call_residue_vars/2, which causes significant overhead and disables GC for attributed variables.
This seems related. Possibly we should allow some annotation on the attribute? I do realise that the above distinction is not crystal clear though
One thing you can do is to define attribute_goals//1 to return no goals for the second type of attributes and define attr_portray_hook/2 to print the attributed variable.
I guess it depends on what you mean by “full answer”. In my interpretation an unbound variable in an answer means the proof is valid for any possible binding to that variable. In the freeze example I concocted, the interpretation would be any value which is a number. In this model all constraints are related to the answer, as are all unbound variables.
The top level makes choices as to what variables in the answer are output, conditional on the variable name. I was just suggesting the same conventions might be applied to attributed variables.
As @herme contributed, Ciao uses the same convention. I did a few more tests. It appears Ciao, SICStus, YAP and XSB all hide _A, at least by default. Ciao, SICStus and YAP print constraints on such variables. XSB hides them.
And Ciao has a little bug that is the opposite of the bug that initiated this discussion:
Ciao: Note hat the constraint is reported on an invented variable _B rather than on _A. There is no problem when using a normal variable.