91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Common/SExpr.hs
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederDescription : S-Expressions as intermediate output format
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederCopyright : (c) E. Schulz, D. Dietrich, C. Maeder, DFKI 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederMaintainer : Christian.Maeder@dfki.de
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederStability : provisional
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederPortability : portable
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederS-Expressions for the translation from HasCASL, CASL and VSE to OMDoc
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder-}
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maedermodule Common.SExpr
9029484754c7b2037321e7cbd077580866845265Christian Maeder ( SExpr (..)
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder , prettySExpr
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder , idToSSymbol
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder , transToken
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder , transString
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder ) where
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maederimport Common.Doc
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport Common.Id
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maederimport Common.LibName
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport Common.ProofUtils
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maederimport qualified Data.Map as Map
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian Maederimport Data.Char
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maederdata SExpr = SSymbol String | SList [SExpr] deriving (Eq, Ord, Show)
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederprettySExpr :: SExpr -> Doc
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian MaederprettySExpr sexpr = case sexpr of
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder SSymbol s -> text s
91cee4f3b7fba73f6eb6c60209e36526a19e22e2Christian Maeder SList l -> parens . fsep $ map prettySExpr l
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder-- | transform an overloaded identifier
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederidToSSymbol :: Int -> Id -> SExpr
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaederidToSSymbol n i = SSymbol
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder $ transQualId i . (if n < 2 then id else showString "_O" . shows n) $ ""
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian Maeder
7c149ef873c83d57dba00d95f5b7e7bca72f0ac5Christian MaedertransQualId :: Id -> ShowS
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedertransQualId = transId . unQualName
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedertransId :: Id -> ShowS
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedertransId (Id ts cs _) =
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder showSepList id (showString . transToken) ts .
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if null cs then id else
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder showString "{" . showSepList (showString "-") transId cs
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder . showString "}"
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedertransToken :: Token -> String
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian MaedertransToken t = if isPlace t then "_2" else transString $ tokStr t
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian MaedertransStringAux :: String -> String
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian MaedertransStringAux = concatMap (\ c -> Map.findWithDefault [c] c cMap)
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian Maeder
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian MaedertransString :: String -> String
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian MaedertransString s = case s of
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian Maeder c : r | isDigit c -> "_D" ++ c : transStringAux r
a2feb624c01288b84ddb25bf9a5ddac509523ec0Christian Maeder _ -> transStringAux s
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedercMap :: Map.Map Char String
5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian MaedercMap = Map.map ('_' :) $ Map.insert '_' "1" charMap