module PGIP.Output.Formatting where

import Common.Utils

import Logic.Logic
import Logic.Comorphism

import Proofs.AbstractState

import Data.Char

internalProverName :: ProverOrConsChecker -> String
internalProverName :: ProverOrConsChecker -> String
internalProverName pOrCc :: ProverOrConsChecker
pOrCc = case ProverOrConsChecker
pOrCc of
  Prover pr :: G_prover
pr -> G_prover -> String
getProverName G_prover
pr
  ConsChecker cc :: G_cons_checker
cc -> G_cons_checker -> String
getCcName G_cons_checker
cc

showComorph :: AnyComorphism -> String
showComorph :: AnyComorphism -> String
showComorph (Comorphism cid :: cid
cid) = String -> String
mkNiceProverName (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> String
forall a. Int -> [a] -> [a]
drop 1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= ':')
  (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ';' then ':' else Char
c)
  (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid

mkNiceProverName :: String -> String
mkNiceProverName :: String -> String
mkNiceProverName = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (\ c :: Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_.:-")

proversOnly :: [(AnyComorphism, [ProverOrConsChecker])] -> [ProverOrConsChecker]
proversOnly :: [(AnyComorphism, [ProverOrConsChecker])] -> [ProverOrConsChecker]
proversOnly = (ProverOrConsChecker -> String)
-> [ProverOrConsChecker] -> [ProverOrConsChecker]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (String -> String
mkNiceProverName (String -> String)
-> (ProverOrConsChecker -> String) -> ProverOrConsChecker -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProverOrConsChecker -> String
internalProverName) ([ProverOrConsChecker] -> [ProverOrConsChecker])
-> ([(AnyComorphism, [ProverOrConsChecker])]
    -> [ProverOrConsChecker])
-> [(AnyComorphism, [ProverOrConsChecker])]
-> [ProverOrConsChecker]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((AnyComorphism, [ProverOrConsChecker]) -> [ProverOrConsChecker])
-> [(AnyComorphism, [ProverOrConsChecker])]
-> [ProverOrConsChecker]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (AnyComorphism, [ProverOrConsChecker]) -> [ProverOrConsChecker]
forall a b. (a, b) -> b
snd

showProversOnly :: [(AnyComorphism, [String])] -> [String]
showProversOnly :: [(AnyComorphism, [String])] -> [String]
showProversOnly = [String] -> [String]
forall a. Ord a => [a] -> [a]
nubOrd ([String] -> [String])
-> ([(AnyComorphism, [String])] -> [String])
-> [(AnyComorphism, [String])]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((AnyComorphism, [String]) -> [String])
-> [(AnyComorphism, [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (AnyComorphism, [String]) -> [String]
forall a b. (a, b) -> b
snd