content: {- |
  Module      :  ./LF/Parse.hs
  Description :  A parser for the Edinburgh Logical Framework
  Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  k.sojakova@jacobs-university.de
  Stability   :  experimental
  Portability :  portable
  -}
  
  module LF.Parse
         ( basicSpec
         , symbItems
         , symbMapItems
         ) where
  
  import Text.ParserCombinators.Parsec
  
  import Common.Parsec
  import Common.AnnoState
  import Common.Lexer
  import Common.Token
  import Common.Keywords
  import Common.GlobalAnnotations (PrefixMap)
  
  import Data.Char
  
  import LF.AS
  
  basicSpec :: PrefixMap -> AParser st BASIC_SPEC
  basicSpec _ =
    fmap Basic_spec (trailingAnnosParser basicItem)
    <|>
    (oBraceT >> cBraceT >> return (Basic_spec []))
  
  basicItem :: AParser st BASIC_ITEM
  basicItem =
   do d <- tokensP twelfMultDeclChars
      dotT
      return $ Decl $ trim d
   <|>
   do dotT
      f <- tokensP twelfMultDeclChars
      return $ Form $ trim f
  
  tokenP :: String -> AParser st String
  tokenP chars = reserved criticalKeywords $
     many1 $ scanLPD <|> oneOf chars
  
  tokensP :: String -> AParser st String
  tokensP chars = do
    ss <- many1 (tokenP chars <|> whitesp)
    return $ concat ss
  
  whitesp :: AParser st String
  whitesp = many1 $ oneOf whiteChars
  
  symbItems :: AParser st SYMB_ITEMS
  symbItems = fmap (Symb_items . fst) $
     tokenP twelfSymChars `separatedBy` anComma
  
  symbMapItems :: AParser st SYMB_MAP_ITEMS
  symbMapItems = fmap (Symb_map_items . fst) $
    symbOrMap `separatedBy` anComma
  
  symbOrMap :: AParser st SYMB_OR_MAP
  symbOrMap = do
    s <- tokenP twelfSymChars
    (do asKey mapsTo
        t <- tokensP twelfDeclChars
        return $ Symb_map s $ trim t)
      <|>
      return (Symb s)
  
  trim :: String -> String
  trim = let f = reverse . dropWhile isSpace
             in f . f
  