Translate.hs revision 96a6c2a58e8c534f983002f8d503f97ea1b4aa8d
{- |
Module : $Header$
Description : create legal THF mixfix identifier
Copyright : (c) A. Tsogias, DFKI Bremen 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Alexis.Tsogias@dfki.de
Stability : provisional
Portability : portable
translate 'Id' to THF Constant
-}
module THF.Translate where
import Common.Id
import Common.Result
import HasCASL.Builtin
import HasCASL.AsUtils
import THF.As as THFAs
import Data.Char
import qualified Data.Map as Map
mkTypesName :: THFAs.Constant -> THFAs.Name
mkTypesName c = case c of
A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word ("type_" ++ w)
A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted ("type_" ++ s)
mkConstsName :: THFAs.Constant -> THFAs.Name
mkConstsName c = case c of
A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word ("const_" ++ w)
A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted ("const_" ++ s)
mkDefName :: THFAs.Constant -> THFAs.Name
mkDefName c = case c of
A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word ("def_" ++ w)
A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted ("def_" ++ s)
transTypeId :: Id -> Result THFAs.Constant
transTypeId id1 = case maybeElem id1 preDefHCTypeIds of
Just res -> return $ stringToConstant res
Nothing -> case transToTHFString $ show id1 of
Just s -> return $ stringToConstant s
Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
" into a THF valide Constant.") nullRange
transAssumpId :: Id -> Result THFAs.Constant
transAssumpId id1 = case maybeElem id1 preDefHCAssumpIds of
Just res -> return $ stringToConstant res
Nothing -> case transToTHFString $ show id1 of
Just s -> return $ stringToConstant s
Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
" into a THF valide Constant.") nullRange
transAssumpsId :: Id -> Int -> Result THFAs.Constant
transAssumpsId id1 int = if int == 1 then transAssumpId id1 else
case transToTHFString $ show id1 of
Just s -> return $ stringToConstant (s ++ show int)
Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
" into a THF valide Constant.") nullRange
stringToConstant :: String -> THFAs.Constant
stringToConstant = A_Lower_Word . stringToLowerWord
stringToLowerWord :: String -> THFAs.LowerWord
stringToLowerWord (c1 : rc) = toLower c1 : rc
stringToLowerWord [] = []
stringToVariable :: String -> THFAs.Variable
stringToVariable (c1 : rc) = toUpper c1 : rc
stringToVariable [] = []
transVarId :: Id -> Result THFAs.Variable
transVarId id1 = case transToTHFString $ show id1 of
Just s -> return $ stringToVariable s
Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
" into a THF valide Variable.") nullRange
transToTHFString :: String -> Maybe String
transToTHFString s = case s of
[] -> Just []
(c : rc) ->
if isTHFChar c
then fmap (c :) (transToTHFString rc)
else case Map.lookup c charMap of
Just res -> fmap (res ++) (transToTHFString rc)
Nothing -> Nothing
isTHFChar :: Char -> Bool
isTHFChar c = (isAlphaNum c && isAscii c) || c == '_'
isLowerTHFChar :: Char -> Bool
isLowerTHFChar c = isLower c && isAscii c
preDefHCTypeIds :: Map.Map Id String
preDefHCTypeIds = Map.fromList
[ (logId, "hct" ++ show logId)
, (predTypeId, "hct" ++ show predTypeId)
, (unitTypeId, "hct" ++ show unitTypeId)
, (lazyTypeId, "hctLazy")
, (arrowId FunArr, "hct__FunArr__")
, (arrowId PFunArr, "hct__PFunArr__")
, (arrowId ContFunArr, "hct__ContFunArr__")
, (arrowId PContFunArr, "hct__PContFunArr__")
, (productId 2 nullRange, "hct__X__")
, (productId 3 nullRange, "hct__X__X__")
, (productId 4 nullRange, "hct__X__X__X__")
, (productId 5 nullRange, "hct__X__X__X__X__") ]
preDefHCAssumpIds :: Map.Map Id String
preDefHCAssumpIds = Map.fromList
[ (botId, "hcc" ++ show botId)
, (defId, "hcc" ++ show defId)
, (notId, "hcc" ++ show notId)
, (negId, "hccNeg__")
, (whenElse, "hcc" ++ show whenElse)
, (trueId, "hcc" ++ show trueId)
, (falseId, "hcc" ++ show falseId)
, (eqId, "hcc__Eq__")
, (exEq, "hcc__ExEq__")
, (resId, "hcc" ++ show resId)
, (andId, "hcc__And__")
, (orId, "hcc__Or__")
, (eqvId, "hcc__Eqv__")
, (implId, "hcc__Impl__")
, (infixIf, "hcc" ++ show infixIf) ]
maybeElem :: Id -> Map.Map Id a -> Maybe a
maybeElem id1 m = helper id1 (Map.toList m)
where
helper :: Id -> [(Id, a)] -> Maybe a
helper _ [] = Nothing
helper id2 ((eid, ea) : r) =
if myEqId id2 eid then Just ea else helper id2 r
myEqId :: Id -> Id -> Bool
myEqId (Id t1 c1 _) (Id t2 c2 _) = (t1, c1) == (t2, c2)
-- | a separate Map speeds up lookup
charMap :: Map.Map Char String
charMap = Map.fromList
[(' ' , "Space"),
('\n', "Newline"),
('\t', "Tab"),
('!' , "Exclam"),
('"' , "Quot"),
('#' , "Hash"),
('$' , "Dollar"),
('%' , "Percent"),
('&' , "Amp"),
('\'', "Apostrophe"),
('(' , "OBr"),
(')' , "CBr"),
('*' , "X"),
('+' , "Plus"),
(',' , "Comma"),
('-' , "Minus"),
('.' , "Dot"),
('/' , "Slash"),
(':' , "Colon"),
(';' , "Semi"),
('<' , "Lt"),
('=' , "Eq"),
('>' , "Gt"),
('?' , "Quest"),
('@' , "At"),
('[' , "OSqBr"),
('\\' , "Bslash"),
(']' , "CSqBr"),
('^' , "Caret"), -- Hat?
('`' , "Grave"),
('{' , "LBrace"),
('|' , "VBar"),
('}' , "RBrace"),
('~' , "Tilde"),
('\160', "Nbsp"),
('\161', "Iexcl"),
('\162', "Cent"),
('\163', "Pound"),
('\164', "Curren"),
('\165', "Yen"),
('\166', "Brvbar"),
('\167', "Sect"),
('\168', "Uml"),
('\169', "Copy"),
('\170', "Ordf"),
('\171', "Laquo"),
('\172', "Not"),
('\173', "Shy"),
('\174', "Reg"),
('\175', "Macr"),
('\176', "Deg"),
('\177', "Plusmn"),
('\178', "Sup2"),
('\179', "Sup3"),
('\180', "Acute"),
('\181', "Micro"),
('\182', "Para"),
('\183', "Middot"),
('\184', "Cedil"),
('\185', "Sup1"),
('\186', "Ordm"),
('\187', "Raquo"),
('\188', "Quarter"),
('\189', "Half"),
('\190', "Frac34"),
('\191', "Iquest"),
('\192', "Agrave"),
('\193', "Aacute"),
('\194', "Acirc"),
('\195', "Atilde"),
('\196', "Auml"),
('\197', "Aring"),
('\198', "AElig"),
('\199', "Ccedil"),
('\200', "Egrave"),
('\201', "Eacute"),
('\202', "Ecirc"),
('\203', "Euml"),
('\204', "Igrave"),
('\205', "Iacute"),
('\206', "Icirc"),
('\207', "Iuml"),
('\208', "ETH"),
('\209', "Ntilde"),
('\210', "Ograve"),
('\211', "Oacute"),
('\212', "Ocirc"),
('\213', "Otilde"),
('\214', "Ouml"),
('\215', "Times"),
('\216', "OSlash"),
('\217', "Ugrave"),
('\218', "Uacute"),
('\219', "Ucirc"),
('\220', "Uuml"),
('\221', "Yacute"),
('\222', "THORN"),
('\223', "Szlig"),
('\224', "Agrave"),
('\225', "Aacute"),
('\226', "Acirc"),
('\227', "Atilde"),
('\228', "Auml"),
('\229', "Aring"),
('\230', "Aelig"),
('\231', "Ccedil"),
('\232', "Egrave"),
('\233', "Eacute"),
('\234', "Ecirc"),
('\235', "Euml"),
('\236', "Igrave"),
('\237', "Iacute"),
('\238', "Icirc"),
('\239', "Iuml"),
('\240', "Eth"),
('\241', "Ntilde"),
('\242', "Ograve"),
('\243', "Oacute"),
('\244', "Ocirc"),
('\245', "Otilde"),
('\246', "Ouml"),
('\247', "Divide"),
('\248', "Oslash"),
('\249', "Ugrave"),
('\250', "Uacute"),
('\251', "Ucirc"),
('\252', "Uuml"),
('\253', "Yacute"),
('\254', "Thorn"),
('\255', "Yuml")]