cex: color the counterexamples

Use colors to show the counterexamples and the derivations in color,
to highlight their structure.  Align the outputs, and add i18n
support. Reduce width by using a one-space separator instead of
two-space.

From

    Example  A  •  B  C
    First  derivation  s ::=[ a ::=[ A  • ]  x ::=[ B  C ] ]
    Second derivation  s ::=[ y ::=[ A  •  B ]  c ::=[ C ] ]

to

    Example              A • B C
    First derivation     s ::=[ a ::=[ A • ] x ::=[ B C ] ]
    Example              A • B C
    Second derivation    s ::=[ y ::=[ A • B ] c ::=[ C ] ]

with colors.

* data/bison-default.css (cex-dot, cex-0, cex-1, cex-2, cex-3, cex-4)
(cex-5, cex-6, cex-7, cex-step, cex-leaf): New.
* src/derivation.c (derivation_print_styled_impl): New.
(derivation_print, derivation_print_leaves): Use it.
* src/counterexample.c: Reformat the output.
* tests/counterexample.at: Adjust.
This commit is contained in:
Akim Demaille
2020-05-23 19:13:01 +02:00
parent 296e2f90ab
commit ae5edcc23b
5 changed files with 197 additions and 147 deletions

View File

@@ -30,5 +30,28 @@
/* "Sections" in traces (--trace). */
.trace0 { color: green; }
/* Syntax error messages. */
.expected { color: green; }
.unexpected { color: red; }
/* Counterexamples. */
/* Cex: point in rule. */
.cex-dot { color: red; }
/* Cex: coloring various rules. */
.cex-0 { color: yellow; }
.cex-1 { color: green; }
.cex-2 { color: blue; }
.cex-3 { color: cobalt; }
.cex-4 { color: violet; }
.cex-5 { color: orange; }
.cex-6 { color: brown; }
.cex-7 { color: mauve; }
/* Cex: derivation rewriting steps. */
.cex-step { font-style: italic; }
/* Cex: leaves of a derivation. */
.cex-leaf { font-weight: 600; }

View File

