root/trunk/HasCASL/ParseItem.hs @ 11877

Revision 11877, 12.3 kB (checked in by maeder, 5 months ago)

disallowed explicit pseudo type notation following := (assign)

  • Property svn:eol-style set to native
  • Property svn:keywords set to Author Date Id Revision
Line 
1{- |
2Module      :  $Header$
3Description :  parser for HasCASL basic Items
4Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
5License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
6
7Maintainer  :  Christian.Maeder@dfki.de
8Stability   :  provisional
9Portability :  portable
10
11parser for HasCASL basic Items
12-}
13
14module HasCASL.ParseItem (basicItems, basicSpec) where
15
16import Text.ParserCombinators.Parsec
17
18import Common.AS_Annotation
19import Common.AnnoState
20import Common.Id
21import Common.Keywords
22import Common.Lexer
23import Common.Token
24
25import HasCASL.HToken
26import HasCASL.As
27import HasCASL.AsUtils
28import HasCASL.ParseTerm
29
30-- * adapted item list parser (using 'itemAux')
31
32hasCaslItemList :: String -> AParser st b
33                -> ([Annoted b] -> Range -> a) -> AParser st a
34hasCaslItemList kw ip constr = do
35    p <- pluralKeyword kw
36    auxItemList hasCaslStartKeywords [p] ip constr
37
38hasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
39               -> AParser st a
40hasCaslItemAux ps = auxItemList hasCaslStartKeywords ps
41
42-- * parsing type items
43
44commaTypeDecl :: TypePattern -> AParser st TypeItem
45commaTypeDecl s = do
46    c <- anComma
47    (is, cs) <- typePattern `separatedBy` anComma
48    let l = s : is
49        p = c : cs
50    subTypeDecl (l, p) <|> kindedTypeDecl (l, p)
51        <|> return (TypeDecl l universe $ catRange p)
52
53kindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
54kindedTypeDecl (l, p) = do
55    t <- colT
56    s <- kind
57    let d = TypeDecl l s $ catRange $ p ++ [t]
58    case l of
59      [hd] -> pseudoTypeDef hd (Just s) [t] <|> dataDef hd s [t] <|> return d
60      _ -> return d
61
62isoDecl :: TypePattern -> AParser st TypeItem
63isoDecl s = do
64    e <- equalT
65    subTypeDefn (s, e) <|> do
66        (l, p) <- typePattern `separatedBy` equalT
67        return $ IsoDecl (s : l) $ catRange $ e : p
68
69vars :: AParser st Vars
70vars = fmap Var var <|> do
71    o <- oParenT
72    (vs, ps) <- vars `separatedBy` anComma
73    c <- cParenT
74    return $ VarTuple vs $ toRange o ps c
75
76subTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
77subTypeDefn (s, e) = do
78    a <- annos
79    o <- oBraceT << addAnnos
80    v <- vars
81    c <- colT
82    t <- parseType
83    d <- dotT -- or bar
84    f <- term
85    a2 <- annos
86    p <- cBraceT
87    let qs = toRange e [o,c,d] p
88    return $ SubtypeDefn s v t (Annoted f qs a a2) qs
89
90subTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
91subTypeDecl (l, p) = do
92    t <- lessT
93    s <- parseType
94    return $ SubtypeDecl l s $ catRange $ p ++ [t]
95
96sortItem :: AParser st TypeItem
97sortItem = do
98    s <- typePattern
99    subTypeDecl ([s],[])
100        <|> kindedTypeDecl ([s],[])
101        <|> commaTypeDecl s
102        <|> isoDecl s
103        <|> return (TypeDecl [s] universe nullRange)
104
105sortItems :: AParser st SigItems
106sortItems = hasCaslItemList sortS sortItem (TypeItems Plain)
107
108typeItem :: AParser st TypeItem
109typeItem = do
110    s <- typePattern;
111    subTypeDecl ([s],[])
112        <|> dataDef s universe []
113        <|> pseudoTypeDef s Nothing []
114        <|> kindedTypeDecl ([s],[])
115        <|> commaTypeDecl s
116        <|> isoDecl s
117        <|> return (TypeDecl [s] universe nullRange)
118
119typeItemList :: [Token] -> Instance -> AParser st SigItems
120typeItemList ps k = hasCaslItemAux ps typeItem $ TypeItems k
121
122typeItems :: AParser st SigItems
123typeItems = do
124    p <- pluralKeyword typeS
125    do  q <- pluralKeyword instanceS
126        typeItemList [p, q] Instance
127      <|> typeItemList [p] Plain
128
129pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
130pseudoTypeDef t k l = do
131    c <- asKey assignS
132    p <- parseType
133    return $ AliasType t k (simpleTypeScheme p) $ catRange $ l ++ [c]
134
135-- * parsing datatypes
136
137component :: AParser st [Component]
138component = try (do
139    (is, cs) <- opId `separatedBy` anComma
140    compType is cs) <|> do
141    t <- parseType
142    return [NoSelector t]
143
144concatFst :: [[a]] -> Range -> ([a], Range)
145concatFst as ps = (concat as, ps)
146
147tupleComponent :: AParser st ([Component], Range)
148tupleComponent = bracketParser component oParenT cParenT anSemi concatFst
149
150altComponent :: AParser st ([Component], Range)
151altComponent = tupleComponent <|> do
152    i <- typeVar
153    let t = case i of
154          Id [tok] [] _ -> TypeToken tok
155          _ -> error "altComponent"
156    return ([NoSelector t], nullRange)
157
158compType :: [Id] -> [Token] -> AParser st [Component]
159compType is cs = do
160    c <- colonST
161    t <- parseType
162    let makeComps l1 l2 = case (l1, l2) of
163          ([a], [b]) -> [Selector a Total t Other $ tokPos b]
164          (a : r, b : s) -> Selector a Total t Comma (tokPos b) : makeComps r s
165          _ -> error "makeComps: empty selector list"
166    return $ makeComps is $ cs ++ [c]
167
168alternative :: AParser st Alternative
169alternative = do
170    s <- pluralKeyword sortS <|> pluralKeyword typeS
171    (ts, cs) <- parseType `separatedBy` anComma
172    return $ Subtype ts $ catRange $ s : cs
173  <|> do
174    i <- hconsId
175    cps <- many altComponent
176    let ps = concatMapRange snd cps
177        cs = map fst cps
178    do  q <- quMarkT
179        return $ Constructor i cs Partial $ appRange ps $ tokPos q
180      <|> return (Constructor i cs Total ps)
181
182dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
183dataDef t k l = do
184    c <- asKey defnS
185    a <- annos
186    let aAlternative = bind (\ i an -> Annoted i nullRange [] an)
187          alternative annos
188    (Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT
189    let aa = Annoted v nullRange a b : as
190        qs = catRange $ l ++ c : ps
191    do  d <- asKey derivingS
192        (cs, cps) <- classId `separatedBy` anComma
193        return $ Datatype $ DatatypeDecl t k aa cs
194                    $ appRange qs $ appRange (tokPos d) $ catRange cps
195      <|> return (Datatype (DatatypeDecl t k aa [] qs))
196
197dataItem :: AParser st DatatypeDecl
198dataItem = do
199     t <- typePattern
200     do  c <- colT
201         k <- kind
202         Datatype d <- dataDef t k [c]
203         return d
204       <|> do
205         Datatype d <- dataDef t universe []
206         return d
207
208dataItems :: AParser st BasicItem
209dataItems = hasCaslItemList typeS dataItem FreeDatatype
210
211-- * parse class items
212
213classDecl :: AParser st ClassDecl
214classDecl = do
215    (is, cs) <- classId `separatedBy` anComma
216    (ps, k) <- option ([], universe) $ bind  (,) (single lessT) kind
217    return $ ClassDecl is k $ catRange $ cs ++ ps
218
219classItem :: AParser st ClassItem
220classItem = do
221    c <- classDecl
222    do  o <- oBraceT
223        is <- annosParser basicItems
224        p <- cBraceT
225        return $ ClassItem c is $ toRange o [] p
226      <|> return (ClassItem c [] nullRange)
227
228classItemList :: [Token] -> Instance -> AParser st BasicItem
229classItemList ps k = hasCaslItemAux ps classItem $ ClassItems k
230
231classItems :: AParser st BasicItem
232classItems = do
233    p <- asKey (classS ++ "es") <|> asKey classS <?> classS
234    do  q <- pluralKeyword instanceS
235        classItemList [p, q] Instance
236      <|> classItemList [p] Plain
237
238-- * parse op items
239
240opAttr :: AParser st OpAttr
241opAttr = let l = [Assoc, Comm, Idem] in
242    choice (map ( \ a -> do
243      b <- asKey $ show a
244      return $ BinOpAttr a $ tokPos b) l)
245    <|> do
246    a <- asKey unitS
247    t <- term
248    return $ UnitOpAttr t $ tokPos a
249
250multiTypeScheme :: [PolyId] -> AParser st TypeScheme
251multiTypeScheme os = case os of
252    p : r -> if null r || all ( \ (PolyId _ tys _) -> null tys) os
253      then typeScheme p
254      else fail $ "instantiation list in identifier list: "
255               ++ show (map ( \ (PolyId i _ _) -> i) os)
256    _ -> error "HasCASL.ParseItem.opDecl"
257
258opDecl :: [PolyId] -> [Token] -> AParser st OpItem
259opDecl os ps = do
260    c <- colonST
261    t <- multiTypeScheme os
262    opAttrs os ps c t <|> return (OpDecl os t [] $ catRange $ ps ++ [c])
263
264opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
265opAttrs os ps c t = do
266    d <- anComma
267    (attrs, cs) <- opAttr `separatedBy` anComma
268    return $ OpDecl os t attrs $ catRange $ ps ++ [c, d] ++ cs
269
270opArg :: AParser st ([VarDecl], Range)
271opArg = bracketParser varDecls oParenT cParenT anSemi concatFst
272
273opArgs :: AParser st ([[VarDecl]], Range)
274opArgs = do
275    cps <- many1 opArg
276    return (map fst cps, concatMapRange snd cps)
277
278opDeclOrDefn :: PolyId -> AParser st OpItem
279opDeclOrDefn o = do
280    c <- colonST
281    t <- typeScheme o
282    opAttrs [o] [] c t <|> opTerm o [] nullRange c t
283        <|> return (OpDecl [o] t [] $ tokPos c)
284  <|> do
285    (args, ps) <- opArgs
286    c <- colonST
287    t <- fmap simpleTypeScheme parseType
288    opTerm o args ps c t
289
290opTerm :: PolyId -> [[VarDecl]] -> Range -> Token -> TypeScheme
291       -> AParser st OpItem
292opTerm o as ps c sc = do
293    e <- equalT
294    f <- term
295    return $ OpDefn o as sc f $ appRange ps $ toRange c [] e
296
297opItem :: AParser st OpItem
298opItem = do
299    (os, ps) <- parsePolyId `separatedBy` anComma
300    case os of
301      [hd] -> opDeclOrDefn hd
302      _ -> opDecl os ps
303
304opItems :: AParser st SigItems
305opItems = hasCaslItemList opS opItem (OpItems Op)
306    <|> hasCaslItemList functS opItem (OpItems Fun)
307
308-- * parse pred items as op items
309
310predDecl :: [PolyId] -> [Token] -> AParser st OpItem
311predDecl os ps = do
312    c <- colT
313    t <- multiTypeScheme os
314    let p = catRange $ ps ++ [c]
315    return $ OpDecl os (predTypeScheme p t) [] p
316
317predDefn :: PolyId -> AParser st OpItem
318predDefn o = do
319    (args, ps) <- opArg
320    e <- asKey equivS
321    f <- term
322    let p = appRange ps $ tokPos e
323    return $ OpDefn o [args]
324        (simpleTypeScheme $ mkLazyType $ unitTypeWithRange p) f p
325
326predItem :: AParser st OpItem
327predItem = do
328    (os, ps) <- parsePolyId `separatedBy` anComma
329    let d = predDecl os ps
330    case os of
331      [hd] -> d <|> predDefn hd
332      _ -> d
333
334predItems :: AParser st SigItems
335predItems = hasCaslItemList predS predItem (OpItems Pred)
336
337-- * other items
338
339sigItems :: AParser st SigItems
340sigItems = sortItems <|> opItems <|> predItems <|> typeItems
341
342generatedItems :: AParser st BasicItem
343generatedItems = do
344    g <- asKey generatedS
345    do  FreeDatatype ds ps <- dataItems
346        return $ GenItems [Annoted (TypeItems Plain (map ( \ d -> Annoted
347            (Datatype $ item d) nullRange (l_annos d) (r_annos d)) ds) ps)
348                          nullRange [] []] $ tokPos g
349      <|> do
350        o <- oBraceT
351        is <- annosParser sigItems
352        c <- cBraceT
353        return $ GenItems is $ toRange g [o] c
354
355genVarItems :: AParser st ([GenVarDecl], [Token])
356genVarItems = do
357    vs <- genVarDecls
358    do  s <- try (addAnnos >> Common.Lexer.semiT << addLineAnnos)
359        do  tryItemEnd hasCaslStartKeywords
360            return (vs, [s])
361          <|> do
362            (ws, ts) <- genVarItems
363            return (vs ++ ws, s : ts)
364      <|> return (vs, [])
365
366freeDatatype :: AParser st BasicItem
367freeDatatype = do
368    f <- asKey freeS
369    FreeDatatype ds ps <- dataItems
370    return $ FreeDatatype ds $ appRange (tokPos f) ps
371
372progItems :: AParser st BasicItem
373progItems = hasCaslItemList programS
374    (patternTermPair [equalS] (WithIn, []) equalS) ProgItems
375
376axiomItems :: AParser st BasicItem
377axiomItems = hasCaslItemList axiomS term $ AxiomItems []
378
379forallItem :: AParser st BasicItem
380forallItem = do
381    f <- forallT
382    (vs, ps) <- genVarDecls `separatedBy` anSemi
383    a <- annos
384    AxiomItems _ ((Annoted ft qs as rs):fs) ds <- dotFormulae
385    let aft = Annoted ft qs (a ++ as) rs
386    return $ AxiomItems (concat vs) (aft : fs) $ appRange (catRange $ f : ps) ds
387
388genVarItem :: AParser st BasicItem
389genVarItem = do
390    v <- pluralKeyword varS
391    (vs, ps) <- genVarItems
392    return $ GenVarItems vs $ catRange $ v:ps
393
394dotFormulae :: AParser st BasicItem
395dotFormulae = do
396    d <- dotT
397    let aFormula = bind appendAnno (annoParser term) lineAnnos
398    (fs, ds) <- aFormula `separatedBy` dotT
399    let ps = catRange $ d : ds
400        lst = last fs
401    if null $ r_annos lst then do
402        (m, an) <- optSemi
403        return $ AxiomItems [] (init fs ++ [appendAnno lst an]) $ appRange ps
404               $ catRange m
405       else return $ AxiomItems [] fs ps
406
407internalItems :: AParser st BasicItem
408internalItems = do
409    i <- asKey internalS
410    o <- oBraceT
411    is <- annosParser basicItems
412    p <- cBraceT
413    return (Internal is $ toRange i [o] p)
414
415basicItems :: AParser st BasicItem
416basicItems = fmap SigItems sigItems
417    <|> classItems
418    <|> progItems
419    <|> generatedItems
420    <|> freeDatatype
421    <|> genVarItem
422    <|> forallItem
423    <|> dotFormulae
424    <|> axiomItems
425    <|> internalItems
426
427basicSpec :: AParser st BasicSpec
428basicSpec = fmap BasicSpec (annosParser basicItems)
Note: See TracBrowser for help on using the browser.