ParseItem.hs revision 9e0472be46104307b974fe5079bf5cc9e94a1a96
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
0992b212df8eec8af18e1c208da54897021964c4Christian MaederDescription : parser for HasCASL basic Items
0992b212df8eec8af18e1c208da54897021964c4Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder
0992b212df8eec8af18e1c208da54897021964c4Christian MaederMaintainer : Christian.Maeder@dfki.de
0992b212df8eec8af18e1c208da54897021964c4Christian MaederStability : provisional
0992b212df8eec8af18e1c208da54897021964c4Christian MaederPortability : portable
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder
0992b212df8eec8af18e1c208da54897021964c4Christian Maederparser for HasCASL basic Items
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder-}
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maedermodule HasCASL.ParseItem (basicItems, basicSpec) where
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maeder
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maederimport Text.ParserCombinators.Parsec
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maeder
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maederimport Common.AS_Annotation
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport Common.AnnoState
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport Common.Id
c1cb6bd6e48671031b23730b3cd1dcc7593ecb30Christian Maederimport Common.Keywords
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport Common.Lexer
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport Common.Token
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport HasCASL.HToken
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport HasCASL.As
0992b212df8eec8af18e1c208da54897021964c4Christian Maederimport HasCASL.AsUtils
92dc581bf568c9e225aa9d0570ab0a4b6ebdab69Christian Maederimport HasCASL.ParseTerm
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- * adapted item list parser (using 'itemAux')
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederhasCaslItemList :: String -> AParser st b
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -> ([Annoted b] -> Range -> a) -> AParser st a
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederhasCaslItemList kw ip constr = do
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder p <- pluralKeyword kw
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder auxItemList hasCaslStartKeywords [p] ip constr
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian MaederhasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder -> AParser st a
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian MaederhasCaslItemAux ps = auxItemList hasCaslStartKeywords ps
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder-- * parsing type items
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder
0d3b1901921690f9ac499d03b08f63b44182481cChristian MaedercommaTypeDecl :: TypePattern -> AParser st TypeItem
0d3b1901921690f9ac499d03b08f63b44182481cChristian MaedercommaTypeDecl s = do
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder c <- anComma
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maeder (is, cs) <- typePattern `separatedBy` anComma
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maeder let l = s : is
0d3b1901921690f9ac499d03b08f63b44182481cChristian Maeder p = c : cs
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder subTypeDecl (l, p) <|> kindedTypeDecl (l, p)
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder <|> return (TypeDecl l universe $ catPos p)
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian MaederkindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian MaederkindedTypeDecl (l, p) = do
0a73a105711f90b75f4785fbe2bbdf16071b98a9Christian Maeder t <- colT
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder s <- kind
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian Maeder let d = TypeDecl l s $ catPos $ p ++ [t]
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder case l of
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder [hd] -> pseudoTypeDef hd (Just s) [t] <|> dataDef hd s [t] <|> return d
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder _ -> return d
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian Maeder
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian MaederisoDecl :: TypePattern -> AParser st TypeItem
0d3b1901921690f9ac499d03b08f63b44182481cChristian MaederisoDecl s = do
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder e <- equalT
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder subTypeDefn (s, e) <|> do
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder (l, p) <- typePattern `separatedBy` equalT
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder return $ IsoDecl (s : l) $ catPos $ e : p
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian Maeder
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maedervars :: AParser st Vars
8dfaa1b79cf2f92e897a034408954b4715f602b4Christian Maedervars = fmap Var var <|> do
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian Maeder o <- oParenT
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (vs, ps) <- vars `separatedBy` anComma
d009a47a0497fe50dd3c11d3bb3ad639be3f947dChristian Maeder c <- cParenT
d009a47a0497fe50dd3c11d3bb3ad639be3f947dChristian Maeder return $ VarTuple vs $ toPos o ps c
d009a47a0497fe50dd3c11d3bb3ad639be3f947dChristian Maeder
d009a47a0497fe50dd3c11d3bb3ad639be3f947dChristian MaedersubTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
8cffae2c30c242f56abac2052d0b5691dc6e1784Christian MaedersubTypeDefn (s, e) = do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder a <- annos
0992b212df8eec8af18e1c208da54897021964c4Christian Maeder o <- oBraceT
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder v <- vars
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder c <- colT
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder t <- parseType
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder d <- dotT -- or bar
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder f <- term
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder p <- cBraceT
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder let qs = toPos e [o,c,d] p
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder return $ SubtypeDefn s v t (Annoted f qs a []) qs
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedersubTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian MaedersubTypeDecl (l, p) = do
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder t <- lessT
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder s <- parseType
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder return $ SubtypeDecl l s $ catPos $ p ++ [t]
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian MaedersortItem :: AParser st TypeItem
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedersortItem = do
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder s <- typePattern
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder subTypeDecl ([s],[])
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder <|> kindedTypeDecl ([s],[])
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder <|> commaTypeDecl s
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder <|> isoDecl s
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder <|> return (TypeDecl [s] universe nullRange)
ad5f48cb4f7d459e2c0fa67ea108243dcc399de2Christian Maeder
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedersortItems :: AParser st SigItems
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaedersortItems = hasCaslItemList sortS sortItem (TypeItems Plain)
typeItem :: AParser st TypeItem
typeItem = do
s <- typePattern;
subTypeDecl ([s],[])
<|> dataDef s universe []
<|> pseudoTypeDef s Nothing []
<|> kindedTypeDecl ([s],[])
<|> commaTypeDecl s
<|> isoDecl s
<|> return (TypeDecl [s] universe nullRange)
typeItemList :: [Token] -> Instance -> AParser st SigItems
typeItemList ps k = hasCaslItemAux ps typeItem $ TypeItems k
typeItems :: AParser st SigItems
typeItems = do
p <- pluralKeyword typeS
do q <- pluralKeyword instanceS
typeItemList [p, q] Instance
<|> typeItemList [p] Plain
-- | several 'typeArg's
typeArgs :: AParser st ([TypeArg], [Token])
typeArgs = do
l <- many1 typeArg
return (map fst l, concatMap snd l)
pseudoType :: AParser st TypeScheme
pseudoType = do
l <- asKey lamS
(ts, pps) <- typeArgs
d <- dotT
t <- pseudoType
let qs = toPos l pps d
case t of
TypeScheme ts1 gt ps ->
return $ TypeScheme (ts1 ++ ts) gt (ps `appRange` qs)
<|> do
st <- parseType
return $ simpleTypeScheme st
pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef t k l = do
c <- asKey assignS
p <- pseudoType
return $ AliasType t k p $ catPos $ l ++ [c]
-- * parsing datatypes
component :: AParser st [Component]
component = try (do
(is, cs) <- opId `separatedBy` anComma
compType is cs) <|> do
t <- parseType
return [NoSelector t]
concatFst :: [[a]] -> Range -> ([a], Range)
concatFst as ps = (concat as, ps)
tupleComponent :: AParser st ([Component], Range)
tupleComponent = bracketParser component oParenT cParenT anSemi concatFst
altComponent :: AParser st ([Component], Range)
altComponent = tupleComponent <|> do
i <- typeVar
let t = case i of
Id [tok] [] _ -> TypeToken tok
_ -> error "altComponent"
return ([NoSelector t], nullRange)
compType :: [Id] -> [Token] -> AParser st [Component]
compType is cs = do
c <- colonST
t <- parseType
let makeComps l1 l2 = case (l1, l2) of
([a], [b]) -> [Selector a Total t Other $ tokPos b]
(a : r, b : s) -> Selector a Total t Comma (tokPos b) : makeComps r s
_ -> error "makeComps: empty selector list"
return $ makeComps is $ cs ++ [c]
alternative :: AParser st Alternative
alternative = do
s <- pluralKeyword sortS <|> pluralKeyword typeS
(ts, cs) <- parseType `separatedBy` anComma
return $ Subtype ts $ catPos $ s : cs
<|> do
i <- hconsId
cps <- many altComponent
let ps = concatMapRange snd cps
cs = map fst cps
do q <- quMarkT
return $ Constructor i cs Partial $ appRange ps $ tokPos q
<|> return (Constructor i cs Total ps)
dataDef :: TypePattern -> Kind -> [Token] -> AParser st TypeItem
dataDef t k l = do
c <- asKey defnS
a <- annos
let aAlternative = bind (\ i an -> Annoted i nullRange [] an)
alternative annos
(Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT
let aa = Annoted v nullRange a b : as
qs = catPos $ l ++ c : ps
do d <- asKey derivingS
(cs, cps) <- classId `separatedBy` anComma
return $ Datatype $ DatatypeDecl t k aa cs
$ appRange qs $ appRange (tokPos d) $ catPos cps
<|> return (Datatype (DatatypeDecl t k aa [] qs))
dataItem :: AParser st DatatypeDecl
dataItem = do
t <- typePattern
do c <- colT
k <- kind
Datatype d <- dataDef t k [c]
return d
<|> do
Datatype d <- dataDef t universe []
return d
dataItems :: AParser st BasicItem
dataItems = hasCaslItemList typeS dataItem FreeDatatype
-- * parse class items
classDecl :: AParser st ClassDecl
classDecl = do
(is, cs) <- classId `separatedBy` anComma
(ps, k) <- option ([], universe) $ bind (,) (single $ colT <|> lessT) kind
return $ ClassDecl is k $ catPos $ cs ++ ps
classItem :: AParser st ClassItem
classItem = do
c <- classDecl
do o <- oBraceT
is <- annosParser basicItems
p <- cBraceT
return $ ClassItem c is $ toPos o [] p
<|> return (ClassItem c [] nullRange)
classItemList :: [Token] -> Instance -> AParser st BasicItem
classItemList ps k = hasCaslItemAux ps classItem $ ClassItems k
classItems :: AParser st BasicItem
classItems = do
p <- asKey (classS ++ "es") <|> asKey classS <?> classS
do q <- pluralKeyword instanceS
classItemList [p, q] Instance
<|> classItemList [p] Plain
-- * parse op items
opAttr :: AParser st OpAttr
opAttr = let l = [Assoc, Comm, Idem] in
choice (map ( \ a -> do
b <- asKey $ show a
return $ BinOpAttr a $ tokPos b) l)
<|> do
a <- asKey unitS
t <- term
return $ UnitOpAttr t $ tokPos a
opDecl :: [PolyId] -> [Token] -> AParser st OpItem
opDecl os ps = do
c <- colonST
t <- typeScheme
opAttrs os ps c t <|> return (OpDecl os t [] $ catPos $ ps ++ [c])
opAttrs :: [PolyId] -> [Token] -> Token -> TypeScheme -> AParser st OpItem
opAttrs os ps c t = do
d <- anComma
(attrs, cs) <- opAttr `separatedBy` anComma
return $ OpDecl os t attrs $ catPos $ ps ++ [c, d] ++ cs
opArg :: AParser st ([VarDecl], Range)
opArg = bracketParser varDecls oParenT cParenT anSemi concatFst
opArgs :: AParser st ([[VarDecl]], Range)
opArgs = do
cps <- many1 opArg
return (map fst cps, concatMapRange snd cps)
opDeclOrDefn :: PolyId -> AParser st OpItem
opDeclOrDefn o = do
c <- colonST
t <- typeScheme
opAttrs [o] [] c t <|> opTerm o [] nullRange c t
<|> return (OpDecl [o] t [] $ tokPos c)
<|> do
(args, ps) <- opArgs
c <- colonST
t <- fmap simpleTypeScheme parseType
opTerm o args ps c t
opTerm :: PolyId -> [[VarDecl]] -> Range -> Token -> TypeScheme
-> AParser st OpItem
opTerm o as ps c sc = do
e <- equalT
f <- term
return $ OpDefn o as sc f $ appRange ps $ toPos c [] e
opItem :: AParser st OpItem
opItem = do
(os, ps) <- parsePolyId `separatedBy` anComma
case os of
[hd] -> opDeclOrDefn hd
_ -> opDecl os ps
opItems :: AParser st SigItems
opItems = hasCaslItemList opS opItem (OpItems Op)
<|> hasCaslItemList functS opItem (OpItems Fun)
-- * parse pred items as op items
predDecl :: [PolyId] -> [Token] -> AParser st OpItem
predDecl os ps = do
c <- colT
t <- typeScheme
let p = catPos $ ps ++ [c]
return $ OpDecl os (predTypeScheme p t) [] p
predDefn :: PolyId -> AParser st OpItem
predDefn o = do
(args, ps) <- opArg
e <- asKey equivS
f <- term
let p = appRange ps $ tokPos e
return $ OpDefn o [args]
(simpleTypeScheme $ mkLazyType $ unitTypeWithRange p) f p
predItem :: AParser st OpItem
predItem = do
(os, ps) <- parsePolyId `separatedBy` anComma
let d = predDecl os ps
case os of
[hd] -> d <|> predDefn hd
_ -> d
predItems :: AParser st SigItems
predItems = hasCaslItemList predS predItem (OpItems Pred)
-- * other items
sigItems :: AParser st SigItems
sigItems = sortItems <|> opItems <|> predItems <|> typeItems
generatedItems :: AParser st BasicItem
generatedItems = do
g <- asKey generatedS
do FreeDatatype ds ps <- dataItems
return $ GenItems [Annoted (TypeItems Plain (map ( \ d -> Annoted
(Datatype $ item d) nullRange (l_annos d) (r_annos d)) ds) ps)
nullRange [] []] $ tokPos g
<|> do
o <- oBraceT
is <- annosParser sigItems
c <- cBraceT
return $ GenItems is $ toPos g [o] c
genVarItems :: AParser st ([GenVarDecl], [Token])
genVarItems = do
vs <- genVarDecls
do s <- try (addAnnos >> Common.Lexer.semiT << addLineAnnos)
do tryItemEnd hasCaslStartKeywords
return (vs, [s])
<|> do
(ws, ts) <- genVarItems
return (vs ++ ws, s : ts)
<|> return (vs, [])
freeDatatype :: AParser st BasicItem
freeDatatype = do
f <- asKey freeS
FreeDatatype ds ps <- dataItems
return $ FreeDatatype ds $ appRange (tokPos f) ps
progItems :: AParser st BasicItem
progItems = hasCaslItemList programS
(patternTermPair [equalS] (WithIn, []) equalS) ProgItems
axiomItems :: AParser st BasicItem
axiomItems = hasCaslItemList axiomS term $ AxiomItems []
forallItem :: AParser st BasicItem
forallItem = do
f <- forallT
(vs, ps) <- genVarDecls `separatedBy` anSemi
a <- annos
AxiomItems _ ((Annoted ft qs as rs):fs) ds <- dotFormulae
let aft = Annoted ft qs (a ++ as) rs
return $ AxiomItems (concat vs) (aft : fs) $ appRange (catPos $ f : ps) ds
genVarItem :: AParser st BasicItem
genVarItem = do
v <- pluralKeyword varS
(vs, ps) <- genVarItems
return $ GenVarItems vs $ catPos $ v:ps
dotFormulae :: AParser st BasicItem
dotFormulae = do
d <- dotT
let aFormula = bind appendAnno (annoParser term) lineAnnos
(fs, ds) <- aFormula `separatedBy` dotT
let ps = catPos $ d : ds
lst = last fs
if null $ r_annos lst then do
(m, an) <- optSemi
return $ AxiomItems [] (init fs ++ [appendAnno lst an]) $ appRange ps
$ catPos m
else return $ AxiomItems [] fs ps
internalItems :: AParser st BasicItem
internalItems = do
i <- asKey internalS
o <- oBraceT
is <- annosParser basicItems
p <- cBraceT
return (Internal is $ toPos i [o] p)
basicItems :: AParser st BasicItem
basicItems = fmap SigItems sigItems
<|> classItems
<|> progItems
<|> generatedItems
<|> freeDatatype
<|> genVarItem
<|> forallItem
<|> dotFormulae
<|> axiomItems
<|> internalItems
basicSpec :: AParser st BasicSpec
basicSpec = fmap BasicSpec (annosParser basicItems)
<|> (oBraceT >> cBraceT >> return (BasicSpec []))