SymbolParser.hs revision 61e38a4f194d3adc66646326c938eb9263a2f39b
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederModule : $Header$
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederDescription : Parser for symbols in translations and reductions
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2002-2006
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : Christian.Maeder@dfki.de
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : portable
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederParsing symbols for translations and reductions
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | parsing a possibly qualified identifier
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedersymb :: [String] -> GenParser Char st SYMB
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder do i <- parseId ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do c <- colonST
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder t <- opOrPredType ks
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (Qual_id i t $ tokPos c)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder <|> return (Symb_id i)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | parsing a type for an operation or a predicate
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederopOrPredType :: [String] -> GenParser Char st TYPE
64e1905404e5135e98a26d2ab4150b6764956576Christian MaederopOrPredType ks =
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do (b, s, p) <- opSort ks
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder if b then return (O_type (Op_type Partial [] s p))
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder else do c <- crossT
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder (ts, ps) <- sortId ks `separatedBy` crossT
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder fmap O_type (opFunSort ks (s:ts) (c:ps))
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> return (P_type $ Pred_type (s:ts)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder $ catRange $ c:ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> fmap O_type (opFunSort ks [s] [])
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder <|> return (A_type s)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> fmap P_type predUnitType
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | parsing one symbol or a mapping of one to second symbol
64e1905404e5135e98a26d2ab4150b6764956576Christian MaedersymbMap :: [String] -> GenParser Char st SYMB_OR_MAP
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do s <- symb ks
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do f <- pToken $ toKey mapsTo
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (Symb_map s t $ tokPos f)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder <|> return (Symb s)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- | parse a kind keyword
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbKind :: GenParser Char st (SYMB_KIND, Token)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbKind = try(
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do q <- pluralKeyword opS
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder return (Ops_kind, q)
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do q <- pluralKeyword predS
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (Preds_kind, q)
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder do q <- pluralKeyword sortS
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (Sorts_kind, q)) <?> "kind"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | parse a possible kinded list of comma separated symbols
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbItems :: [String] -> GenParser Char st SYMB_ITEMS
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbItems ks =
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder do (is, ps) <- symbs ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Symb_items Implicit is $ catRange ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do (k, p) <- symbKind
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (is, ps) <- symbs ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Symb_items k is $ catRange $ p:ps)
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder-- | parse a comma separated list of symbols
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedersymbs :: [String] -> GenParser Char st ([SYMB], [Token])
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do s <- symb ks
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder do c <- commaT `followedWith` symb ks
62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder (is, ps) <- symbs ks
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (s:is, c:ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> return ([s], [])
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | parse a possible kinded list of symbol mappings
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbMapItems :: [String] -> GenParser Char st SYMB_MAP_ITEMS
67869d63d1725c79e4c07b51acd466a31932b275Christian MaedersymbMapItems ks =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do s <- symbMap ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Symb_map_items Implicit [s] nullRange)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do (k, p) <- symbKind
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (is, ps) <- symbMaps ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder return (Symb_map_items k is $ catRange $ p:ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | parse a comma separated list of symbol mappings
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedersymbMaps :: [String] -> GenParser Char st ([SYMB_OR_MAP], [Token])
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do s <- symbMap ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do c <- commaT `followedWith` symb ks
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (is, ps) <- symbMaps ks
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder return (s:is, c:ps)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder <|> return ([s], [])