bei ResStep-Wiedergabe auch die Nummerierung mit ausgeben

[jvoigtlaender]

Wenn bei einer entsprechenden Aufgabe aktuell sowas eingegeben wird:

[ (1,2,{D} = 42), (3,4,{-D} = 23), (42,23,{}) ]

erfolgt dann als Wiedergabe im Bewertungsabschnitt:

gelesen: 
[ (1,2,{D}), (3,4,{¬D}), (42,23,{}) ]
...

Die Information über die Nummerierung der Resolventen ist nicht mehr vorhanden. Insofern lässt sich der Bewertungsteil nicht eindeutig lesen.

Besser wäre Ausgabe von:

gelesen: 
[ (1,2,{D} = 42), (3,4,{¬D} = 23), (42,23,{}) ]
...

oder gegebenenfalls auch (per Normalisierung der Nummerierung für die Ausgabe):

gelesen: 
[ (1,2,{D} = 5), (3,4,{¬D} = 6), (5,6,{}) ]
...

[jvoigtlaender]

Maybe pretty' after the change from https://github.com/fmidue/logic-tasks/pull/78/commits/bb0aa1dcd8da31fe95aa999939a1fd82170b9488 can simply be used to fix this?

[nimec01]

Wo befindet sich der Code, der das "gelesen: ..." ausgibt?

Wenn ich es in der Konsole teste, sieht es richtig aus (auch wenn es hier anders dargestellt ist):

[jvoigtlaender]

Das Problem ist genau die Ausgabe. Also was dort in der Zeile nach Input steht, wird in Autotool pretty-printed. Sollte es zumindest. Im konkreten Fall aber wird dabei Information weggelassen (bei der Ausgabe in Autotool). Der relevante Code ist hier: https://git.uni-due.de/fmi/autotool-dev/-/blob/autotool-fmi/interface/src/Inter/Evaluate.hs?ref_type=heads#L38-L47

Bzw. in Quelltext:

parse_or_complain :: ( Reader a, ToDoc a ) 
                  => String -> Reporter a
parse_or_complain cs = 
    case parse (parse_complete reader) "input" cs of
         Left e -> do
               informText $ text "Syntaxfehler:"
               rejectPreWith Syntax $ errmsg 72 e $ cs
         Right b  -> do
               output $ Pre $ text "gelesen:" <+> toDoc b
               return b

Es kann also wohl nur Autotool-seitig gefixt werden.

[jvoigtlaender]

Bzw. nein, Autotool greift letztlich in den meisten Fällen doch auf Code in diesem Repo zurück, um etwas anzuzeigen. Im konkreten Fall dürfte das Problem hier liegen: https://github.com/fmidue/logic-tasks/blob/ee6dd0c40c4873b7f0e70997afbca03927aeb007/src/Formula/Printing.hs#L42-L47

Also dass prettyClause einen Teil ignoriert.

[jvoigtlaender]

Das heißt auch, dass der Code https://github.com/fmidue/logic-tasks/blob/ee6dd0c40c4873b7f0e70997afbca03927aeb007/src/Formula/Resolution.hs#L190-L201 dann vielleicht auf die obige (zu korrigierende) Pretty-Instanz "umgebogen" werden sollte.