@@ -103,21 +103,18 @@ static void
print_counterexample (counterexample *cex)
{
FILE *out = stderr;
if (cex->unifying)
fprintf (out, "Example ");
else
fprintf (out, "First Example ");
fprintf (out, "%-20s ", cex->unifying ? _("Example") : _("First example"));
derivation_print_leaves (cex->d1, out);
fprintf (out, "\nFirst derivation ");
fprintf (out, "%-20s ", _("First derivation"));
derivation_print (cex->d1, out);
if (!cex->unifying)
{
fprintf (out, "\nSecond Example ");
fprintf (out, "%-20s ", cex->unifying ? _("Example") : _("Second example"));
derivation_print_leaves (cex->d2, out);
}
fprintf (out, "\nSecond derivation ");
fprintf (out, "%-20s ", _("Second derivation"));
derivation_print (cex->d2, out);
fputs ("\n\n", out);
fputc ('\n', out);
}
/*

View File

@@ -18,11 +18,13 @@
along with this program. If not, see <http://www.gnu.org/licenses/>. */
#include <config.h>
#include "derivation.h"
#include <gl_linked_list.h>
#include "system.h"
#include "derivation.h"
#include "complain.h"
struct derivation
{
@@ -124,49 +126,26 @@ derivation_size (const derivation *deriv)
return size;
}
// these are used rarely enough that I don't think they should be interned.
void
derivation_print (const derivation *deriv, FILE *f)
/* Print DERIV, colored according to COUNTER. */
static void
derivation_print_impl (const derivation *deriv, FILE *f,
bool leaves_only,
int *counter)
{
if (deriv == &d_dot)
if (deriv->children)
{
fputs ("", f);
return;
}
symbol *sym = symbols[deriv->sym];
if (!deriv->children)
{
fprintf (f, " %s", sym->tag);
return;
}
const symbol *sym = symbols[deriv->sym];
char style[20];
snprintf (style, 20, "cex-%d", *counter);
++*counter;
begin_use_class (style, f);
if (!leaves_only)
{
begin_use_class ("cex-step", f);
fprintf (f, "%s ::=[ ", sym->tag);
derivation *child;
for (gl_list_iterator_t it = gl_list_iterator (deriv->children);
derivation_list_next (&it, &child);
)
{
derivation_print (child, f);
fputs (" ", f);
end_use_class ("cex-step", f);
}
fputs ("]", f);
}
void
derivation_print_leaves (const derivation *deriv, FILE *f)
{
if (deriv == &d_dot)
{
fputs ("", f);
return;
}
if (!deriv->children)
{
symbol *sym = symbols[deriv->sym];
fprintf (f, "%s", sym->tag);
return;
}
const char *sep = "";
derivation *child;
for (gl_list_iterator_t it = gl_list_iterator (deriv->children);
@@ -175,6 +154,44 @@ derivation_print_leaves (const derivation *deriv, FILE *f)
{
fputs (sep, f);
sep = " ";
derivation_print_leaves (child, f);
derivation_print_impl (child, f, leaves_only, counter);
}
if (!leaves_only)
{
begin_use_class ("cex-step", f);
fputs (" ]", f);
end_use_class ("cex-step", f);
}
end_use_class (style, f);
}
else if (deriv == &d_dot)
{
begin_use_class ("cex-dot", f);
fputs ("", f);
end_use_class ("cex-dot", f);
}
else // leaf.
{
const symbol *sym = symbols[deriv->sym];
begin_use_class ("cex-leaf", f);
fprintf (f, "%s", sym->tag);
end_use_class ("cex-leaf", f);
}
}
void
derivation_print (const derivation *deriv, FILE *f)
{
int counter = 0;
derivation_print_impl (deriv, f, false, &counter);
fputc ('\n', f);
}
void
derivation_print_leaves (const derivation *deriv, FILE *f)
{
int counter = 0;
derivation_print_impl (deriv, f, true, &counter);
fputc ('\n', f);
}

View File

@@ -20,6 +20,7 @@
#ifndef DERIVATION_H
# define DERIVATION_H
# include <gl_linked_list.h>
# include <gl_xlist.h>
# include "gram.h"

View File

@@ -49,6 +49,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
1: 8 y: A . B
Example A • B C
First derivation s ::=[ a ::=[ A • ] x ::=[ B C ] ]
Example A • B C
Second derivation s ::=[ y ::=[ A • B ] c ::=[ C ] ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -80,6 +81,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
1: 5 b: . B
Example A • B C
First derivation s ::=[ a ::=[ A • ] bc ::=[ B C ] ]
Example A • B C
Second derivation s ::=[ ac ::=[ A ac ::=[ b ::=[ • B ] ] C ] ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -112,14 +114,15 @@ AT_BISON_CHECK_CEX([input.y], [], [],
1: 9 xby: . B
Example A • B y
First derivation s ::=[ ax ::=[ A x ::=[ • ] ] by ::=[ B y ] ]
Example A • B
Second derivation s ::=[ A xby ::=[ • B ] ]
Shift/reduce conflict on token B:
5: 4 x: . %empty
5: 9 xby: . B
First Example A X • B y $end
First example A X • B y $end
First derivation $accept ::=[ s ::=[ ax ::=[ A x ::=[ X x ::=[ • ] ] ] by ::=[ B y ] ] $end ]
Second Example A X B Y $end
Second example A X • B Y $end
Second derivation $accept ::=[ s ::=[ A xby ::=[ X xby ::=[ • B ] Y ] ] $end ]
input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
@@ -150,9 +153,9 @@ AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift/reduce conflict on token C:
2: 7 b: B .
2: 9 bc: B . C
First Example B C D $end
First example B • C D $end
First derivation $accept ::=[ g ::=[ x ::=[ b ::=[ B • ] cd ::=[ C D ] ] ] $end ]
Second Example B • C $end
Second example B • C $end
Second derivation $accept ::=[ g ::=[ x ::=[ bc ::=[ B • C ] ] ] $end ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -181,9 +184,9 @@ AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift/reduce conflict on token A:
1: 5 x: A .
1: 6 y: A . A B
First Example A A $end
First example A • A $end
First derivation $accept ::=[ s ::=[ s ::=[ t ::=[ x ::=[ A • ] ] ] t ::=[ x ::=[ A ] ] ] $end ]
Second Example A A B $end
Second example A • A B $end
Second derivation $accept ::=[ s ::=[ t ::=[ y ::=[ A • A B ] ] ] $end ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -218,14 +221,15 @@ AT_BISON_CHECK_CEX([input.y], [], [],
4: 7 s: b . A xx y
Example b • A X X Y
First derivation a ::=[ r ::=[ b • ] t ::=[ A x ::=[ X ] xy ::=[ X Y ] ] ]
Example b • A X X Y
Second derivation a ::=[ s ::=[ b • xx ::=[ A X X ] y ::=[ Y ] ] ]
Shift/reduce conflict on token X:
10: 8 x: X .
10: 9 xx: X . X
First Example X X xy
First example X • X xy
First derivation a ::=[ x ::=[ X • ] t ::=[ X xy ] ]
Second Example A X • X
Second example A X • X
Second derivation a ::=[ t ::=[ A xx ::=[ X • X ] ] ]
input.y: warning: 2 shift/reduce conflicts [-Wconflicts-sr]
@@ -255,6 +259,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
4: 3 b: b .
Example A b •
First derivation a ::=[ A b • ]
Example A b •
Second derivation a ::=[ A b ::=[ b • ] ]
input.y: warning: 1 reduce/reduce conflict [-Wconflicts-rr]
@@ -282,9 +287,9 @@ AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce/reduce conflict on tokens A, C:
2: 5 a: D .
2: 6 b: D .
First Example D • A $end
First example D • A $end
First derivation $accept ::=[ s ::=[ a ::=[ D • ] A ] $end ]
Second Example B D A $end
Second example B D • A $end
Second derivation $accept ::=[ s ::=[ B b ::=[ D • ] A ] $end ]
input.y: warning: 2 reduce/reduce conflicts [-Wconflicts-rr]
@@ -313,9 +318,9 @@ AT_BISON_CHECK_CEX([input.y], [], [],
5: 2 a: H i .
5: 4 i: i . J K
time limit exceeded: XXX
First Example H i J $end
First example H i • J $end
First derivation $accept ::=[ s ::=[ a ::=[ H i • ] J ] $end ]
Second Example H i J K $end
Second example H i • J K $end
Second derivation $accept ::=[ a ::=[ H i ::=[ i • J K ] ] $end ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -349,6 +354,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
4: 8 b: A . B C
Example N A • B C
First derivation s ::=[ n ::=[ N a ::=[ A • ] B ] C ]
Example N A • B C
Second derivation s ::=[ n ::=[ N b ::=[ A • B C ] ] ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -383,6 +389,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
3: 5 A: . %empty
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:
@@ -390,6 +397,7 @@ Reduce/reduce conflict on tokens b, c:
4: 5 A: . %empty
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 ] ]
input.y: warning: 4 reduce/reduce conflicts [-Wconflicts-rr]
@@ -417,52 +425,52 @@ AT_BISON_CHECK_CEX([input.y], [], [],
[[Reduce/reduce conflict on token A:
0: 3 b: . %empty
0: 4 c: . %empty
First Example c A A $end
First example • c A A $end
First derivation $accept ::=[ a ::=[ b ::=[ • ] d ::=[ c A A ] ] $end ]
Second Example c A A $end
Second example • c A A $end
Second derivation $accept ::=[ a ::=[ c ::=[ • ] d ::=[ c A A ] ] $end ]
Reduce/reduce conflict on token A:
2: 3 b: . %empty
2: 4 c: . %empty
time limit exceeded: XXX
First Example b c A A $end
First example b • c A A $end
First derivation $accept ::=[ a ::=[ b d ::=[ a ::=[ b ::=[ • ] d ::=[ c A A ] ] ] ] $end ]
Second Example b • A $end
Second example b • A $end
Second derivation $accept ::=[ a ::=[ b d ::=[ c ::=[ • ] A ] ] $end ]
Reduce/reduce conflict on token A:
3: 3 b: . %empty
3: 4 c: . %empty
time limit exceeded: XXX
First Example c c A A $end
First example c • c A A $end
First derivation $accept ::=[ a ::=[ c d ::=[ a ::=[ b ::=[ • ] d ::=[ c A A ] ] ] ] $end ]
Second Example c • A $end
Second example c • A $end
Second derivation $accept ::=[ a ::=[ c d ::=[ c ::=[ • ] A ] ] $end ]
Shift/reduce conflict on token A:
6: 3 b: . %empty
6: 6 d: c . A
time limit exceeded: XXX
First Example b c c A A $end
First example b c • c A A $end
First derivation $accept ::=[ a ::=[ b d ::=[ a ::=[ c d ::=[ a ::=[ b ::=[ • ] d ::=[ c A A ] ] ] ] ] ] $end ]
Second Example b c • A
Second example b c • A
Second derivation a ::=[ b d ::=[ c • A ] ]
Reduce/reduce conflict on token A:
6: 3 b: . %empty
6: 4 c: . %empty
First Example b c c A A $end
First example b c • c A A $end
First derivation $accept ::=[ a ::=[ b d ::=[ a ::=[ c d ::=[ a ::=[ b ::=[ • ] d ::=[ c A A ] ] ] ] ] ] $end ]
Second Example b c A $end
Second example b c • A $end
Second derivation $accept ::=[ a ::=[ b d ::=[ a ::=[ c d ::=[ c ::=[ • ] A ] ] ] ] $end ]
Shift/reduce conflict on token A:
6: 4 c: . %empty
6: 6 d: c . A
First Example b c A $end
First example b c • A $end
First derivation $accept ::=[ a ::=[ b d ::=[ a ::=[ c d ::=[ c ::=[ • ] A ] ] ] ] $end ]
Second Example b c • A
Second example b c • A
Second derivation a ::=[ b d ::=[ c • A ] ]
Reduce/reduce conflict on token $end:
@@ -470,6 +478,7 @@ Reduce/reduce conflict on token $end:
7: 7 d: d .
Example b d •
First derivation a ::=[ b d • ]
Example b d •
Second derivation a ::=[ b d ::=[ d • ] ]
Reduce/reduce conflict on token $end:
@@ -477,6 +486,7 @@ Reduce/reduce conflict on token $end:
8: 7 d: d .
Example c d •
First derivation a ::=[ c d • ]
Example c d •
Second derivation a ::=[ c d ::=[ d • ] ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -511,6 +521,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
7: 3 a: H i J . J
Example H i J • J J
First derivation s ::=[ a ::=[ H i ::=[ i J • ] J J ] ]
Example H i J • J J
Second derivation s ::=[ a ::=[ H i J • J ] J ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -545,6 +556,7 @@ AT_BISON_CHECK_CEX([input.y], [], [],
3: 6 d: . D
Example A a • D
First derivation s ::=[ A a a ::=[ b ::=[ c ::=[ • ] ] ] d ::=[ D ] ]
Example A a • D
Second derivation s ::=[ A a d ::=[ • D ] ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]
@@ -575,9 +587,9 @@ AT_BISON_CHECK_CEX([input.y], [], [],
[[Shift/reduce conflict on token D:
3: 5 c: . %empty
3: 6 d: . D
First Example A a • D E $end
First example A a • D E $end
First derivation $accept ::=[ s ::=[ A a a ::=[ b ::=[ c ::=[ • ] ] ] d ::=[ D ] E ] $end ]
Second Example A a D $end
Second example A a • D $end
Second derivation $accept ::=[ s ::=[ A a d ::=[ • D ] ] $end ]
input.y: warning: 1 shift/reduce conflict [-Wconflicts-sr]