content: {- |
  Module      :  ./Common/AnnoState.hs
  Description :  parsing of interspersed annotations
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Parsing of interspersed annotations
  
  - a parser state to collect annotations
  
  - parsing annoted keywords
  
  - parsing an annoted item list
  -}
  
  module Common.AnnoState where
  
  import Common.Parsec
  import Common.Lexer
  import Common.Token
  import Common.Id
  import Common.Keywords
  import Common.AS_Annotation
  import Common.AnnoParser
  
  import Text.ParserCombinators.Parsec
  
  import Data.List
  import Control.Monad
  
  -- | parsers that can collect annotations via side effects
  type AParser st = GenParser Char (AnnoState st)
  
  class AParsable a where
    aparser :: AParser st a
  
  -- used for CASL extensions. If there is no extension, just fail
  instance AParsable () where
    aparser = pzero
  
  -- a parser for terms or formulas
  class TermParser a where
    termParser :: Bool -> AParser st a -- ^ True for terms, formulas otherwise
    termParser _ = pzero
  
  instance TermParser ()
  
  aToTermParser :: AParser st a -> Bool -> AParser st a
  aToTermParser p b = if b then pzero else p
  
  -- | just the list of currently collected annotations
  data AnnoState st = AnnoState { toAnnos :: [Annotation], _userState :: st }
  
  -- | no annotations
  emptyAnnos :: st -> AnnoState st
  emptyAnnos = AnnoState []
  
  -- | add further annotations to the input state
  parseAnnos :: AnnoState a -> GenParser Char st (AnnoState a)
  parseAnnos (AnnoState as b) =
      do a <- skip >> annotations
         return $ AnnoState (as ++ a) b
  
  -- | add only annotations on consecutive lines to the input state
  parseLineAnnos :: AnnoState a -> GenParser Char st (AnnoState a)
  parseLineAnnos (AnnoState as b) =
      do l <- mLineAnnos
         return $ AnnoState (as ++ l) b
  
  -- | add annotations to the internal state
  addAnnos :: AParser st ()
  addAnnos = getState >>= parseAnnos >>= setState
  
  -- | add only annotations on consecutive lines to the internal state
  addLineAnnos :: AParser st ()
  addLineAnnos = getState >>= parseLineAnnos >>= setState
  
  {- | extract all annotation from the internal state,
  resets the internal state to 'emptyAnnos' -}
  getAnnos :: AParser st [Annotation]
  getAnnos = do
    aSt <- getState
    setState aSt { toAnnos = [] }
    return $ toAnnos aSt
  
  -- | annotations on consecutive lines
  mLineAnnos :: GenParser Char st [Annotation]
  mLineAnnos = optionL $ do
      a <- annotationL
      skipSmart
      fmap (a :) $ optionL mLineAnnos
  
  -- | explicitly parse annotations, reset internal state
  annos :: AParser st [Annotation]
  annos = addAnnos >> getAnnos
  
  -- | explicitly parse annotations on consecutive lines. reset internal state
  lineAnnos :: AParser st [Annotation]
  lineAnnos = addLineAnnos >> getAnnos
  
  -- | succeeds if the previous item is finished
  tryItemEnd :: [String] -> AParser st ()
  tryItemEnd l = try $ do
    c <- lookAhead $ annos >>
      (single (oneOf "\"([{") <|> placeS <|> scanAnySigns
       <|> many (scanLPD <|> char '_' <?> "") <?> "")
    unless (null c || elem c l) pzero
  
  {- | keywords that indicate a new item for 'tryItemEnd'.
  the quantifier exists does not start a new item. -}
  startKeyword :: [String]
  startKeyword = dotS : cDot : delete existsS casl_reserved_words
  
  -- | parse preceding annotations and the following item
  annoParser :: AParser st a -> AParser st (Annoted a)
  annoParser = liftM2 addLeftAnno annos
  
  allAnnoParser :: AParser st a -> AParser st (Annoted a)
  allAnnoParser p = liftM2 appendAnno (annoParser p) lineAnnos
  
  {- | parse preceding and consecutive trailing annotations of an item in
       between.  Unlike 'annosParser' do not treat all trailing annotations as
       preceding annotations of the next item. -}
  trailingAnnosParser :: AParser st a -> AParser st [Annoted a]
  trailingAnnosParser p = do
    l <- many1 $ allAnnoParser p
    a <- annos -- append remaining annos to last item
    return $ init l ++ [appendAnno (last l) a]
  
  -- | parse an item list preceded and followed by annotations
  annosParser :: AParser st a -> AParser st [Annoted a]
  annosParser parser =
      do a <- annos
         l <- many1 $ pair parser annos
         let ps = map fst l
             as = map snd l
             is = zipWith addLeftAnno (a : init as) ps
         return (init is ++ [appendAnno (last is) (last as)])
  
  {- | parse an item list preceded by a singular or plural keyword,
  interspersed with semicolons and an optional semicolon at the end -}
  itemList :: [String] -> String -> ([String] -> AParser st b)
                 -> ([Annoted b] -> Range -> a) -> AParser st a
  itemList ks kw ip constr =
      do p <- pluralKeyword kw
         auxItemList (ks ++ startKeyword) [p] (ip ks) constr
  
  {- | generalized version of 'itemList'
  for an other keyword list for 'tryItemEnd' and without 'pluralKeyword' -}
  auxItemList :: [String] -> [Token] -> AParser st b
              -> ([Annoted b] -> Range -> a) -> AParser st a
  auxItemList startKeywords ps parser constr = do
         (vs, ts, ans) <- itemAux startKeywords (annoParser parser)
         let r = zipWith appendAnno vs ans in
             return (constr r (catRange (ps ++ ts)))
  
  -- | parse an item list without a starting keyword
  itemAux :: [String] -> AParser st a
          -> AParser st ([a], [Token], [[Annotation]])
  itemAux startKeywords itemParser =
      do a <- itemParser
         (m, an) <- optSemi
         let r = return ([a], [], [an])
         (tryItemEnd startKeywords >> r) <|>
            do (ergs, ts, ans) <- itemAux startKeywords itemParser
               return (a : ergs, m ++ ts, an : ans)
  
  -- | collect preceding and trailing annotations
  wrapAnnos :: AParser st a -> AParser st a
  wrapAnnos p = try (addAnnos >> p) << addAnnos
  
  -- | parse an annoted keyword
  asKey :: String -> AParser st Token
  asKey = wrapAnnos . pToken . toKey
  
  -- * annoted keywords
  
  anComma :: AParser st Token
  anComma = wrapAnnos commaT
  
  anSemi :: AParser st Token
  anSemi = wrapAnnos semiT
  
  semiOrComma :: CharParser st Token
  semiOrComma = semiT <|> commaT
  
  anSemiOrComma :: AParser st Token
  anSemiOrComma = wrapAnnos semiOrComma << addLineAnnos
  
  -- | check for a semicolon beyond annotations
  trySemi :: AParser st Token
  trySemi = try $ addAnnos >> semiT
  
  -- | check for a semicolon or comma beyond annotations and trailing line annos
  trySemiOrComma :: AParser st Token
  trySemiOrComma = try (addAnnos >> semiOrComma) << addLineAnnos
  
  -- | optional semicolon followed by annotations on consecutive lines
  optSemi :: AParser st ([Token], [Annotation])
  optSemi = do
      s <- trySemi
      a1 <- getAnnos
      a2 <- lineAnnos
      return ([s], a1 ++ a2)
    <|> do
      a <- lineAnnos
      return ([], a)
  
  equalT :: AParser st Token
  equalT = wrapAnnos $ pToken $ reserved [exEqual]
           (choice (map (keySign . string) [exEqual, equalS]) <?> show equalS)
  
  colonT :: AParser st Token
  colonT = asKey colonS
  
  equiT :: AParser st Token
  equiT = asKey equiS
  
  lessT :: AParser st Token
  lessT = asKey lessS
  
  dotT :: AParser st Token
  dotT = asKey dotS <|> asKey cDot <?> show dotS
  
  asT :: AParser st Token
  asT = asKey asS
  
  barT :: AParser st Token
  barT = asKey barS
  
  forallT :: AParser st Token
  forallT = asKey forallS
  