ParseItem.hs revision a21be3ba0cb875d618b2b227f7c23e2ccc0bcb3b
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu{- |
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuModule : $Header$
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuDescription : parser for HasCASL basic Items
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuMaintainer : Christian.Maeder@dfki.de
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuStability : provisional
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuPortability : portable
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savuparser for HasCASL basic Items
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu-}
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savumodule HasCASL.ParseItem (basicItems, basicSpec) where
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert Savuimport Text.ParserCombinators.Parsec
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert Savuimport Common.AS_Annotation
69b1e90bbb27ce2dd365628c07c0f03a3ae97b26Robert Savuimport Common.AnnoState
ad2e68e571352b6759441733df697e075ceed341Robert Savuimport Common.Id
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulzimport Common.Keywords
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulzimport Common.Lexer
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulzimport Common.Token
ad2e68e571352b6759441733df697e075ceed341Robert Savu
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savuimport HasCASL.HToken
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savuimport HasCASL.As
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savuimport HasCASL.AsUtils
37dd4c99dbe470cce3fe0d89a011186f080e8910Robert Savuimport HasCASL.ParseTerm
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu-- * adapted item list parser (using 'itemAux')
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzhasCaslItemList :: String -> AParser st b
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu -> ([Annoted b] -> Range -> a) -> AParser st a
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavuhasCaslItemList kw ip constr = do
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu p <- pluralKeyword kw
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz auxItemList hasCaslStartKeywords [p] ip constr
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert SavuhasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
ad2e68e571352b6759441733df697e075ceed341Robert Savu -> AParser st a
ad2e68e571352b6759441733df697e075ceed341Robert SavuhasCaslItemAux ps = auxItemList hasCaslStartKeywords ps
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert Savu-- * parsing type items
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert SavucommaTypeDecl :: TypePattern -> AParser st TypeItem
ad2e68e571352b6759441733df697e075ceed341Robert SavucommaTypeDecl s = do
ad2e68e571352b6759441733df697e075ceed341Robert Savu c <- anComma
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu (is, cs) <- typePattern `separatedBy` anComma
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu let l = s : is
ad2e68e571352b6759441733df697e075ceed341Robert Savu p = c : cs
ad2e68e571352b6759441733df697e075ceed341Robert Savu subTypeDecl (l, p) <|> kindedTypeDecl (l, p)
ad2e68e571352b6759441733df697e075ceed341Robert Savu <|> return (TypeDecl l universe $ catPos p)
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavukindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavukindedTypeDecl (l, p) = do
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu t <- colT
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu s <- kind
ad2e68e571352b6759441733df697e075ceed341Robert Savu let d = TypeDecl l s $ catPos $ p ++ [t]
ad2e68e571352b6759441733df697e075ceed341Robert Savu case l of
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz [hd] -> pseudoTypeDef hd (Just s) [t] <|> dataDef hd s [t] <|> return d
ad2e68e571352b6759441733df697e075ceed341Robert Savu _ -> return d
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert SavuisoDecl :: TypePattern -> AParser st TypeItem
ad2e68e571352b6759441733df697e075ceed341Robert SavuisoDecl s = do
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu e <- equalT
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu subTypeDefn (s, e) <|> do
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (l, p) <- typePattern `separatedBy` equalT
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu return $ IsoDecl (s : l) $ catPos $ e : p
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuvars :: AParser st Vars
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuvars = fmap Var var <|> do
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu o <- oParenT
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu (vs, ps) <- vars `separatedBy` anComma
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu c <- cParenT
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu return $ VarTuple vs $ toPos o ps c
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavusubTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst SchulzsubTypeDefn (s, e) = do
ad2e68e571352b6759441733df697e075ceed341Robert Savu a <- annos
ad2e68e571352b6759441733df697e075ceed341Robert Savu o <- oBraceT
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz v <- vars
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu c <- colT
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz t <- parseType
ad2e68e571352b6759441733df697e075ceed341Robert Savu d <- dotT -- or bar
ad2e68e571352b6759441733df697e075ceed341Robert Savu f <- term
e09066e7b76cea97557974b825bb057455b24ab0Robert Savu p <- cBraceT
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert Savu let qs = toPos e [o,c,d] p
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz return $ SubtypeDefn s v t (Annoted f qs a []) qs
ad2e68e571352b6759441733df697e075ceed341Robert Savu
b3df7e69d4d6066fdfae0a8a2f3b4a161eaaf540Robert SavusubTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavusubTypeDecl (l, p) = do
ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu t <- lessT
ad2e68e571352b6759441733df697e075ceed341Robert Savu s <- parseType
ad2e68e571352b6759441733df697e075ceed341Robert Savu return $ SubtypeDecl l s $ catPos $ p ++ [t]
ad2e68e571352b6759441733df697e075ceed341Robert Savu
ad2e68e571352b6759441733df697e075ceed341Robert SavusortItem :: AParser st TypeItem
ad2e68e571352b6759441733df697e075ceed341Robert SavusortItem = do
a9c461443a740732a62d58c1c465b88cba3c606bRobert Savu s <- typePattern
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz subTypeDecl ([s],[])
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz <|> kindedTypeDecl ([s],[])
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz <|> commaTypeDecl s
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz <|> isoDecl s
<|> return (TypeDecl [s] universe nullRange)
sortItems :: AParser st SigItems
sortItems = 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
return ([NoSelector $ idToType i], nullRange) where
idToType :: Id -> Type
idToType (Id [t] [] _) = TypeToken t
idToType _ = error "idToType"
-- | a colon immediately followed by a question mark
qColonT :: AParser st Token
qColonT = asKey colonQuMark
compType :: [Id] -> [Token] -> AParser st [Component]
compType is cs = do
c <- colT
t <- parseType
return $ makeComps is (cs ++ [c]) Total t
<|> do
c <- qColonT
t <- mixType
return $ makeComps is (cs ++ [c]) Partial t where
makeComps [a] [b] k t = [Selector a k t Other $ tokPos b]
makeComps (a : r) (b : s) k t =
Selector a k t Comma (tokPos b) : makeComps r s k t
makeComps _ _ _ _ = error "makeComps: empty selector list"
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
(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))
where aAlternative = bind (\ a an -> Annoted a nullRange [] an)
alternative annos
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 :: [Id] -> [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 :: [Id] -> [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 :: Id -> AParser st OpItem
opDeclOrDefn o = do
c <- colonST
t <- typeScheme
opAttrs [o] [] c t <|> opTerm o [] nullRange c (TotalTypeScheme t)
<|> return (OpDecl [o] t [] $ tokPos c)
<|> do
(args, ps) <- opArgs
(c, st) <- typeOrTotalType
opTerm o args ps c st
data TypeOrTypeScheme = PartialType Type | TotalTypeScheme TypeScheme
-- | a 'Total' or a 'Partial' function definition type
typeOrTotalType :: AParser st (Token, TypeOrTypeScheme)
typeOrTotalType = do
c <- colT
t <- parseType
return (c, TotalTypeScheme $ simpleTypeScheme t)
<|> do
c <- qColonT
t <- mixType
return (c, PartialType t)
opTerm :: Id -> [[VarDecl]] -> Range -> Token -> TypeOrTypeScheme
-> AParser st OpItem
opTerm o as ps c st = do
e <- equalT
f <- term
let (p, sc) = case st of
PartialType t -> (Partial, simpleTypeScheme t)
TotalTypeScheme s -> (Total, s)
return $ OpDefn o as sc p f $ appRange ps $ toPos c [] e
opItem :: AParser st OpItem
opItem = do
(os, ps) <- opId `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 :: [Id] -> [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 :: Id -> 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 $ unitTypeWithRange p)
Partial f p
predItem :: AParser st OpItem
predItem = do
(os, ps) <- opId `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
(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
where aFormula = bind appendAnno
(annoParser term) lineAnnos
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 []))