Translate.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{- |
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.fromList $ map showSPSymbol
[ SPEqual
, SPTrue
, SPFalse
, SPOr
, SPAnd
, SPNot
, SPImplies
, SPImplied
, SPEquiv]
{- this list of reserved words has been generated with:
perl HetCATS/utils/transformLexerFile.pl spass-3.0c/dfgscanner.l -}
++ concatMap 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"]
++ map (('e' :) . show) [0 .. 20 :: Int]
++ map (("fmdarwin_e" ++) . show) [0 .. 20 :: Int]
transSenName :: String -> String
transSenName = transIdString CKSort . concatMap 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 t str = case str of
"" -> False
c : _ -> all checkSPChar str && case t of
CKVar -> isUpper c -- for TPTP
_ -> isLower c
{- |
Allowed SPASS characters are letters, digits, and underscores.
Warning:
Data.Char.isAlphaNum includes all kinds of isolatin1 characters!! -}
checkSPChar :: Char -> Bool
checkSPChar c = isAlphaNum c && isAscii c || '_' == c
transId :: CKType -> Id -> SPIdentifier
transId t = mkSimpleId . transIdString t . concatMap transToSPChar . show
transIdString :: CKType -> String -> String
transIdString t str = case str of
"" -> error "SoftFOL.Translate.transId: empty string not allowed"
c : r -> if isDigit c then transIdString t $ substDigit c ++ r
else case t of
CKOp | '_' == c -> 'o' : str
CKPred | '_' == c -> 'p' : str
CKVar -> toUpper c : r
_ -> let lstr = toLower c : r in
if Set.member lstr reservedWords then "x_" ++ str else lstr
transToSPChar :: Char -> String
transToSPChar c
| checkSPChar c = [c]
| elem c " \n" = "_"
| otherwise = lookupCharMap c
substDigit :: Char -> String
substDigit c = case c of
'0' -> "zero"
'1' -> "one"
'2' -> "two"
'3' -> "three"
'4' -> "four"
'5' -> "five"
'6' -> "six"
'7' -> "seven"
'8' -> "eight"
'9' -> "nine"
_ -> [c]