hets/CspCASL/SymbItems.hs

	SymbItems.hs revision ab0274ab68a174d3e92235b4c4ca865c03901583


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
6332N/A{- |
6332N/AModule      :  $Header$
6332N/ADescription :  syntactic csp-casl symbols
6332N/ACopyright   :  (c) Christian Maeder, DFKI GmbH 2011
6332N/ALicense     :  GPLv2 or higher, see LICENSE.txt
6332N/AMaintainer  :  Christian.Maeder@dfki.de
6332N/AStability   :  provisional
6332N/APortability :  portable
6332N/A
6332N/A-}
6332N/A
6332N/Amodule CspCASL.SymbItems where
6332N/A
6332N/Aimport CspCASL.AS_CspCASL_Process
6332N/Aimport CspCASL.CspCASL_Keywords
6332N/Aimport CspCASL.Print_CspCASL
6332N/A
6332N/Aimport CASL.AS_Basic_CASL
6332N/Aimport CASL.SymbolParser
6332N/Aimport CASL.ToDoc
6332N/A
import Common.Doc hiding (braces)
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token

import Text.ParserCombinators.Parsec

import Control.Monad

import qualified Data.Set as Set

data CspSymbItems = CspSymbItems CspSymbKind [CspSymb]
  deriving (Show, Eq)

data CspSymbMapItems = CspSymbMapItems CspSymbKind [CspSymbMap]
  deriving (Show, Eq)

data CspSymbKind = CaslKind SYMB_KIND | ProcessKind | ChannelKind
  deriving (Show, Eq, Ord)

data CspSymb = CspSymb Id (Maybe CspType)
  deriving (Show, Eq)

-- for channels with sorts we may re-use A_type that is ambiguous
data CspType = CaslType TYPE | ProcType ProcProfile
  deriving (Show, Eq)

data CspSymbMap = CspSymbMap CspSymb (Maybe CspSymb)
  deriving (Show, Eq)

pluralCspSympKind :: CspSymbKind -> [a] -> Doc
pluralCspSympKind k l = case k of
    CaslKind c -> case c of
      Implicit -> empty
      _ -> keyword $ pluralS_symb_list c l
    ProcessKind -> keyword processS
    ChannelKind -> keyword $ channelS ++ appendS l

instance Pretty CspSymbKind where
  pretty k = pluralCspSympKind k [()]

instance Pretty CspType where
  pretty t = case t of
    CaslType c -> colon <> pretty c
    ProcType p -> printProcProfile p

instance Pretty CspSymb where
  pretty (CspSymb i ms) = pretty i <+> pretty ms

instance Pretty CspSymbMap where
  pretty (CspSymbMap s ms) = pretty s <+> case ms of
    Nothing -> empty
    Just t -> mapsto <+> pretty t

instance Pretty CspSymbItems where
  pretty (CspSymbItems k l) = pluralCspSympKind k l <+> ppWithCommas l

instance Pretty CspSymbMapItems where
  pretty (CspSymbMapItems k l) = pluralCspSympKind k l <+> ppWithCommas l

parseCspId :: GenParser Char st Id
parseCspId = parseId csp_casl_keywords

cspSortId :: GenParser Char st SORT
cspSortId = sortId csp_casl_keywords

plainColon :: GenParser Char st ()
plainColon = forget $ pToken $ toKey colonS

commType :: GenParser Char st CommType
commType = do
  s <- cspSortId
  do
    plainColon
    r <- cspSortId
    if isSimpleId s
      then return $ CommTypeChan $ TypedChanName (idToSimpleId s) r
      else unexpected $ "sort " ++ show s
   <|> return (CommTypeSort s)

bracedList :: GenParser Char st [CommType]
bracedList = braces $ commaSep1 commType

commAlpha :: GenParser Char st CommAlpha
commAlpha = fmap Set.fromList $ single commType <|> bracedList

-- | parsing a possibly qualified identifier
cspSymb :: GenParser Char st CspSymb
cspSymb =
    do i <- parseCspId
       do
         _ <- colonST
         t <- fmap CaslType (opOrPredType csp_casl_keywords) <|>
            fmap (ProcType . ProcProfile []) commAlpha
         return $ CspSymb i $ Just t
        <|> do
         ts <- between oParenT cParenT $ commaSep1 cspSortId
         plainColon
         cs <- commAlpha
         return $ CspSymb i $ Just $ ProcType $ ProcProfile ts cs
        <|> return (CspSymb i Nothing)

-- | parsing one symbol or a mapping of one to second symbol
cspSymbMap :: GenParser Char st CspSymbMap
cspSymbMap = liftM2 CspSymbMap cspSymb $ optionMaybe
  $ pToken (toKey mapsTo) >> cspSymb

-- | parse a kind keyword
cspSymbKind :: GenParser Char st CspSymbKind
cspSymbKind =
  fmap (const ChannelKind) (pluralKeyword channelS)
  <|> fmap (const ProcessKind) (pToken $ toKey processS)
  <|> fmap (CaslKind . fst) symbKind

-- | parse a comma separated list of symbols
cspSymbs :: GenParser Char st [CspSymb]
cspSymbs =
    do s <- cspSymb
       do
         _ <- commaT `followedWith` parseCspId
         is <- cspSymbs
         return $ s : is
        <|> return [s]

{- | Parse a possible kinded list of comma separated CspCASL symbols.
     The argument is a list of keywords to avoid as identifiers. -}
cspSymbItems :: GenParser Char st CspSymbItems
cspSymbItems = fmap (CspSymbItems $ CaslKind Implicit) cspSymbs <|> do
    k <- cspSymbKind
    fmap (CspSymbItems k) cspSymbs

-- | parse a comma separated list of symbols
cspSymbMaps :: GenParser Char st [CspSymbMap]
cspSymbMaps =
    do s <- cspSymbMap
       do
         _ <- commaT `followedWith` parseCspId
         is <- cspSymbMaps
         return $ s : is
        <|> return [s]

-- | parse a possible kinded list of CspCASL symbol mappings
cspSymbMapItems :: GenParser Char st CspSymbMapItems
cspSymbMapItems = fmap (CspSymbMapItems $ CaslKind Implicit) cspSymbMaps
  <|> do
    k <- cspSymbKind
    fmap (CspSymbMapItems k) cspSymbMaps