{- |

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