Is there a standard way to see the what phrase/3 translates?
No. The meaning of phrase/3 is defined, but the actual implementation behind is not accessible. There are several different ways, how phrase/3 can be defined. It could be as simple as in YAP:
phrase(P, S0, S) :-
call(P, S0, S).
Or it could use expand_term/2 (or something of that kind). That is:
phrase(P, S0, S) :-
expand_term(( pseudont --> P ), ( pseudont(CS0, CS) :- Goal) )),
S0 = CS0,
S = CS,
Goal.
It could execute the final unification after calling Goal:
phrase(P, S0, S) :-
expand_term(( pseudont --> P ), ( pseudont(CS0, CS) :- Goal) )),
S0 = CS0,
Goal,
S = CS.
And by that introduce the (implementation dependent) convention that the expanded predicates are always called with an uninstantiated and unaliased variable in the last argument which would permit tail-recursiveness in the presence of semicontext.
It is all up to the implementer.
Does this tell me how phrase/3 is used in my test/3?
No, there is no way telling.
But then, why do you ask? Or, to rephrase:
What effect could a differing but conforming implementation of phrase/3 have?
Resource consumption
This should be evident. Consider ?- phrase([],Xs). which does not create any term on the heap in YAP, but does so for the naive expand_term-expansion above. But then, resource consumption is out of scope of the current standards.
Variable ordering
Consider the body of a rule ..., phrase([], Xs, Xs), ... in YAP: Xs remains a local variable, whereas an expand_term-based phrase makes it global. In many implementations this would affect the relative order of variables. Now, the standard explicitly states in 7.2.1:
If X and Y are variables which are not identical then
X term_precedes Y shall be implementation dependent
except that during the creation of a sorted list (7.1.6.5,
8.10.3.1 j) the ordering shall remain constant.
So this is again not a problem, but still this might be annoying.
NSTO property
The Prolog standard (that is, part 1 ISO/IEC 13211-1) only defines execution if it is NSTO. That is, if all unifications happening during execution are NSTO — Not subject to occurs-check (see 7.3.3).
Now, consider your case: phrase(("a",!,"b"), Xs, Ys). At first sight, this is equivalent to phrase("ab", Xs, Ys). But now consider assuming set_prolog_flag(double_quotes,chars)
?- Xs = [c|_], Xs = Ys, phrase(("a",!,"b"), Xs, Ys).
This query should fail, no doubt. But is it NSTO? Naively, we could assume that this can be replaced by:
?- Xs = [c|_], Xs = Ys, Xs = [a,b|Ys].
Which is tantamount to:
?- Xs = [c|_], Xs = [a,b|Xs].
Clearly, Xs = [a,b|Xs] alone is STO (Subject to occurs check). But also both together are STO! To understand this, consider the Herbrand algorithm in 7.3.2. In essence, it non-deterministically rewrites the equations "in any order". Here is one such derivation:
Xs = [c|Zs], Xs = [a,b|Xs].
(7.3.2 f) Xs = [c|Zs], [c|Zs] = [a,b,c|Zs].
(7.3.2 d) Xs = [c|Zs], c = a, Zs = [b,c|Zs].
(7.3.2 g) failure (not unifiable, positive occurs-check)
Of course, this derivation is unusual. Usually, one would fail immediately in the presence of c = a, but the algorithm is non-deterministic in this respect. And a set of equations is NSTO only if all possible derivations do not lead to 7.3.2 g. To cite 7.3.3:
A set of equations (or two terms) is "not subject to
occurs-check" (NSTO) iff there exists no way to proceed
through the steps of the Herbrand Algorithm such that
7.3.2 g happens.
freeze/2 and when/2
These constructs might also be affected. While they are currently not covered by existing standard documents understanding potential impacts is still of relevance. Consider:
?- freeze(L, (X=1;X=2)), phrase(("a",!,"b"),L).
L = [a,b], X = 1.
B, SICStus, SWI, YAP all produce this one answer. So the cut is significant.
In any case, thanks for asking – I understood the NSTO issue only while answering your question! This clearly has some impact in how the DCG translation is formulated.
