{- |
Module      :  ./TPTP/Common.hs
Description :  Common functions for TPTP handling.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional

-}

module TPTP.Common where

import Common.IRI
import Common.Id

import Data.Text (pack, replace, unpack)

-- The TPTP library uses filenames like AGT027^1.p which are not IRI compliant.
-- They need to be escaped.
-- In order to display the filename anyway, the unescaped IRI is saved as the
-- name of the spec.
-- These functions are only used for file names (in includes) and spec names.

escapeTPTPFilePath :: String -> String
escapeTPTPFilePath :: String -> String
escapeTPTPFilePath s :: String
s = Text -> String
unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text -> Text
replace (String -> Text
pack "^") (String -> Text
pack "%5E") (String -> Text
pack String
s)

unescapeTPTPFilePath :: String -> String
unescapeTPTPFilePath :: String -> String
unescapeTPTPFilePath s :: String
s = Text -> String
unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text -> Text
replace (String -> Text
pack "%5E") (String -> Text
pack "^") (String -> Text
pack String
s)

unescapeTPTPFileToken :: Token -> Token
unescapeTPTPFileToken :: Token -> Token
unescapeTPTPFileToken t :: Token
t = Token
t { tokStr :: String
tokStr = String -> String
unescapeTPTPFilePath (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Token -> String
tokStr Token
t }

unescapeTPTPFileId :: Id -> Id
unescapeTPTPFileId :: Id -> Id
unescapeTPTPFileId i :: Id
i = Id
i { getTokens :: [Token]
getTokens = (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map Token -> Token
unescapeTPTPFileToken ([Token] -> [Token]) -> [Token] -> [Token]
forall a b. (a -> b) -> a -> b
$ Id -> [Token]
getTokens Id
i }

unescapeTPTPFileIRI :: IRI -> IRI
unescapeTPTPFileIRI :: IRI -> IRI
unescapeTPTPFileIRI i :: IRI
i = IRI
i { iriPath :: Id
iriPath = Id -> Id
unescapeTPTPFileId (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ IRI -> Id
iriPath IRI
i }