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 bb0aa1d 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:

logic-tasks/src/Formula/Printing.hs

Lines 42 to 47 in ee6dd0c

	instance Pretty ResStep where
	pretty (Res (a,b,(c,_))) = tupled [litsOrNum a, litsOrNum b, prettyClause c]
	where
	litsOrNum = either prettyClause pretty
	curlyBracesList = encloseSep (char '{') (char '}') (char ',')
	prettyClause = curlyBracesList . map pretty . literals

Also dass prettyClause einen Teil ignoriert.

[jvoigtlaender]

Das heißt auch, dass der Code

logic-tasks/src/Formula/Resolution.hs

Lines 190 to 201 in ee6dd0c

	pretty' :: ResStep -> Bool -> String
	pretty' (Res (a,b,(c,d))) isLast = "(" ++ showEither a ++ ", " ++ showEither b ++ ", " ++ showClause ++ showNum ++ ")"
	where showEither (Left x) = show x
	showEither (Right y) = show y
	showNum = if isJust d && not isLast then " = " ++ show (fromJust d) else ""
	litSet = literalSet c
	showClause = if null litSet then "{ }" else "{" ++ intercalate "," (map show (Set.toList litSet)) ++ "}"
	showResSteps :: [ResStep] -> [String]
	showResSteps [] = []
	showResSteps [x] = [pretty' x True]
	showResSteps (x:xs) = pretty' x False : showResSteps xs

dann vielleicht auf die obige (zu korrigierende) Pretty-Instanz "umgebogen" werden sollte.