{- |
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 :: PrefixMap -> AParser st BASIC_SPEC
basicSpec _ =
  ([Annoted BASIC_ITEM] -> BASIC_SPEC)
-> ParsecT [Char] (AnnoState st) Identity [Annoted BASIC_ITEM]
-> AParser st BASIC_SPEC
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec (AParser st BASIC_ITEM
-> ParsecT [Char] (AnnoState st) Identity [Annoted BASIC_ITEM]
forall st a. AParser st a -> AParser st [Annoted a]
trailingAnnosParser AParser st BASIC_ITEM
forall st. AParser st BASIC_ITEM
basicItem)
  AParser st BASIC_SPEC
-> AParser st BASIC_SPEC -> AParser st BASIC_SPEC
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
  (CharParser (AnnoState st) Token
forall st. CharParser st Token
oBraceT CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CharParser (AnnoState st) Token
forall st. CharParser st Token
cBraceT CharParser (AnnoState st) Token
-> AParser st BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BASIC_SPEC -> AParser st BASIC_SPEC
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted BASIC_ITEM] -> BASIC_SPEC
Basic_spec []))

basicItem :: AParser st BASIC_ITEM
basicItem :: AParser st BASIC_ITEM
basicItem =
 do [Char]
d <- [Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokensP [Char]
twelfMultDeclChars
    AParser st Token
forall st. AParser st Token
dotT
    BASIC_ITEM -> AParser st BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEM -> AParser st BASIC_ITEM)
-> BASIC_ITEM -> AParser st BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Char] -> BASIC_ITEM
Decl ([Char] -> BASIC_ITEM) -> [Char] -> BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
trim [Char]
d
 AParser st BASIC_ITEM
-> AParser st BASIC_ITEM -> AParser st BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
 do AParser st Token
forall st. AParser st Token
dotT
    [Char]
f <- [Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokensP [Char]
twelfMultDeclChars
    BASIC_ITEM -> AParser st BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (BASIC_ITEM -> AParser st BASIC_ITEM)
-> BASIC_ITEM -> AParser st BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Char] -> BASIC_ITEM
Form ([Char] -> BASIC_ITEM) -> [Char] -> BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
trim [Char]
f

tokenP :: String -> AParser st String
tokenP :: [Char] -> AParser st [Char]
tokenP chars :: [Char]
chars = [[Char]] -> AParser st [Char] -> AParser st [Char]
forall st. [[Char]] -> CharParser st [Char] -> CharParser st [Char]
reserved [[Char]]
criticalKeywords (AParser st [Char] -> AParser st [Char])
-> AParser st [Char] -> AParser st [Char]
forall a b. (a -> b) -> a -> b
$
   ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char])
-> ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char]
forall a b. (a -> b) -> a -> b
$ ParsecT [Char] (AnnoState st) Identity Char
forall st. CharParser st Char
scanLPD ParsecT [Char] (AnnoState st) Identity Char
-> ParsecT [Char] (AnnoState st) Identity Char
-> ParsecT [Char] (AnnoState st) Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Char] -> ParsecT [Char] (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf [Char]
chars

tokensP :: String -> AParser st String
tokensP :: [Char] -> AParser st [Char]
tokensP chars :: [Char]
chars = do
  [[Char]]
ss <- AParser st [Char]
-> ParsecT [Char] (AnnoState st) Identity [[Char]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ([Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokenP [Char]
chars AParser st [Char] -> AParser st [Char] -> AParser st [Char]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st [Char]
forall st. AParser st [Char]
whitesp)
  [Char] -> AParser st [Char]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> AParser st [Char]) -> [Char] -> AParser st [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Char]]
ss

whitesp :: AParser st String
whitesp :: AParser st [Char]
whitesp = ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char])
-> ParsecT [Char] (AnnoState st) Identity Char -> AParser st [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> ParsecT [Char] (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
[Char] -> ParsecT s u m Char
oneOf [Char]
whiteChars

symbItems :: AParser st SYMB_ITEMS
symbItems :: AParser st SYMB_ITEMS
symbItems = (([[Char]], [Token]) -> SYMB_ITEMS)
-> ParsecT [Char] (AnnoState st) Identity ([[Char]], [Token])
-> AParser st SYMB_ITEMS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([[Char]] -> SYMB_ITEMS
Symb_items ([[Char]] -> SYMB_ITEMS)
-> (([[Char]], [Token]) -> [[Char]])
-> ([[Char]], [Token])
-> SYMB_ITEMS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[Char]], [Token]) -> [[Char]]
forall a b. (a, b) -> a
fst) (ParsecT [Char] (AnnoState st) Identity ([[Char]], [Token])
 -> AParser st SYMB_ITEMS)
