Symbol.hs revision fd896e2068ad7e50aed66ac18c3720ea7ff2619f
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Christian Maeder and Uni Bremen 2003
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicence : All rights reserved.
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hets@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : experimental
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach HasCASL symbols for structured specs
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder-- * symbol data types
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettdata SymbItems = SymbItems SymbKind [Symb] [Annotation] [Pos]
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett -- pos: kind, commas
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving (Show,Eq)
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett-- | mapped symbols
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederdata SymbMapItems = SymbMapItems SymbKind [SymbOrMap] [Annotation] [Pos]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- pos: kind commas
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving (Show,Eq)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | kind of symbols
842ae753ab848a8508c4832ab64296b929167a97Christian Maederdata SymbKind = Implicit | SK_sort | SK_type | SK_op | SK_pred | SK_class
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder deriving (Show, Eq, Ord)
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett-- | type annotated symbols
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillydata Symb = Symb Id (Maybe SymbType) [Pos]
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -- pos: colon (or empty)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly deriving (Show,Eq)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | type for symbols
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettdata SymbType = SymbType TypeScheme
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder deriving (Show,Eq)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | mapped symbol
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederdata SymbOrMap = SymbOrMap Symb (Maybe Symb) [Pos]
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder -- pos: "|->" (or empty)
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder deriving (Show,Eq)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- * parsers for symbols
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | parse a (typed) symbol
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillysymb :: AParser Symb
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillysymb = do i <- uninstOpId
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly t <- typeScheme
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder return (Symb i (Just $ SymbType t) [tokPos c])
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder do c <- qColonT
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder t <- parseType
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder return (Symb i (Just $ SymbType $ simpleTypeScheme $
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder LazyType t [tokPos c]) [tokPos c])
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett <|> return (Symb i Nothing [])
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- | parse a mapped symbol
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettsymbMap :: AParser SymbOrMap
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy GimblettsymbMap = do s <- symb
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett do f <- asKey mapsTo
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett return (SymbOrMap s (Just t) [tokPos f])
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <|> return (SymbOrMap s Nothing [])
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | parse kind of symbols
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettsymbKind :: AParser (SymbKind, Token)
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettsymbKind = try(
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett do q <- pluralKeyword opS
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (SK_op, q)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do q <- pluralKeyword predS
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (SK_pred, q)
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett do q <- pluralKeyword typeS
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return (SK_type, q)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do q <- pluralKeyword sortS
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return (SK_sort, q)
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett do q <- asKey (classS ++ "es") <|> asKey classS
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett return (SK_class, q))
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder-- | parse symbol items
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedersymbItems :: AParser SymbItems
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettsymbItems = do s <- symb
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return (SymbItems Implicit [s] [] [])
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett do (k, p) <- symbKind
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (is, ps) <- symbs
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett return (SymbItems k is [] (map tokPos (p:ps)))
842ae753ab848a8508c4832ab64296b929167a97Christian Maedersymbs :: AParser ([Symb], [Token])
842ae753ab848a8508c4832ab64296b929167a97Christian Maedersymbs = do s <- symb
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder do c <- anComma `followedWith` symb
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (is, ps) <- symbs
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (s:is, c:ps)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <|> return ([s], [])
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | parse symbol mappings
842ae753ab848a8508c4832ab64296b929167a97Christian MaedersymbMapItems :: AParser SymbMapItems
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettsymbMapItems =
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do s <- symbMap
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach return (SymbMapItems Implicit [s] [] [])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do (k, p) <- symbKind
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (is, ps) <- symbMaps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (SymbMapItems k is [] (map tokPos (p:ps)))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillysymbMaps :: AParser ([SymbOrMap], [Token])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do s <- symbMap
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett do c <- anComma `followedWith` symb
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (is, ps) <- symbMaps
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett return (s:is, c:ps)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett <|> return ([s], [])
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- pretty printing
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | print symbol kind
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettprintSK :: SymbKind -> Doc
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case k of Implicit -> empty
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> ptext (drop 3 $ show k) <> PP.space
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrettyPrint Symb where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga (Symb i mt _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga i <> (case mt of Nothing -> empty
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just (SymbType t) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly empty <+> colon <+>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga t)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrettyPrint SymbItems where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga (SymbItems k syms _ _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printSK k <> commaT_text ga syms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance PrettyPrint SymbOrMap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga (SymbOrMap s mt _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printText0 ga s <> (case mt of Nothing -> empty
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder empty <+> ptext mapsTo <+>
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder printText0 ga t)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettinstance PrettyPrint SymbMapItems where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett printText0 ga (SymbMapItems k syms _ _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly printSK k <> commaT_text ga syms