Add defined for formulas

[susuhahnml]

If you add a show statement for a formula that is not used in the input you get

:7:29-41: info: atom does not occur in any rule head:
__next(B,A)

[susuhahnml]

This is also an issue with the syntactic sugar, this transformed program does not have the externals for the show statements

light(l1).
red(L) :- not green(L), light(L).
__next(push(l1)) :- __initial.

__next(__eventually(green(L))):- push(L).

:- not __eventually(__final), __initial.

_show_atom(__final()) :- __final().
_show_atom(__not(A)) :- __not(A).
_show_atom(__next(A)) :- __next(A).

#external push(l1).
#external __initial.
#external __eventually(__final).
#external __initial.
#external green(L): push(L).

[namcsi]

Hi!

I do not immediately understand how the first and second comment is related, some detail on the first issue would be helpful for me.

The second issue is quite tricky.
For showing of metasp expression signatures like #show &final/0. this can easily be fixed by also generating a #external final. statement when rewriting the shows.

However it gets somewhat tricky when we are showing metasp expression signatures of non-zero arity - what even is the intended meaning of #show &next/1? I am not sure if we hammered this out in detail, but maybe I just forget.

Is it supposed to mean that I would like to show &next(A) for any atom A for which &next(A) holds?
We can't write a rule which will generate _show_atom(next(A)) for all such atoms A during grounding, as the condition "for which &next(A) holds" isn't something we can check during grounding, for this we need the semantics meta-encoding which is only applied later.

This is even more clear for the #show &not/1 example. Is this supposed to show all atoms which do not hold? I think it is unfeasible to rewrite this to a rule since any rule that would generate such _show_atom(not(A)) atoms would have to be unsafe.

[namcsi]

So I think all in all we might have to rethink how we rewrite show statements for metasp signatures - the current approach seems to be flawed to me.