18d589be75aa0cbaacae9ab2884c0b07943de024Eugen Kuksamodule PGIP.Output.Formatting where

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

e1e5f30cafbcd33549c60a77eee73709b6f46249Eugen Kuksaimport Common.Utils

e1e5f30cafbcd33549c60a77eee73709b6f46249Eugen Kuksa

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksaimport Logic.Logic

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksaimport Logic.Comorphism

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksaimport Proofs.AbstractState

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksaimport Data.Char

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

beba53186708a907254c229f4097bb7de519b625Eugen KuksainternalProverName :: ProverOrConsChecker -> String

beba53186708a907254c229f4097bb7de519b625Eugen KuksainternalProverName pOrCc = case pOrCc of

bb39f9f3b231588a5ed36d424ae27c6e31852feaEugen Kuksa Prover pr -> getProverName pr

bb39f9f3b231588a5ed36d424ae27c6e31852feaEugen Kuksa ConsChecker cc -> getCcName cc

18d589be75aa0cbaacae9ab2884c0b07943de024Eugen Kuksa

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen KuksashowComorph :: AnyComorphism -> String

5fa563f0173e7791139e4229800fc91652293647Eugen KuksashowComorph (Comorphism cid) = mkNiceProverName . drop 1 . dropWhile (/= ':')

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa . map (\ c -> if c == ';' then ':' else c)

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa $ language_name cid

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

5fa563f0173e7791139e4229800fc91652293647Eugen KuksamkNiceProverName :: String -> String

5fa563f0173e7791139e4229800fc91652293647Eugen KuksamkNiceProverName = filter (\ c -> isAlphaNum c || elem c "_.:-")

fdf9cef4c2e81f477f3023fb8e45f6faebfa5a65Eugen Kuksa

d102a920578426a89411cc8dabe47d7a881eab8fEugen KuksaproversOnly :: [(AnyComorphism, [ProverOrConsChecker])] -> [ProverOrConsChecker]

ceb5bd32f163b29b1cbea577334bc869c07add04Eugen KuksaproversOnly = nubOrdOn (mkNiceProverName . internalProverName) . concatMap snd

d102a920578426a89411cc8dabe47d7a881eab8fEugen Kuksa

e1e5f30cafbcd33549c60a77eee73709b6f46249Eugen KuksashowProversOnly :: [(AnyComorphism, [String])] -> [String]

e1e5f30cafbcd33549c60a77eee73709b6f46249Eugen KuksashowProversOnly = nubOrd . concatMap snd