7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder HasCASL symbols for structured specs

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maedermodule HasCASL.Symbol where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Id

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Keywords

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Lexer

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.AS_Annotation

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederimport Common.AnnoState

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Lib.Parsec

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport HasCASL.HToken

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport HasCASL.ParseTerm

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.As

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport HasCASL.PrintAs

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.PrettyPrint

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.Lib.Pretty as PP

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Common.PPUtils

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Data.Dynamic

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- * symbol data types

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | symbols

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdata SymbItems = SymbItems SymbKind [Symb] [Annotation] [Pos]

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder -- pos: kind, commas

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder deriving (Show, Eq, Typeable)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | mapped symbols

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata SymbMapItems = SymbMapItems SymbKind [SymbOrMap] [Annotation] [Pos]

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder -- pos: kind commas

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder deriving (Show, Eq, Typeable)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | kind of symbols

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederdata SymbKind = Implicit | SK_type | SK_op | SK_class

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder deriving (Show, Eq, Ord)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | type annotated symbols

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederdata Symb = Symb Id (Maybe SymbType) [Pos]

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -- pos: colon (or empty)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder deriving (Show, Eq)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | type for symbols

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederdata SymbType = SymbType TypeScheme

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder deriving (Show, Eq)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- | mapped symbol

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederdata SymbOrMap = SymbOrMap Symb (Maybe Symb) [Pos]

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -- pos: "|->" (or empty)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder deriving (Show, Eq)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- * parsers for symbols

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | parse a (typed) symbol

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedersymb :: AParser Symb

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maedersymb = do i <- uninstOpId

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder do c <- colT

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder t <- typeScheme

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder return (Symb i (Just $ SymbType t) [tokPos c])

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder <|>

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder do c <- qColonT

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder t <- parseType

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder return (Symb i (Just $ SymbType $ simpleTypeScheme $

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder LazyType t [tokPos c]) [tokPos c])

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder <|> return (Symb i Nothing [])

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | parse a mapped symbol

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersymbMap :: AParser SymbOrMap

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersymbMap = do s <- symb

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder do f <- asKey mapsTo

7feac39f792f587cffdc8b63b0e7c5a7d2de292eChristian Maeder t <- symb

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SymbOrMap s (Just t) [tokPos f])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|> return (SymbOrMap s Nothing [])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | parse kind of symbols

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbKind :: AParser (SymbKind, Token)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbKind = try(

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do q <- pluralKeyword opS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SK_op, q)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder do q <- pluralKeyword functS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SK_op, q)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do q <- pluralKeyword predS

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder return (SK_op, q)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do q <- pluralKeyword typeS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SK_type, q)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do q <- pluralKeyword sortS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SK_type, q)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do q <- asKey (classS ++ "es") <|> asKey classS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SK_class, q))

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <?> "kind"

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | parse symbol items

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbItems :: AParser SymbItems

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbItems = do s <- symb

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SymbItems Implicit [s] [] [])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do (k, p) <- symbKind

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder (is, ps) <- symbs

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder return (SymbItems k is [] (map tokPos (p:ps)))

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedersymbs :: AParser ([Symb], [Token])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedersymbs = do s <- symb

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do c <- anComma `followedWith` symb

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder (is, ps) <- symbs

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (s:is, c:ps)

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder <|> return ([s], [])

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder-- | parse symbol mappings

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersymbMapItems :: AParser SymbMapItems

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian MaedersymbMapItems =

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder do s <- symbMap

94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder return (SymbMapItems Implicit [s] [] [])

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do (k, p) <- symbKind

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder (is, ps) <- symbMaps

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return (SymbMapItems k is [] (map tokPos (p:ps)))

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedersymbMaps :: AParser ([SymbOrMap], [Token])

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedersymbMaps =

do s <- symbMap

do c <- anComma `followedWith` symb

(is, ps) <- symbMaps

return (s:is, c:ps)

<|> return ([s], [])

-- pretty printing

-- | print symbol kind

printSK :: SymbKind -> Doc

printSK k =

case k of Implicit -> empty

_ -> ptext (drop 3 $ show k) <> PP.space

instance PrettyPrint Symb where

printText0 ga (Symb i mt _) =

printText0 ga i <> (case mt of Nothing -> empty

Just (SymbType t) ->

empty <+> colon <+>

printText0 ga t)

instance PrettyPrint SymbItems where

printText0 ga (SymbItems k syms _ _) =

printSK k <> commaT_text ga syms

instance PrettyPrint SymbOrMap where

printText0 ga (SymbOrMap s mt _) =

printText0 ga s <> (case mt of Nothing -> empty

Just t ->

empty <+> ptext mapsTo <+>

printText0 ga t)

instance PrettyPrint SymbMapItems where

printText0 ga (SymbMapItems k syms _ _) =

printSK k <> commaT_text ga syms