{- |
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 SoftFOL.Translate
    ( transId
    , transSenName
    , checkIdentifier
    , CKType (..)
    ) where

import Data.Char
import qualified Data.Set as Set

import Common.Id
import Common.ProofUtils

import SoftFOL.Sign

data CKType = CKSort | CKVar | CKPred | CKOp

-- | collect all keywords of SoftFOL
reservedWords :: Set.Set String
reservedWords :: Set String
reservedWords = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ (SPSymbol -> String) -> [SPSymbol] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SPSymbol -> String
showSPSymbol
  [ SPSymbol
SPEqual
  , SPSymbol
SPTrue
  , SPSymbol
SPFalse
  , SPSymbol
SPOr
  , SPSymbol
SPAnd
  , SPSymbol
SPNot
  , SPSymbol
SPImplies
  , SPSymbol
SPImplied
  , SPSymbol
SPEquiv]
 {- this list of reserved words has been generated with:
 perl HetCATS/utils/transformLexerFile.pl spass-3.0c/dfgscanner.l -}
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
words
  [ "and author axioms begin_problem by box all clause cnf comp"
  , "conjectures conv date description dia some div dnf domain"
  , "domrestr eml EML DL end_of_list end_problem equal equiv"
  , "exists false forall formula freely functions generated"
  , "hypothesis id implied implies list_of_clauses list_of_declarations"
  , "list_of_descriptions list_of_formulae list_of_general_settings"
  , "list_of_proof list_of_settings list_of_special_formulae"
  , "list_of_symbols list_of_terms logic name not operators"
  , "or prop_formula concept_formula predicate predicates quantifiers"
  , "ranrestr range rel_formula role_formula satisfiable set_DomPred"
  , "set_flag set_precedence set_ClauseFormulaRelation set_selection"
  , "sort sorts status step subsort sum test translpairs true"
  , "unknown unsatisfiable version static"]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (('e' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [0 .. 20 :: Int]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (("fmdarwin_e" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) [0 .. 20 :: Int]

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 -> SPIdentifier
transId :: CKType -> Id -> SPIdentifier
transId t :: CKType
t = String -> SPIdentifier
mkSimpleId (String -> SPIdentifier) -> (Id -> String) -> Id -> SPIdentifier
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 "SoftFOL.Translate.transId: 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
        if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
lstr Set String
reservedWords then "x_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str else 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]