{- |
Module      :  ./SoftFOL/Translate.hs
Description :  utility to create valid identifiers for atp provers
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

collection of functions used by "Comorphisms.SuleCFOL2SoftFOL" and
 "SoftFOL.ProveSPASS" for the translation of CASL identifiers and axiom labels
 into valid SoftFOL identifiers -}

module TPTP.Translate
    ( transId
    , transSenName
    , checkIdentifier
    , CKType (..)
    ) where

import Data.Char

import Common.Id
import Common.ProofUtils


data CKType = CKSort | CKVar | CKPred | CKOp


transSenName :: String -> String
transSenName :: String -> String
transSenName = CKType -> String -> String
transIdString CKType
CKSort (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
transToSPChar

{- |
  SPASS Identifiers may contain letters, digits, and underscores only; but
  for TPTP the allowed starting letters are different for each sort of
  identifier.
-}
checkIdentifier :: CKType -> String -> Bool
checkIdentifier :: CKType -> String -> Bool
checkIdentifier t :: CKType
t str :: String
str = case String
str of
  "" -> Bool
False
  c :: Char
c : _ -> (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
checkSPChar String
str Bool -> Bool -> Bool
&& case CKType
t of
    CKVar -> Char -> Bool
isUpper Char
c -- for TPTP
    _ -> Char -> Bool
isLower Char
c

{- |
Allowed SPASS characters are letters, digits, and underscores.
Warning:
Data.Char.isAlphaNum includes all kinds of isolatin1 characters!! -}
checkSPChar :: Char -> Bool
checkSPChar :: Char -> Bool
checkSPChar c :: Char
c = Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
&& Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
|| '_' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c

transId :: CKType -> Id -> Token
transId :: CKType -> Id -> Token
transId t :: CKType
t = String -> Token
mkSimpleId (String -> Token) -> (Id -> String) -> Id -> Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CKType -> String -> String
transIdString CKType
t (String -> String) -> (Id -> String) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
transToSPChar (String -> String) -> (Id -> String) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> String
forall a. Show a => a -> String
show

transIdString :: CKType -> String -> String
transIdString :: CKType -> String -> String
transIdString t :: CKType
t str :: String
str = case String
str of
  "" -> String -> String
forall a. HasCallStack => String -> a
error "TPTP.Translate.transIdString: empty string not allowed"
  c :: Char
c : r :: String
r -> if Char -> Bool
isDigit Char
c then CKType -> String -> String
transIdString CKType
t (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Char -> String
substDigit Char
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r
    else case CKType
t of
      CKOp | '_' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c -> 'o' Char -> String -> String
forall a. a -> [a] -> [a]
: String
str
      CKPred | '_' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c -> 'p' Char -> String -> String
forall a. a -> [a] -> [a]
: String
str
      CKVar -> Char -> Char
toUpper Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r
      _ -> let lstr :: String
lstr = Char -> Char
toLower Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
r in String
lstr

transToSPChar :: Char -> String
transToSPChar :: Char -> String
transToSPChar c :: Char
c
 | Char -> Bool
checkSPChar Char
c = [Char
c]
 | Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c " \n" = "_"
 | Bool
otherwise = Char -> String
lookupCharMap Char
c

substDigit :: Char -> String
substDigit :: Char -> String
substDigit c :: Char
c = case Char
c of
  '0' -> "zero"
  '1' -> "one"
  '2' -> "two"
  '3' -> "three"
  '4' -> "four"
  '5' -> "five"
  '6' -> "six"
  '7' -> "seven"
  '8' -> "eight"
  '9' -> "nine"
  _ -> [Char
c]