Ast.hs revision 03b3c9dc9de5716538a9b04ae9bd8f36e22660e3
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
d657c51f14601d0235434ffb78cf6ac0f27cc83cLennart Poetteringmodule Ast where
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sieversimport Parsec
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sieversimport ParseType
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sieversimport ParseTerm
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sieverstype SortId = Id
71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sieverstype OpId = Id
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay Sieverstype VarId = Id
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieversbarChar = '|'
4196a3ead3cfb823670d225eefcb3e60e34c7d95Kay SieverssortStr = "sort"
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringtype Axiom = Term
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata BasicItems = SigItems SigItems
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | FreeDatatypeItems [DatatypeDecl]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | SortGen [SigItems]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | VarItems [VarDecl]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | LocalVarDecl [VarDecl] [Axiom]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | Axioms [Axiom]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata SigItems = SortItems Keyword [SortItem]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | OpItems Keyword [OpItem]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | DatatypeItems [DatatypeDecl]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering deriving (Show)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata SortItem = SubsortDecl [SortId] (Maybe Type)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | IsoDecl [SortId]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | SubsortDefn SortId VarId Type Term
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | AnnotatedSortItem SortItem [Anno]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringshowSortItem (SubsortDecl l Nothing) = showCommaList l
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringshowSortItem (SubsortDecl l (Just t)) =
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showCommaList l . showSignStr lessStr . showSign t
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringshowSortItem (IsoDecl l) =
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showSepList (showSignStr equalStr) showSign l
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringshowSortItem (AnnotatedSortItem s _) = shows s
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringshowSortItem (SubsortDefn s _ _ e) =
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering shows s. showSignStr equalStr . shows e
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringinstance Show SortItem where
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showsPrec _ = showSortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringassocStr = "assoc"
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringcommStr = "comm"
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringidemStr = "idem"
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringunitStr = "unit"
cd14eda3212f9109c98a77cd5fee4168010d80daLennart Poetteringdata OpAttr = AssocOpAttr | CommOpAttr | IdemOpAttr | UnitOpAttr Term
cd14eda3212f9109c98a77cd5fee4168010d80daLennart Poetteringinstance Show OpAttr where
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showsPrec _ AssocOpAttr = showString assocStr
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showsPrec _ CommOpAttr = showString commStr
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showsPrec _ IdemOpAttr = showString idemStr
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showsPrec _ (UnitOpAttr t) = showSignStr unitStr . shows t
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering showList = showString . concat . map (\a -> ',' : show a)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata OpItem = OpItem [OpId] Type [OpAttr] (Maybe Term) [Anno]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering deriving (Show)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata Component = Component Decl deriving (Show)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering-- full function type (in Decl) of constructor
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata Alternative = Construct Decl [Component]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering | Subsorts [SortId]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering deriving (Show)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringdata DatatypeDecl = DatatypeDecl SortId [Alternative] deriving (Show)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringclass Annotatable a where
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering annotate :: a -> [Anno] -> a
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringinstance Annotatable OpItem where
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering annotate (OpItem os t as def _) l = OpItem os t as def l
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringinstance Annotatable SortItem where
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering annotate (AnnotatedSortItem s _) l = AnnotatedSortItem s l
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering annotate s l = AnnotatedSortItem s l
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringcommaSortDecl :: SortId -> Parser SortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringcommaSortDecl s = do { l <- comma >> (sortId `sepBy1` comma)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; let l' = s : l in
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering subSortDecl l'
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering <|> return (SubsortDecl l' Nothing)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringisoDecl :: SortId -> Parser SortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringisoDecl s = do { e <- equal
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; subSortDefn s
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering (do { l <- sortId `sepBy1` equal
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; return (IsoDecl (s:l))
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsubSortDefn :: SortId -> Parser SortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsubSortDefn s = do { o <- oBrace
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; t <- colon >>= funType
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; e <- parseTerm
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; let f = Binding SupersortVar [Decl (Symb [v] t) o []] e
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering in return (SubsortDefn s v t f)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsubSortDecl :: [SortId] -> Parser SortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsubSortDecl l = do { s <- lessSign >>= funType
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; return (SubsortDecl l (Just s))
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsortItem :: Parser SortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsortItem = do { s <- sortId
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; subSortDecl [s]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering commaSortDecl s
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering return (SubsortDecl [s] Nothing)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringsortItems = do { key <- pluralKeyword sortStr
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; l <- itemAux sortItem
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; return (SortItems key l)
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringpluralKeyword s = makeToken (string s <++> option "" (string "s"))
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringoptSemi = bind (\ x y -> (x, y)) (option Nothing (fmap Just semi)) ann
71449cafa1f3aecad6fc755ae5e571eddf0bbd02Kay Sieversdot = toKey [dotChar] <|> toKey middleDotStr <?> "dot"
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringbar = toKey [barChar]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poetteringequal = toKey equalStr
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringisStartKeyword s = s `elem` [dotChar]:middleDotStr:casl_reserved_words
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringlookAheadItemKeyword :: a -> Parser a
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringlookAheadItemKeyword a =
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering do { c <- lookAhead (many (oneOf (['0'..'9'] ++ "'" ++ caslLetters))
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering <|> many (oneOf signChars))
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; if isStartKeyword c then return a else unexpected c
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringitemAux :: Annotatable a => (Parser a) -> Parser [a]
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart PoetteringitemAux itemParser =
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering do { i <- itemParser
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; (m, an) <- optSemi
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; let i' = if null an then i else annotate i an
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering in case m of Nothing -> return [i']
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering Just _ -> try (lookAheadItemKeyword [i'])
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering do { l <- itemAux itemParser
04e91da2cfdfb7153218be7a77c885f1c23d3fd7Lennart Poettering ; return (i':l)