cex: unifying counterexamples that are not unified

[Akim Demaille]

Hi Vincent,

There is something not quite right in the current implementation.  On the 
following grammar, taken from the test suite:

$ cat bar.y
%left b
%right c
%%
S: B C | C B;
A: B  | C  | %empty;
B: A b A;
C: A c A;

bison thinks it found two unifying examples, but the derivations actually yield 
two different sentential forms:

$ bison bar.y -Wcex
bar.y: avertissement: 4 conflits par réduction/réduction [-Wconflicts-rr]
Reduce/reduce conflict on tokens b, c:
  Example              B • b A A c A
  First derivation     S ::=[ B ::=[ A ::=[ B • ] b A ] C ::=[ A c A ] ]
  Example              B • b A c A
  Second derivation    S ::=[ B C ::=[ A ::=[ B ::=[ A ::=[ • ] b A ] ] c A ] ]

Reduce/reduce conflict on tokens b, c:
  Example              C • c A A b A
  First derivation     S ::=[ C ::=[ A ::=[ C • ] c A ] B ::=[ A b A ] ]
  Example              C • c A b A
  Second derivation    S ::=[ C B ::=[ A ::=[ C ::=[ A ::=[ • ] c A ] ] b A ] ]

The derivations are difficult to read.  They look as follows (hoping nothing 
will wreck the indentation):

> S
> |
> B       C
> |       |
> A b A   A c A
> |
> B •



> S
> |
> B  C
>    |
>    A c A
>    |
>    B
>    |
>    A b A
>    |
>    •
> 



The code appears to believe the example is unifying because both derivations 
share the same prefix up to the dot, and both comply with 
parse_state_derivation_completed, whose meaning is unclear to me (could you 
please add comments to these routines?).

But here it seems insufficient to dub this as unifying.

Cheers!