43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder{- HetCATS/CASL/SymbolParser.hs

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder $Id$

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Authors: Christian Maeder

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Year: 2002

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder may be needed for structured specs

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-}

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedermodule CASL.SymbolParser where

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder

f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederimport Common.Id

c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maederimport Common.Keywords

c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maederimport Common.Lexer

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport CASL.AS_Basic_CASL

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport Common.Lib.Parsec

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Common.Token

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport CASL.Formula

a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder-- ------------------------------------------------------------------------

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- symbol

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder-- ------------------------------------------------------------------------

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maedersymb :: GenParser Char st SYMB

4cb215739e9ab13447fa21162482ebe485b47455Christian Maedersymb = do i <- parseId

8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder do c <- colonST

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich t <- opOrPredType

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return (Qual_id i t [tokPos c])

74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder <|> return (Symb_id i)

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder

3e8b136f23ed57d40ee617f49bcac37830b58cabChristian MaederopOrPredType :: GenParser Char st TYPE

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian MaederopOrPredType =

3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder do (b, s, p) <- opSort

ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder if b then return (O_type (Partial_op_type [] s [p]))

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else do c <- crossT

e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder (ts, ps) <- sortId `separatedBy` crossT

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder fmap O_type (opFunSort (s:ts) (c:ps))

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder <|> return (P_type (Pred_type (s:ts) (map tokPos (c:ps))))

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder <|> fmap O_type (opFunSort [s] [])

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder <|> return (A_type s)

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder <|> fmap P_type predUnitType

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder

f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder-- ------------------------------------------------------------------------

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder-- symbol or map, symbKind

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder-- ------------------------------------------------------------------------

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder

1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedersymbMap :: GenParser Char st SYMB_OR_MAP

c3053d57f642ca507cdf79512e604437c4546cb9Christian MaedersymbMap = do s <- symb

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder do f <- pToken $ toKey mapsTo

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder t <- symb

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder return (Symb_map s t [tokPos f])

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder <|> return (Symb s)

05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder

05a62e84edac8c64de04f8349dee418598d216b9Christian MaedersymbKind :: GenParser Char st (SYMB_KIND, Token)

1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedersymbKind = try(

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder do q <- pluralKeyword opS

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder return (Ops_kind, q)

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder <|>

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder do q <- pluralKeyword predS

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder return (Preds_kind, q)

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder <|>

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder do q <- pluralKeyword sortS

d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder return (Sorts_kind, q)) <?> "kind"

23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder

48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder-- ------------------------------------------------------------------------

8cacad2a09782249243b80985f28e9387019fe40Christian Maeder-- symb-items

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- ------------------------------------------------------------------------

a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder

363939beade943a02b31004cea09dec34fa8a6d9Christian MaedersymbItemsList :: GenParser Char st SYMB_ITEMS_LIST

014dc30f64ec25e4790cca987d4d1e6635430510Christian MaedersymbItemsList = do (is, ps) <- symbItems `separatedBy` commaT

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich return (Symb_items_list is (map tokPos ps))

6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder

6aea82c63ba1d2efc0329bc784a14e521469ec20Christian MaedersymbItems :: GenParser Char st SYMB_ITEMS

431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedersymbItems = do s <- symb

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder return (Symb_items Implicit [s] [])

498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder <|>

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder do (k, p) <- symbKind

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder (is, ps) <- symbs

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder return (Symb_items k is (map tokPos (p:ps)))

6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedersymbs :: GenParser Char st ([SYMB], [Token])

61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maedersymbs = do s <- symb

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder do c <- commaT `followedWith` symb

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (is, ps) <- symbs

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return (s:is, c:ps)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder <|> return ([s], [])

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- ------------------------------------------------------------------------

9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- symb-map-items

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- ------------------------------------------------------------------------

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersymbMapItemsList :: GenParser Char st SYMB_MAP_ITEMS_LIST

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedersymbMapItemsList = do (is, ps) <- symbMapItems `separatedBy` commaT

ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder return (Symb_map_items_list is (map tokPos ps))

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedersymbMapItems :: GenParser Char st SYMB_MAP_ITEMS

a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaedersymbMapItems =

bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder do s <- symbMap

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder return (Symb_map_items Implicit [s] [])

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder <|>

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder do (k, p) <- symbKind

a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder (is, ps) <- symbMaps

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder return (Symb_map_items k is (map tokPos (p:ps)))

bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder

2d130d212db7208777ca896a7ecad619a8944971Christian MaedersymbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaedersymbMaps =

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder do s <- symbMap

2d130d212db7208777ca896a7ecad619a8944971Christian Maeder do c <- commaT `followedWith` symb

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (is, ps) <- symbMaps

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder return (s:is, c:ps)

6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder <|> return ([s], [])

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder

4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder

a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder