55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaModule : $Header$

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaDescription : create legal THF mixfix identifier

b43458b4d81f7451112cecbd757f3a05216e7088Kristina SojakovaCopyright : (c) A. Tsogias, DFKI Bremen 2011

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaLicense : GPLv2 or higher, see LICENSE.txt

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Alexis.Tsogias@dfki.de

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaStability : provisional

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaPortability : portable

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovatranslate 'Id' to THF Constant

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-}

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovamodule THF.Translate where

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Id

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport Common.Result

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport qualified Common.ProofUtils as CM (charMap)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakovaimport HasCASL.Builtin

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakovaimport HasCASL.AsUtils

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatovimport THF.As as THFAs

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Data.Char

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Data.Map as Map

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina SojakovamkTypesName :: THFAs.Constant -> THFAs.Name

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovamkTypesName c = case c of

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova $ mkSimpleId ("type_" ++ show w)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova $ mkSimpleId ("type_" ++ show s)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

b43458b4d81f7451112cecbd757f3a05216e7088Kristina SojakovamkConstsName :: THFAs.Constant -> THFAs.Name

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovamkConstsName c = case c of

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova $ mkSimpleId ("const_" ++ show w)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova $ mkSimpleId ("const_" ++ show s)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovamkDefName :: THFAs.Constant -> THFAs.Name

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovamkDefName c = case c of

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova A_Lower_Word w -> N_Atomic_Word $ A_Lower_Word

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova $ mkSimpleId ("def_" ++ show w)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova A_Single_Quoted s -> N_Atomic_Word $ A_Single_Quoted

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova $ mkSimpleId ("def_" ++ show s)

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina SojakovatransTypeId :: Id -> Result THFAs.Constant

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina SojakovatransTypeId id1 = case maybeElem id1 preDefHCTypeIds of

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova Just res -> return $ stringToConstant res

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova Nothing -> case transToTHFString $ "x_" ++ show id1 of

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova Just s -> return $ stringToConstant s

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder Nothing -> fatal_error ("Unable to translate " ++ show id1 ++

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova " into a THF valide Constant.") nullRange

b43458b4d81f7451112cecbd757f3a05216e7088Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovatransAssumpId :: Id -> Result THFAs.Constant

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovatransAssumpId id1 = case maybeElem id1 preDefHCAssumpIds of

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Just res -> return $ stringToConstant res

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Nothing -> case transToTHFString $ show id1 of

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Just s -> return $ stringToConstant s

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Nothing -> fatal_error ("Unable to translate " ++ show id1 ++

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova " into a THF valide Constant.") nullRange

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovatransAssumpsId :: Id -> Int -> Result THFAs.Constant

abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovatransAssumpsId id1 int = if int == 1 then transAssumpId id1 else

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova case transToTHFString $ show id1 of

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova Just s -> return $ stringToConstant (s ++ show int)

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova Nothing -> fatal_error ("Unable to translate " ++ show id1 ++

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova " into a THF valide Constant.") nullRange

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovastringToConstant :: String -> THFAs.Constant

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovastringToConstant = A_Lower_Word . stringToLowerWord

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovastringToLowerWord :: String -> Token

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovastringToLowerWord = mkSimpleId . \ s -> case s of

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova c : r -> if isLower c then s else 'x' : c : r

ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova "" -> ""

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder

80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian MaederstringToVariable :: String -> String

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaederstringToVariable s = case s of

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova c : r -> if isUpper c then s else toUpper c : 'x' : r

168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova "" -> ""

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maeder

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedertransVarId :: Id -> Result Token

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina SojakovatransVarId id1 = case transToTHFString $ show id1 of

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova Just s -> return $ mkSimpleId $ stringToVariable s

d2786879b4733fd4886a5b654f7c6de1d234f638Kristina Sojakova Nothing -> fatal_error ("Unable to translate " ++ show id1 ++

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova " into a THF valide Variable.") nullRange

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovatransToTHFString :: String -> Maybe String

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedertransToTHFString = transToTHFStringAux True

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovatransToTHFStringAux :: Bool -> String -> Maybe String

a669e4685b32ff5ca1bca785eacc5e30a545b010Christian MaedertransToTHFStringAux first s = case s of

b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova "" -> Just ""

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova c : rc -> let

abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova x = 'x' -- escape character

168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova rest = transToTHFStringAux False rc

80d2ec8f37d5ddec13c14b17b1bab01e9c94630aChristian Maeder in

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova if isTHFChar c

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova then if first && isDigit c || c == x then fmap ([x, c] ++) rest else

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova fmap (c :) rest

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova else case Map.lookup c charMap of

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Just res -> fmap (res ++) rest

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Nothing -> Nothing

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaisTHFChar :: Char -> Bool

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaisTHFChar c = isAlphaNum c && isAscii c || c == '_'

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovaisLowerTHFChar :: Char -> Bool

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovaisLowerTHFChar c = isLower c && isAscii c

e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovapreDefHCTypeIds :: Map.Map Id String

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovapreDefHCTypeIds = Map.fromList

5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova [ (logId, "hct" ++ show logId)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , (predTypeId, "hct" ++ show predTypeId)

2cb6df4f21c52732336579a79f7e5d28299b3500Iulia Ignatov , (unitTypeId, "hct" ++ show unitTypeId)

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov , (lazyTypeId, "hctLazy")

b2e01ef1b5d4c7a62260eb792291e8e1b10e545bIulia Ignatov , (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.insert '\'' "Apostrophe"

. Map.insert '.' "Dot"

$ Map.map stringToVariable CM.charMap

-- this map is no longer injective