AnnoState.hs revision bcd914850de931848b86d7728192a149f9c0108b
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder{- |
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederModule : $Header$
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederDescription : parsing of interspersed annotations
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederMaintainer : Christian.Maeder@dfki.de
d31090850b029162859d0aedf45bae2a83d7b673Jonathan von SchroederStability : provisional
d31090850b029162859d0aedf45bae2a83d7b673Jonathan von SchroederPortability : portable
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederParsing of interspersed annotations
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder- a parser state to collect annotations
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder- parsing annoted keywords
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder- parsing an annoted item list
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-}
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroedermodule Common.AnnoState where
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroederimport Common.Parsec
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Lexer
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Token
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Id
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederimport Common.Keywords
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroederimport Common.AS_Annotation
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederimport Common.AnnoParser
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroederimport Text.ParserCombinators.Parsec
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederimport Data.List
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederimport Control.Monad
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder-- | parsers that can collect annotations via side effects
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroedertype AParser st = GenParser Char (AnnoState st)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroederclass AParsable a where
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder aparser :: AParser st a
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder-- used for CASL extensions. If there is no extension, just fail
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroederinstance AParsable () where
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder aparser = pzero
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- a parser for terms or formulas
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroederclass TermParser a where
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder termParser :: Bool -> AParser st a -- ^ True for terms, formulas otherwise
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder termParser _ = pzero
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroederinstance TermParser ()
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederaToTermParser :: AParser st a -> Bool -> AParser st a
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von SchroederaToTermParser p b = if b then pzero else p
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | just the list of currently collected annotations
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederdata AnnoState st = AnnoState { toAnnos :: [Annotation], _userState :: st }
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder-- | no annotations
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederemptyAnnos :: st -> AnnoState st
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederemptyAnnos = AnnoState []
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder-- | add further annotations to the input state
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederparseAnnos :: AnnoState a -> GenParser Char st (AnnoState a)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederparseAnnos (AnnoState as b) =
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder do a <- skip >> annotations
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder return $ AnnoState (as ++ a) b
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | add only annotations on consecutive lines to the input state
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederparseLineAnnos :: AnnoState a -> GenParser Char st (AnnoState a)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederparseLineAnnos (AnnoState as b) =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder do l <- mLineAnnos
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder return $ AnnoState (as ++ l) b
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder-- | add annotations to the internal state
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederaddAnnos :: AParser st ()
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von SchroederaddAnnos = getState >>= parseAnnos >>= setState
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder-- | add only annotations on consecutive lines to the internal state
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederaddLineAnnos :: AParser st ()
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederaddLineAnnos = getState >>= parseLineAnnos >>= setState
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder{- | extract all annotation from the internal state,
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroederresets the internal state to 'emptyAnnos' -}
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroedergetAnnos :: AParser st [Annotation]
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroedergetAnnos = do
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder aSt <- getState
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder setState aSt { toAnnos = [] }
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder return $ toAnnos aSt
f34d3f5bda0be3ded217da71c1e2e30ee03ca5a1Jonathan von Schroeder
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder-- | annotations on consecutive lines
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von SchroedermLineAnnos :: GenParser Char st [Annotation]
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von SchroedermLineAnnos = optionL $ do
d40eeef0175161a089443ba027dcb635ed11a1bdJonathan von Schroeder a <- annotationL
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder skipSmart
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder fmap (a :) $ optionL mLineAnnos
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder-- | explicitly parse annotations, reset internal state
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroederannos :: AParser st [Annotation]
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroederannos = addAnnos >> getAnnos
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder-- | explicitly parse annotations on consecutive lines. reset internal state
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederlineAnnos :: AParser st [Annotation]
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von SchroederlineAnnos = addLineAnnos >> getAnnos
59bed9a19a4646b44b7e837f5f9ab35183833d3bJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | succeeds if the previous item is finished
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroedertryItemEnd :: [String] -> AParser st ()
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von SchroedertryItemEnd l = try $ do
b2ffbb0cced4c2e4cc1ec3266847881a17f32d34Jonathan von Schroeder c <- lookAhead $ annos >>
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (single (oneOf "\"([{") <|> placeS <|> scanAnySigns
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder <|> many (scanLPD <|> char '_' <?> "") <?> "")
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder unless (null c || elem c l) pzero
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder{- | keywords that indicate a new item for 'tryItemEnd'.
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederthe quantifier exists does not start a new item. -}
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von SchroederstartKeyword :: [String]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederstartKeyword = dotS : cDot : delete existsS casl_reserved_words
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder-- | parse preceding annotations and the following item
4cd542a7f4e378ab5a36b49da804b258442b13f9Jonathan von SchroederannoParser :: AParser st a -> AParser st (Annoted a)
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederannoParser = liftM2 addLeftAnno annos
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederallAnnoParser :: AParser st a -> AParser st (Annoted a)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederallAnnoParser p = liftM2 appendAnno (annoParser p) lineAnnos
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder{- | parse preceding and consecutive trailing annotations of an item in
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder between. Unlike 'annosParser' do not treat all trailing annotations as
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder preceding annotations of the next item. -}
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroedertrailingAnnosParser :: AParser st a -> AParser st [Annoted a]
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von SchroedertrailingAnnosParser p = do
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder l <- many1 $ allAnnoParser p
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder a <- annos -- append remaining annos to last item
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder return $ init l ++ [appendAnno (last l) a]
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder
383d883a81d3bc4ad7b14aa28e03f0f35baec458Jonathan von Schroeder-- | parse an item list preceded and followed by annotations
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederannosParser :: AParser st a -> AParser st [Annoted a]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von SchroederannosParser parser =
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder do a <- annos
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder l <- many1 $ pair parser annos
04c0a723a860a503c95eecd988cd9c25fa827f3eJonathan von Schroeder let ps = map fst l
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder as = map snd l
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder is = zipWith addLeftAnno (a : init as) ps
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder return (init is ++ [appendAnno (last is) (last as)])
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder{- | parse an item list preceded by a singular or plural keyword,
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroederinterspersed with semicolons and an optional semicolon at the end -}
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederitemList :: [String] -> String -> ([String] -> AParser st b)
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder -> ([Annoted b] -> Range -> a) -> AParser st a
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederitemList ks kw ip constr =
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder do p <- pluralKeyword kw
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder auxItemList (ks ++ startKeyword) [p] (ip ks) constr
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder{- | generalized version of 'itemList'
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroederfor an other keyword list for 'tryItemEnd' and without 'pluralKeyword' -}
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederauxItemList :: [String] -> [Token] -> AParser st b
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder -> ([Annoted b] -> Range -> a) -> AParser st a
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von SchroederauxItemList startKeywords ps parser constr = do
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroeder (vs, ts, ans) <- itemAux startKeywords (annoParser parser)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let r = zipWith appendAnno vs ans in
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder return (constr r (catRange (ps ++ ts)))
74461cfd2fb547267eebd25b91a0f7d1658ca046Jonathan von Schroeder
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder-- | parse an item list without a starting keyword
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederitemAux :: [String] -> AParser st a
19c90cc887b417cf16faddf8595029e46dd37c7eJonathan von Schroeder -> AParser st ([a], [Token], [[Annotation]])
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von SchroederitemAux startKeywords itemParser =
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder do a <- itemParser
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (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
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