root/trunk/HasCASL/ParseItem.hs @ 11328

Revision 11328, 12.7 kB (checked in by maeder, 10 months ago)

add sentence of subtype definition

  • 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
129-- | several 'typeArg's
130typeArgs :: AParser st ([TypeArg], [Token])
131typeArgs = do
132    l <- many1 typeArg
133    return (map fst l, concatMap snd l)
134
135pseudoType :: AParser st TypeScheme
136pseudoType = do
137    l <- asKey lamS
138    (ts, pps) <- typeArgs
139    d <- dotT
140    t <- pseudoType
141    let qs = toRange l pps d
142    case t of
143      TypeScheme ts1 gt ps ->
144          return $ TypeScheme (ts ++ ts1) gt $ appRange qs ps
145  <|> do
146    st <- parseType
147    return $ simpleTypeScheme st
148
149pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
150pseudoTypeDef t k l = do
151    c <- asKey assignS
152    p <- pseudoType
153    return $ AliasType t k p $ catRange $ l ++ [c]
154
155-- * parsing datatypes
156
157component :: AParser st [Component]
158component = try (do
159    (is, cs) <- opId `separatedBy` anComma
160    compType is cs) <|> do
161    t <- parseType
162    return [NoSelector t]
163
164concatFst :: [[a]] -> Range -> ([a], Range)
165concatFst as ps = (concat as, ps)
166
167tupleComponent :: AParser st ([Component], Range)
168tupleComponent = bracketParser component oParenT cParenT anSemi concatFst
169
170altComponent :: AParser st ([Component], Range)
171altComponent = tupleComponent <|> do
172    i <- typeVar
173    let t = case i of
174          Id [tok] [] _ -> TypeToken tok
175          _ -> error "altComponent"
176    return ([NoSelector t], nullRange)
177
178compType :: [Id] -> [Token] -> AParser st [Component]
179compType is cs = do
180    c <- colonST
181    t <- parseType
182    let makeComps l1 l2 = case (l1, l2) of
183          ([a], [b]) -> [Selector a Total t Other $ tokPos b]
184          (a : r, b : s) -> Selector a Total t Comma (tokPos b) : makeComps r s
185          _ -> error "makeComps: empty selector list"
186    return $ makeComps is $ cs ++ [c]
187
188alternative :: AParser st Alternative
189alternative = do
190    s <- pluralKeyword sortS <|> pluralKeyword typeS
191    (ts, cs) <- parseType `separatedBy` anComma
192    return $ Subtype ts $ catRange $ s : cs
193  <|> do
194    i <- hconsId
195    cps <- many altComponent
196    let ps = concatMapRange snd cps
197        cs = map fst cps
198    do  q <- quMarkT
199        return $ Constructor i cs Partial $ appRange ps $ tokPos q
200      <|> return (Constructor i cs Total ps)
201
202dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
203dataDef t k l = do
204    c <- asKey defnS
205    a <- annos
206    let aAlternative = bind (\ i an -> Annoted i nullRange [] an)
207          alternative annos
208    (Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT
209    let aa = Annoted v nullRange a b : as
210        qs = catRange $ l ++ c : ps
211    do  d <- asKey derivingS
212        (cs, cps) <- classId `separatedBy` anComma
213        return $ Datatype $ DatatypeDecl t k aa cs
214                    $ appRange qs $ appRange (tokPos d) $ catRange cps
215      <|> return (Datatype (DatatypeDecl t k aa [] qs))
216
217dataItem :: AParser st DatatypeDecl
218dataItem = do
219     t <- typePattern
220     do  c <- colT
221         k <- kind
222         Datatype d <- dataDef t k [c]
223         return d
224       <|> do
225         Datatype d <- dataDef t universe []
226         return d
227
228dataItems :: AParser st BasicItem
229dataItems = hasCaslItemList typeS dataItem FreeDatatype
230
231-- * parse class items
232
233classDecl :: AParser st ClassDecl
234classDecl = do
235    (is, cs) <- classId `separatedBy` anComma
236    (ps, k) <- option ([], universe) $ bind  (,) (single lessT) kind
237    return $ ClassDecl is k $ catRange $ cs ++ ps
238
239classItem :: AParser st ClassItem
240classItem = do
241    c <- classDecl
242    do  o <- oBraceT
243        is <- annosParser basicItems
244        p <- cBraceT
245        return $ ClassItem c is $ toRange o [] p
246      <|> return (ClassItem c [] nullRange)
247
248classItemList :: [Token] -> Instance -> AParser st BasicItem
249classItemList ps k = hasCaslItemAux ps classItem $ ClassItems k
250
251classItems :: AParser st BasicItem
252classItems = do
253    p <- asKey (classS ++ "es") <|> asKey classS <?> classS
254    do  q <- pluralKeyword instanceS
255        classItemList [p, q] Instance
256      <|> classItemList [p] Plain
257
258-- * parse op items
259
260opAttr :: AParser st OpAttr
261opAttr = let l = [Assoc, Comm, Idem] in
262    choice (map ( \ a -> do
263      b <- asKey $ show a
264      return $ BinOpAttr a $ tokPos b) l)
265    <|> do
266    a <- asKey unitS
267    t <- term
268    return $ UnitOpAttr t $ tokPos a
269
270multiTypeScheme :: [PolyId] -> AParser st TypeScheme
271multiTypeScheme os = case os of
272    p : r -> if null r || all ( \ (PolyId _ tys _) -> null tys) os
273      then typeScheme p
274      else fail $ "instantiation list in identifier list: "
275               ++ show (map ( \ (PolyId i _ _) -> i) os)
276    _ -> error "HasCASL.ParseItem.opDecl"
277
278opDecl :: [PolyId] -> [Token] -> AParser st OpItem
279opDecl os ps = do
280    c <- colonST
281    t <- multiTypeScheme os
282    opAttrs os ps c t <|> return (OpDecl os t [] $ catRange $ ps ++ [c])
283
284opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
285opAttrs os ps c t = do
286    d <- anComma
287    (attrs, cs) <- opAttr `separatedBy` anComma
288    return $ OpDecl os t attrs $ catRange $ ps ++ [c, d] ++ cs
289
290opArg :: AParser st ([VarDecl], Range)
291opArg = bracketParser varDecls oParenT cParenT anSemi concatFst
292
293opArgs :: AParser st ([[VarDecl]], Range)
294opArgs = do
295    cps <- many1 opArg
296    return (map fst cps, concatMapRange snd cps)
297
298opDeclOrDefn :: PolyId -> AParser st OpItem
299opDeclOrDefn o = do
300    c <- colonST
301    t <- typeScheme o
302    opAttrs [o] [] c t <|> opTerm o [] nullRange c t
303        <|> return (OpDecl [o] t [] $ tokPos c)
304  <|> do
305    (args, ps) <- opArgs
306    c <- colonST
307    t <- fmap simpleTypeScheme parseType
308    opTerm o args ps c t
309
310opTerm :: PolyId -> [[VarDecl]] -> Range -> Token -> TypeScheme
311       -> AParser st OpItem
312opTerm o as ps c sc = do
313    e <- equalT
314    f <- term
315    return $ OpDefn o as sc f $ appRange ps $ toRange c [] e
316
317opItem :: AParser st OpItem
318opItem = do
319    (os, ps) <- parsePolyId `separatedBy` anComma
320    case os of
321      [hd] -> opDeclOrDefn hd
322      _ -> opDecl os ps
323
324opItems :: AParser st SigItems
325opItems = hasCaslItemList opS opItem (OpItems Op)
326    <|> hasCaslItemList functS opItem (OpItems Fun)
327
328-- * parse pred items as op items
329
330predDecl :: [PolyId] -> [Token] -> AParser st OpItem
331predDecl os ps = do
332    c <- colT
333    t <- multiTypeScheme os
334    let p = catRange $ ps ++ [c]
335    return $ OpDecl os (predTypeScheme p t) [] p
336
337predDefn :: PolyId -> AParser st OpItem
338predDefn o = do
339    (args, ps) <- opArg
340    e <- asKey equivS
341    f <- term
342    let p = appRange ps $ tokPos e
343    return $ OpDefn o [args]
344        (simpleTypeScheme $ mkLazyType $ unitTypeWithRange p) f p
345
346predItem :: AParser st OpItem
347predItem = do
348    (os, ps) <- parsePolyId `separatedBy` anComma
349    let d = predDecl os ps
350    case os of
351      [hd] -> d <|> predDefn hd
352      _ -> d
353
354predItems :: AParser st SigItems
355predItems = hasCaslItemList predS predItem (OpItems Pred)
356
357-- * other items
358
359sigItems :: AParser st SigItems
360sigItems = sortItems <|> opItems <|> predItems <|> typeItems
361
362generatedItems :: AParser st BasicItem
363generatedItems = do
364    g <- asKey generatedS
365    do  FreeDatatype ds ps <- dataItems
366        return $ GenItems [Annoted (TypeItems Plain (map ( \ d -> Annoted
367            (Datatype $ item d) nullRange (l_annos d) (r_annos d)) ds) ps)
368                          nullRange [] []] $ tokPos g
369      <|> do
370        o <- oBraceT
371        is <- annosParser sigItems
372        c <- cBraceT
373        return $ GenItems is $ toRange g [o] c
374
375genVarItems :: AParser st ([GenVarDecl], [Token])
376genVarItems = do
377    vs <- genVarDecls
378    do  s <- try (addAnnos >> Common.Lexer.semiT << addLineAnnos)
379        do  tryItemEnd hasCaslStartKeywords
380            return (vs, [s])
381          <|> do
382            (ws, ts) <- genVarItems
383            return (vs ++ ws, s : ts)
384      <|> return (vs, [])
385
386freeDatatype :: AParser st BasicItem
387freeDatatype = do
388    f <- asKey freeS
389    FreeDatatype ds ps <- dataItems
390    return $ FreeDatatype ds $ appRange (tokPos f) ps
391
392progItems :: AParser st BasicItem
393progItems = hasCaslItemList programS
394    (patternTermPair [equalS] (WithIn, []) equalS) ProgItems
395
396axiomItems :: AParser st BasicItem
397axiomItems = hasCaslItemList axiomS term $ AxiomItems []
398
399forallItem :: AParser st BasicItem
400forallItem = do
401    f <- forallT
402    (vs, ps) <- genVarDecls `separatedBy` anSemi
403    a <- annos
404    AxiomItems _ ((Annoted ft qs as rs):fs) ds <- dotFormulae
405    let aft = Annoted ft qs (a ++ as) rs
406    return $ AxiomItems (concat vs) (aft : fs) $ appRange (catRange $ f : ps) ds
407
408genVarItem :: AParser st BasicItem
409genVarItem = do
410    v <- pluralKeyword varS
411    (vs, ps) <- genVarItems
412    return $ GenVarItems vs $ catRange $ v:ps
413
414dotFormulae :: AParser st BasicItem
415dotFormulae = do
416    d <- dotT
417    let aFormula = bind appendAnno (annoParser term) lineAnnos
418    (fs, ds) <- aFormula `separatedBy` dotT
419    let ps = catRange $ d : ds
420        lst = last fs
421    if null $ r_annos lst then do
422        (m, an) <- optSemi
423        return $ AxiomItems [] (init fs ++ [appendAnno lst an]) $ appRange ps
424               $ catRange m
425       else return $ AxiomItems [] fs ps
426
427internalItems :: AParser st BasicItem
428internalItems = do
429    i <- asKey internalS
430    o <- oBraceT
431    is <- annosParser basicItems
432    p <- cBraceT
433    return (Internal is $ toRange i [o] p)
434
435basicItems :: AParser st BasicItem
436basicItems = fmap SigItems sigItems
437    <|> classItems
438    <|> progItems
439    <|> generatedItems
440    <|> freeDatatype
441    <|> genVarItem
442    <|> forallItem
443    <|> dotFormulae
444    <|> axiomItems
445    <|> internalItems
446
447basicSpec :: AParser st BasicSpec
448basicSpec = fmap BasicSpec (annosParser basicItems)
Note: See TracBrowser for help on using the browser.