{- |
Module : ./HasCASL/ParseItem.hs
Description : parser for HasCASL basic Items
Copyright : (c) Christian Maeder and Uni Bremen 2002-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
parser for HasCASL basic Items
-}
module HasCASL.ParseItem (basicItems, basicSpec) where
import Common.AS_Annotation
import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.HToken
import HasCASL.ParseTerm
import Control.Monad
-- * adapted item list parser (using 'itemAux')
hasCaslItemList :: String -> AParser st b
-> ([Annoted b] -> Range -> a) -> AParser st a
hasCaslItemList kw ip constr = do
p <- pluralKeyword kw
auxItemList hasCaslStartKeywords [p] ip constr
hasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)
-> AParser st a
hasCaslItemAux = auxItemList hasCaslStartKeywords
-- * parsing type items
commaTypeDecl :: TypePattern -> AParser st TypeItem
commaTypeDecl s = do
c <- anComma
(is, cs) <- typePattern `separatedBy` anComma
let l = s : is
p = c : cs
subTypeDecl (l, p) <|> kindedTypeDecl (l, p)
<|> return (TypeDecl l universe $ catRange p)
kindedTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
kindedTypeDecl (l, p) = do
t <- colT
s <- kind
let d = TypeDecl l s $ catRange $ p ++ [t]
case l of
[hd] -> pseudoTypeDef hd (Just s) [t] <|> dataDef hd s [t] <|> return d
_ -> return d
isoDecl :: TypePattern -> AParser st TypeItem
isoDecl s = do
e <- equalT
subTypeDefn (s, e) <|> do
(l, p) <- typePattern `separatedBy` equalT
return $ IsoDecl (s : l) $ catRange $ e : p
vars :: AParser st Vars
vars = fmap Var var <|> do
o <- oParenT
(vs, ps) <- vars `separatedBy` anComma
c <- cParenT
return $ VarTuple vs $ toRange o ps c
subTypeDefn :: (TypePattern, Token) -> AParser st TypeItem
subTypeDefn (s, e) = do
a <- annos
o <- oBraceT << addAnnos
v <- vars
c <- colT
t <- parseType
d <- dotT -- or bar
f <- term
a2 <- annos
p <- cBraceT
let qs = toRange e [o, c, d] p
return $ SubtypeDefn s v t (Annoted f qs a a2) qs
subTypeDecl :: ([TypePattern], [Token]) -> AParser st TypeItem
subTypeDecl (l, p) = do
t <- lessT
s <- parseType
return $ SubtypeDecl l s $ catRange $ p ++ [t]
sortItem :: AParser st TypeItem
sortItem = do
s <- typePattern
subTypeDecl ([s], [])
<|> kindedTypeDecl ([s], [])
<|> commaTypeDecl s
<|> 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 = hasCaslItemAux ps typeItem . TypeItems
typeItems :: AParser st SigItems
typeItems = do
p <- pluralKeyword typeS
do q <- pluralKeyword instanceS
typeItemList [p, q] Instance
<|> typeItemList [p] Plain
pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
pseudoTypeDef t k l = do
c <- asKey assignS
p <- parseType
return $ AliasType t k (simpleTypeScheme p) $ catRange $ 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 $ catRange $ 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 = liftM2 (\ i -> Annoted i nullRange [])
alternative annos
(Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT
let aa = Annoted v nullRange a b : as
qs = catRange $ l ++ c : ps
do d <- asKey derivingS
(cs, cps) <- classId `separatedBy` anComma
return $ Datatype $ DatatypeDecl t k aa cs
$ appRange qs $ appRange (tokPos d) $ catRange 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) $ pair (single $ lessT <|> colonT) kind
return $ ClassDecl is k $ catRange $ cs ++ ps
classItem :: AParser st ClassItem
classItem = do
c <- classDecl
do o <- oBraceT
is <- annosParser basicItems
p <- cBraceT
return $ ClassItem c is $ toRange o [] p
<|> return (ClassItem c [] nullRange)
classItemList :: [Token] -> Instance -> AParser st BasicItem
classItemList ps = hasCaslItemAux ps classItem . ClassItems
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
multiTypeScheme :: [PolyId] -> AParser st TypeScheme
multiTypeScheme os = case os of
p : r -> if null r || all ( \ (PolyId _ tys _) -> null tys) os
then typeScheme p
else fail $ "instantiation list in identifier list: "
++ show (map ( \ (PolyId i _ _) -> i) os)
_ -> error "HasCASL.ParseItem.opDecl"
opDecl :: [PolyId] -> [Token] -> AParser st OpItem
opDecl os ps = do
c <- colonST
t <- multiTypeScheme os
opAttrs os ps c t <|> return (OpDecl os t [] $ catRange $ 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 $ catRange $ 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 o
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 $ toRange 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 <- multiTypeScheme os
let p = catRange $ 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 $ toRange g [o] c
genVarItems :: AParser st ([GenVarDecl], [Token])
genVarItems = do
vs <- genVarDecls
do s <- trySemi << 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 (catRange $ f : ps) ds
genVarItem :: AParser st BasicItem
genVarItem = do
v <- pluralKeyword varS
(vs, ps) <- genVarItems
return $ GenVarItems vs $ catRange $ v : ps
dotFormulae :: AParser st BasicItem
dotFormulae = do
d <- dotT
(fs, ds) <- allAnnoParser term `separatedBy` dotT
let ps = catRange $ d : ds
lst = last fs
if null $ r_annos lst then do
(m, an) <- optSemi
return $ AxiomItems [] (init fs ++ [appendAnno lst an]) $ appRange ps
$ catRange 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 $ toRange 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)