-> ParsecT [Char] (AnnoState st) Identity ([[Char]], [Token])
-> AParser st SYMB_ITEMS
forall a b. (a -> b) -> a -> b
$
   [Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokenP [Char]
twelfSymChars AParser st [Char]
-> GenParser Char (AnnoState st) Token
-> ParsecT [Char] (AnnoState st) Identity ([[Char]], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
anComma

symbMapItems :: AParser st SYMB_MAP_ITEMS
symbMapItems :: AParser st SYMB_MAP_ITEMS
symbMapItems = (([SYMB_OR_MAP], [Token]) -> SYMB_MAP_ITEMS)
-> ParsecT [Char] (AnnoState st) Identity ([SYMB_OR_MAP], [Token])
-> AParser st SYMB_MAP_ITEMS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([SYMB_OR_MAP] -> SYMB_MAP_ITEMS
Symb_map_items ([SYMB_OR_MAP] -> SYMB_MAP_ITEMS)
-> (([SYMB_OR_MAP], [Token]) -> [SYMB_OR_MAP])
-> ([SYMB_OR_MAP], [Token])
-> SYMB_MAP_ITEMS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SYMB_OR_MAP], [Token]) -> [SYMB_OR_MAP]
forall a b. (a, b) -> a
fst) (ParsecT [Char] (AnnoState st) Identity ([SYMB_OR_MAP], [Token])
 -> AParser st SYMB_MAP_ITEMS)
-> ParsecT [Char] (AnnoState st) Identity ([SYMB_OR_MAP], [Token])
-> AParser st SYMB_MAP_ITEMS
forall a b. (a -> b) -> a -> b
$
  AParser st SYMB_OR_MAP
forall st. AParser st SYMB_OR_MAP
symbOrMap AParser st SYMB_OR_MAP
-> GenParser Char (AnnoState st) Token
-> ParsecT [Char] (AnnoState st) Identity ([SYMB_OR_MAP], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` GenParser Char (AnnoState st) Token
forall st. AParser st Token
anComma

symbOrMap :: AParser st SYMB_OR_MAP
symbOrMap :: AParser st SYMB_OR_MAP
symbOrMap = do
  [Char]
s <- [Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokenP [Char]
twelfSymChars
  (do [Char] -> AParser st Token
forall st. [Char] -> AParser st Token
asKey [Char]
mapsTo
      [Char]
t <- [Char] -> AParser st [Char]
forall st. [Char] -> AParser st [Char]
tokensP [Char]
twelfDeclChars
      SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return (SYMB_OR_MAP -> AParser st SYMB_OR_MAP)
-> SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> SYMB_OR_MAP
Symb_map [Char]
s ([Char] -> SYMB_OR_MAP) -> [Char] -> SYMB_OR_MAP
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
trim [Char]
t)
    AParser st SYMB_OR_MAP
-> AParser st SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    SYMB_OR_MAP -> AParser st SYMB_OR_MAP
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> SYMB_OR_MAP
Symb [Char]
s)

trim :: String -> String
trim :: [Char] -> [Char]
trim = let f :: [Char] -> [Char]
f = [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace
           in [Char] -> [Char]
f ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
f