658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasDescription : create legal THF mixfix identifier
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasCopyright : (c) A. Tsogias, DFKI Bremen 2011
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasLicense : GPLv2 or higher, see LICENSE.txt
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasMaintainer : Alexis.Tsogias@dfki.de
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasStability : provisional
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasPortability : portable
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogiastranslate 'Id' to THF Constant
72204f862232e7e51b0207bba020c1d781fa7798Christian Maederimport qualified Common.ProofUtils as CM (charMap)
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogiasimport THF.As as THFAs
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogiasimport qualified Data.Map as Map
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmkTypesName c = case c of
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("type_" ++ show w)
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("type_" ++ show s)
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmkConstsName c = case c of
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("const_" ++ show w)
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("const_" ++ show s)
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmkDefName c = case c of
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("def_" ++ show w)
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder $ mkSimpleId ("def_" ++ show s)
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiastransTypeId :: Id -> Result THFAs.Constant
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis TsogiastransTypeId id1 = case maybeElem id1 preDefHCTypeIds of
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias Just res -> return $ stringToConstant res
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Nothing -> case transToTHFString $ show id1 of
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Just s -> return . A_Lower_Word . mkSimpleId $ "x_" ++ s
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias " into a THF valide Constant.") nullRange
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiastransAssumpId :: Id -> Result THFAs.Constant
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis TsogiastransAssumpId id1 = case maybeElem id1 preDefHCAssumpIds of
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias Just res -> return $ stringToConstant res
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Nothing -> case transToTHFString $ show id1 of
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Just s -> return $ stringToConstant s
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias " into a THF valide Constant.") nullRange
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiastransAssumpsId :: Id -> Int -> Result THFAs.Constant
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis TsogiastransAssumpsId id1 int = if int == 1 then transAssumpId id1 else
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias case transToTHFString $ show id1 of
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Just s -> return $ stringToConstant (s ++ show int)
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias " into a THF valide Constant.") nullRange
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasstringToConstant :: String -> THFAs.Constant
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasstringToConstant = A_Lower_Word . stringToLowerWord
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von SchroederstringToLowerWord :: String -> Token
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian MaederstringToLowerWord = mkSimpleId . \ s -> case s of
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder c : r -> if isLower c then s else 'x' : c : r
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von SchroederstringToVariable :: String -> String
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian MaederstringToVariable s = case s of
d9d546103be1753c4576502f40c296ce88eb69e3Christian Maeder c : r -> if isUpper c then s else let d = toUpper c in d : 'x' : d : r
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von SchroedertransVarId :: Id -> Result Token
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis TsogiastransVarId id1 = case transToTHFString $ show id1 of
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Just s -> return $ mkSimpleId $ stringToVariable s
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias Nothing -> fatal_error ("Unable to translate " ++ show id1 ++
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias " into a THF valide Variable.") nullRange
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiastransToTHFString :: String -> Maybe String
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian MaedertransToTHFString = transToTHFStringAux True
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian MaedertransToTHFStringAux :: Bool -> String -> Maybe String
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian MaedertransToTHFStringAux first s = case s of
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder "" -> Just ""
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder c : rc -> let
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder x = 'x' -- escape character
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder rest = transToTHFStringAux False rc
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias if isTHFChar c
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder then if first && isDigit c || c == x then fmap ([x, c] ++) rest else
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder fmap (c :) rest
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias else case Map.lookup c charMap of
b63d1c8a4e0ea8b68f91c1c1b35b1b735a290113Christian Maeder Just res -> fmap (res ++) rest
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Nothing -> Nothing
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasisTHFChar :: Char -> Bool
72204f862232e7e51b0207bba020c1d781fa7798Christian MaederisTHFChar c = isAlphaNum c && isAscii c || c == '_'
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasisLowerTHFChar :: Char -> Bool
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasisLowerTHFChar c = isLower c && isAscii c
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiaspreDefHCTypeIds :: Map.Map Id String
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiaspreDefHCTypeIds = Map.fromList
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder [ (logId, "hct" ++ show logId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (predTypeId, "hct" ++ show predTypeId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (unitTypeId, "hct" ++ show unitTypeId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (lazyTypeId, "hctLazy")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (arrowId FunArr, "hct__FunArr__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (arrowId PFunArr, "hct__PFunArr__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (arrowId ContFunArr, "hct__ContFunArr__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (arrowId PContFunArr, "hct__PContFunArr__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (productId 2 nullRange, "hct__X__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (productId 3 nullRange, "hct__X__X__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (productId 4 nullRange, "hct__X__X__X__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (productId 5 nullRange, "hct__X__X__X__X__") ]
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiaspreDefHCAssumpIds :: Map.Map Id String
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiaspreDefHCAssumpIds = Map.fromList
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder [ (botId, "hcc" ++ show botId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (defId, "hcc" ++ show defId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (notId, "hcc" ++ show notId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (negId, "hccNeg__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (whenElse, "hcc" ++ show whenElse)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (trueId, "hcc" ++ show trueId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (falseId, "hcc" ++ show falseId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (eqId, "hcc__Eq__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (exEq, "hcc__ExEq__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (resId, "hcc" ++ show resId)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (andId, "hcc__And__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (orId, "hcc__Or__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (eqvId, "hcc__Eqv__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (implId, "hcc__Impl__")
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder , (infixIf, "hcc" ++ show infixIf) ]
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmaybeElem :: Id -> Map.Map Id a -> Maybe a
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis TsogiasmaybeElem id1 m = helper id1 (Map.toList m)
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias helper :: Id -> [(Id, a)] -> Maybe a
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias helper _ [] = Nothing
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias helper id2 ((eid, ea) : r) =
96a6c2a58e8c534f983002f8d503f97ea1b4aa8dAlexis Tsogias if myEqId id2 eid then Just ea else helper id2 r
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmyEqId :: Id -> Id -> Bool
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiasmyEqId (Id t1 c1 _) (Id t2 c2 _) = (t1, c1) == (t2, c2)
658187feb755694eb5ff29561bda7109c22c743cAlexis Tsogias-- | a separate Map speeds up lookup
658187feb755694eb5ff29561bda7109c22c743cAlexis TsogiascharMap :: Map.Map Char String
72204f862232e7e51b0207bba020c1d781fa7798Christian MaedercharMap = Map.insert '\'' "Apostrophe"
72204f862232e7e51b0207bba020c1d781fa7798Christian Maeder -- this map is no longer injective