{- HetCATS/CASL/ItemList.hs

$Id$

Authors: Christian Maeder

Year: 2002

generically parse "<keyword>/<keywords> ITEM ; ... ; ITEM"

-}

module CASL.ItemList where

import Common.AnnoState

import Common.Id

import Common.Keywords

import Common.Lexer

import Common.AS_Annotation

import Data.Maybe

import Common.Lib.Parsec

import Common.Token

import Data.List(delete)

wrapAnnos :: AParser a -> AParser a

wrapAnnos p = try (addAnnos >> p) << addAnnos

asKey :: String -> AParser Token

asKey s = wrapAnnos $ pToken $ toKey s

anComma, commaT, anSemi, semiT :: AParser Token

anComma = wrapAnnos Common.Lexer.commaT

commaT = anComma

anSemi = wrapAnnos Common.Lexer.semiT

semiT = anSemi

equalT, colonT, lessT, dotT :: AParser Token

equalT = asKey equalS

colonT = asKey colonS

lessT = asKey lessS

dotT = try(asKey dotS <|> asKey cDot) <?> "dot"

asT, barT, forallT :: AParser Token

asT = asKey asS

barT = asKey barS

forallT = asKey forallS

-- ----------------------------------------------

-- annotations

-- ----------------------------------------------

annos, lineAnnos :: AParser [Annotation]

annos = addAnnos >> getAnnos

lineAnnos = addLineAnnos >> getAnnos

-- optional semicolon followed by annotations on the same line

optSemi :: AParser (Maybe Token, [Annotation])

optSemi = do (a1, s) <- try $ bind (,) annos Common.Lexer.semiT

a2 <- lineAnnos

return (Just s, a1 ++ a2)

<|> do a <- lineAnnos

return (Nothing, a)

-- succeeds if an item is not continued after a semicolon

tryItemEnd :: [String] -> AParser ()

tryItemEnd l =

try (do c <- lookAhead (annos >>

(single (oneOf "\"([{")

<|> placeS

<|> scanAnySigns

<|> many scanLPD))

if null c || c `elem` l then return () else unexpected c)

-- remove quantifier exists from casl_reserved_word

-- because it may start a formula in "axiom/axioms ... \;"

startKeyword :: [String]

startKeyword = dotS:cDot:

(delete existsS casl_reserved_words)

appendAnno :: Annoted a -> [Annotation] -> Annoted a

appendAnno (Annoted x p l r) y = Annoted x p l (r++y)

addLeftAnno :: [Annotation] -> a -> Annoted a

addLeftAnno l i = Annoted i [] l []

annoParser :: AParser a

-> AParser (Annoted a)

annoParser parser = bind addLeftAnno annos parser

annosParser :: AParser a

-> AParser [Annoted a]

annosParser parser =

do is <- many1 $ try $ annoParser parser

a <- annos

return (init is ++ [appendAnno (last is) a])

itemList :: String -> AParser b

-> ([Annoted b] -> [Pos] -> a) -> AParser a

itemList = auxItemList startKeyword

auxItemList :: [String] -> String -> AParser b

-> ([Annoted b] -> [Pos] -> a) -> AParser a

auxItemList startKeywords keyword parser constr =

do p <- pluralKeyword keyword

(vs, ts, ans) <- itemAux startKeywords (annoParser parser)

let r = zipWith appendAnno vs ans in

return (constr r (map tokPos (p:ts)))

itemAux :: [String] -> AParser a

-> AParser ([a], [Token], [[Annotation]])

itemAux startKeywords itemParser =

do a <- itemParser

(m, an) <- optSemi

case m of Nothing -> return ([a], [], [an])

Just t -> do tryItemEnd startKeywords

return ([a], [t], [an])

<|>

do (as, ts, ans) <- itemAux startKeywords itemParser

return (a:as, t:ts, an:ans)