Translate.hs revision d9d546103be1753c4576502f40c296ce88eb69e3
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekModule : $Header$
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekDescription : create legal THF mixfix identifier
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekCopyright : (c) A. Tsogias, DFKI Bremen 2011
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekLicense : GPLv2 or higher, see LICENSE.txt
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekMaintainer : Alexis.Tsogias@dfki.de
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekStability : provisional
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekPortability : portable
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozektranslate 'Id' to THF Constant
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozekimport qualified Common.ProofUtils as CM (charMap)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozekimport THF.As as THFAs
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozekimport qualified Data.Map as Map
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub HrozekmkTypesName c = case c of
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek $ mkSimpleId ("type_" ++ show w)
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek $ mkSimpleId ("type_" ++ show s)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmkConstsName c = case c of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek $ mkSimpleId ("const_" ++ show w)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek $ mkSimpleId ("const_" ++ show s)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmkDefName c = case c of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek $ mkSimpleId ("def_" ++ show w)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek $ mkSimpleId ("def_" ++ show s)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransTypeId :: Id -> Result THFAs.Constant
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransTypeId id1 = case maybeElem id1 preDefHCTypeIds of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Just res -> return $ stringToConstant res
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Nothing -> case transToTHFString $ show id1 of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Just s -> return . A_Lower_Word . mkSimpleId $ "x_" ++ s
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek " into a THF valide Constant.") nullRange
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransAssumpId :: Id -> Result THFAs.Constant
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransAssumpId id1 = case maybeElem id1 preDefHCAssumpIds of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Just res -> return $ stringToConstant res
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Nothing -> case transToTHFString $ show id1 of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Just s -> return $ stringToConstant s
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek " into a THF valide Constant.") nullRange
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransAssumpsId :: Id -> Int -> Result THFAs.Constant
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub HrozektransAssumpsId id1 int = if int == 1 then transAssumpId id1 else
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek case transToTHFString $ show id1 of
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Just s -> return $ stringToConstant (s ++ show int)
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek " into a THF valide Constant.") nullRange
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToConstant :: String -> THFAs.Constant
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToConstant = A_Lower_Word . stringToLowerWord
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToLowerWord :: String -> Token
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToLowerWord = mkSimpleId . \ s -> case s of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek c : r -> if isLower c then s else 'x' : c : r
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToVariable :: String -> String
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekstringToVariable s = case s of
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek c : r -> if isUpper c then s else let d = toUpper c in d : 'x' : d : r
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransVarId :: Id -> Result Token
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransVarId id1 = case transToTHFString $ show id1 of
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Just s -> return $ mkSimpleId $ stringToVariable s
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek " into a THF valide Variable.") nullRange
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub HrozektransToTHFString :: String -> Maybe String
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub HrozektransToTHFString = transToTHFStringAux True
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransToTHFStringAux :: Bool -> String -> Maybe String
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozektransToTHFStringAux first s = case s of
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek "" -> Just ""
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek c : rc -> let
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek x = 'x' -- escape character
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek rest = transToTHFStringAux False rc
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek if isTHFChar c
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek then if first && isDigit c || c == x then fmap ([x, c] ++) rest else
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek fmap (c :) rest
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek else case Map.lookup c charMap of
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Just res -> fmap (res ++) rest
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek Nothing -> Nothing
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekisTHFChar :: Char -> Bool
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekisTHFChar c = isAlphaNum c && isAscii c || c == '_'
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekisLowerTHFChar :: Char -> Bool
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekisLowerTHFChar c = isLower c && isAscii c
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekpreDefHCTypeIds :: Map.Map Id String
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekpreDefHCTypeIds = Map.fromList
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek [ (logId, "hct" ++ show logId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (predTypeId, "hct" ++ show predTypeId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (unitTypeId, "hct" ++ show unitTypeId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (lazyTypeId, "hctLazy")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (arrowId FunArr, "hct__FunArr__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (arrowId PFunArr, "hct__PFunArr__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (arrowId ContFunArr, "hct__ContFunArr__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (arrowId PContFunArr, "hct__PContFunArr__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (productId 2 nullRange, "hct__X__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (productId 3 nullRange, "hct__X__X__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (productId 4 nullRange, "hct__X__X__X__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (productId 5 nullRange, "hct__X__X__X__X__") ]
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekpreDefHCAssumpIds :: Map.Map Id String
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekpreDefHCAssumpIds = Map.fromList
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek [ (botId, "hcc" ++ show botId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (defId, "hcc" ++ show defId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (notId, "hcc" ++ show notId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (negId, "hccNeg__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (whenElse, "hcc" ++ show whenElse)
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (trueId, "hcc" ++ show trueId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (falseId, "hcc" ++ show falseId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (eqId, "hcc__Eq__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (exEq, "hcc__ExEq__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (resId, "hcc" ++ show resId)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (andId, "hcc__And__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (orId, "hcc__Or__")
f17d26a8db285622a5cd5f21c7488b62eedc2cf8Jakub Hrozek , (eqvId, "hcc__Eqv__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (implId, "hcc__Impl__")
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek , (infixIf, "hcc" ++ show infixIf) ]
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmaybeElem :: Id -> Map.Map Id a -> Maybe a
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmaybeElem id1 m = helper id1 (Map.toList m)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek helper :: Id -> [(Id, a)] -> Maybe a
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek helper _ [] = Nothing
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek helper id2 ((eid, ea) : r) =
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek if myEqId id2 eid then Just ea else helper id2 r
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmyEqId :: Id -> Id -> Bool
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekmyEqId (Id t1 c1 _) (Id t2 c2 _) = (t1, c1) == (t2, c2)
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek-- | a separate Map speeds up lookup
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekcharMap :: Map.Map Char String
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub HrozekcharMap = Map.insert '\'' "Apostrophe"
cc84fd46f356c4a36a721ab135a33ec77c93e34dJakub Hrozek -- this map is no longer injective