e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski{- |

0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiModule : $Header$

0095c7efbddd0ffeed6aaf8ec015346be161d819Till MossakowskiDescription : parser for HasCASL basic Items

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2005

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiLicense : GPLv2 or higher, see LICENSE.txt

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiMaintainer : Christian.Maeder@dfki.de

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiStability : provisional

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill MossakowskiPortability : portable

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiparser for HasCASL basic Items

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-}

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskimodule HasCASL.ParseItem (basicItems, basicSpec) where

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Text.ParserCombinators.Parsec

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.AS_Annotation

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.AnnoState

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Id

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Keywords

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Lexer

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Parsec

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport Common.Token

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.As

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.AsUtils

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.HToken

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowskiimport HasCASL.ParseTerm

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowskiimport Control.Monad

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski-- * adapted item list parser (using 'itemAux')

be408ef9713fbbbaf7bde82618f7d3f204fe806cTill Mossakowski

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskihasCaslItemList :: String -> AParser st b

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski -> ([Annoted b] -> Range -> a) -> AParser st a

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskihasCaslItemList kw ip constr = do

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski p <- pluralKeyword kw

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski auxItemList hasCaslStartKeywords [p] ip constr

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski

7474388b4c2236f8ab2327289555000268c7901aTill MossakowskihasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a)

7474388b4c2236f8ab2327289555000268c7901aTill Mossakowski -> AParser st a

7474388b4c2236f8ab2327289555000268c7901aTill MossakowskihasCaslItemAux = auxItemList hasCaslStartKeywords

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski-- * parsing type items

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskicommaTypeDecl :: TypePattern -> AParser st TypeItem

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till MossakowskicommaTypeDecl s = do

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski c <- anComma

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski (is, cs) <- typePattern `separatedBy` anComma

e687bd70d6e6c98d82b239e01fef4a60de6739f4Till Mossakowski let l = s : is

4918e2f622cfb96f9a57b7617cd18ca7e4f8b5d4Christian Maeder 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)