{- |
Module      :  ./HasCASL/SymbItem.hs
Description :  parsing symbol items
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

HasCASL parsable symbol items for structured specs
-}

module HasCASL.SymbItem where

import Common.Id
import Common.Token (colonST)
import Common.Keywords
import Common.Lexer
import Common.AnnoState
import qualified Control.Monad.Fail as Fail
import Text.ParserCombinators.Parsec

import HasCASL.ParseTerm
import HasCASL.As

-- * parsers for symbols

-- | parse a (typed) symbol
symb :: AParser st Symb
symb :: AParser st Symb
symb = do
    p :: PolyId
p@(PolyId i :: Id
i tys :: [TypeArg]
tys _) <- AParser st PolyId
forall st. AParser st PolyId
parsePolyId
    do Token
c <- GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
colonST
       TypeScheme
sc <- PolyId -> AParser st TypeScheme
forall st. PolyId -> AParser st TypeScheme
typeScheme PolyId
p
       Symb -> AParser st Symb
forall (m :: * -> *) a. Monad m => a -> m a
return (Symb -> AParser st Symb) -> Symb -> AParser st Symb
forall a b. (a -> b) -> a -> b
$ Id -> Maybe SymbType -> Range -> Symb
Symb Id
i (SymbType -> Maybe SymbType
forall a. a -> Maybe a
Just (SymbType -> Maybe SymbType) -> SymbType -> Maybe SymbType
forall a b. (a -> b) -> a -> b
$ TypeScheme -> SymbType
SymbType TypeScheme
sc) (Range -> Symb) -> Range -> Symb
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
c
      AParser st Symb -> AParser st Symb -> AParser st Symb
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> if [TypeArg] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeArg]
tys then Symb -> AParser st Symb
forall (m :: * -> *) a. Monad m => a -> m a
return (Symb -> AParser st Symb) -> Symb -> AParser st Symb
forall a b. (a -> b) -> a -> b
$ Id -> Maybe SymbType -> Range -> Symb
Symb Id
i Maybe SymbType
forall a. Maybe a
Nothing (Range -> Symb) -> Range -> Symb
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
i else
          String -> AParser st Symb
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("bound type variables for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
i "' without type")

-- | parse a mapped symbol
symbMap :: AParser st SymbOrMap
symbMap :: AParser st SymbOrMap
symbMap = do
    Symb
s <- AParser st Symb
forall st. AParser st Symb
symb
    do Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
mapsTo
       ParsecT String (AnnoState st) Identity (SymbKind, Token)
-> ParsecT String (AnnoState st) Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional ParsecT String (AnnoState st) Identity (SymbKind, Token)
forall st. AParser st (SymbKind, Token)
symbKind
       Symb
t <- AParser st Symb
forall st. AParser st Symb
symb
       SymbOrMap -> AParser st SymbOrMap
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbOrMap -> AParser st SymbOrMap)
-> SymbOrMap -> AParser st SymbOrMap
forall a b. (a -> b) -> a -> b
$ Symb -> Maybe Symb -> Range -> SymbOrMap
SymbOrMap Symb
s (Symb -> Maybe Symb
forall a. a -> Maybe a
Just Symb
t) (Range -> SymbOrMap) -> Range -> SymbOrMap
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
f
      AParser st SymbOrMap
-> AParser st SymbOrMap -> AParser st SymbOrMap
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SymbOrMap -> AParser st SymbOrMap
forall (m :: * -> *) a. Monad m => a -> m a
return (Symb -> Maybe Symb -> Range -> SymbOrMap
SymbOrMap Symb
s Maybe Symb
forall a. Maybe a
Nothing Range
nullRange)

-- | parse kind of symbols
symbKind :: AParser st (SymbKind, Token)
symbKind :: AParser st (SymbKind, Token)
symbKind = [AParser st (SymbKind, Token)] -> AParser st (SymbKind, Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((SymbKind -> AParser st (SymbKind, Token))
-> [SymbKind] -> [AParser st (SymbKind, Token)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ k :: SymbKind
k -> do
   Token
q <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword (String -> CharParser (AnnoState st) Token)
-> String -> CharParser (AnnoState st) Token
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop 3 (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ SymbKind -> String
forall a. Show a => a -> String
show SymbKind
k
   (SymbKind, Token) -> AParser st (SymbKind, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbKind
k, Token
q)) [SymbKind
SyKop, SymbKind
SyKfun, SymbKind
SyKpred, SymbKind
SyKtype, SymbKind
SyKsort])
  AParser st (SymbKind, Token)
-> AParser st (SymbKind, Token) -> AParser st (SymbKind, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
q <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey (String
classS String -> String -> String
forall a. [a] -> [a] -> [a]
++ "es") CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
classS
    (SymbKind, Token) -> AParser st (SymbKind, Token)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbKind
SyKclass, Token
q)
  AParser st (SymbKind, Token)
-> String -> AParser st (SymbKind, Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "kind"

-- | parse symbol items
symbItems :: AParser st SymbItems
symbItems :: AParser st SymbItems
symbItems = do
    Symb
s <- AParser st Symb
forall st. AParser st Symb
symb
    SymbItems -> AParser st SymbItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbItems -> AParser st SymbItems)
-> SymbItems -> AParser st SymbItems
forall a b. (a -> b) -> a -> b
$ SymbKind -> [Symb] -> [Annotation] -> Range -> SymbItems
SymbItems SymbKind
Implicit [Symb
s] [] Range
nullRange
  AParser st SymbItems
-> AParser st SymbItems -> AParser st SymbItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (k :: SymbKind
k, p :: Token
p) <- AParser st (SymbKind, Token)
forall st. AParser st (SymbKind, Token)
symbKind
    (is :: [Symb]
is, ps :: [Token]
ps) <- AParser st ([Symb], [Token])
forall st. AParser st ([Symb], [Token])
symbs
    SymbItems -> AParser st SymbItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbItems -> AParser st SymbItems)
-> SymbItems -> AParser st SymbItems
forall a b. (a -> b) -> a -> b
$ SymbKind -> [Symb] -> [Annotation] -> Range -> SymbItems
SymbItems SymbKind
k [Symb]
is [] (Range -> SymbItems) -> Range -> SymbItems
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
p Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

symbs :: AParser st ([Symb], [Token])
symbs :: AParser st ([Symb], [Token])
symbs = do
    Symb
s <- AParser st Symb
forall st. AParser st Symb
symb
    do Token
c <- AParser st Token
forall st. AParser st Token
anComma AParser st Token -> AParser st Symb -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` AParser st Symb
forall st. AParser st Symb
symb
       (is :: [Symb]
is, ps :: [Token]
ps) <- AParser st ([Symb], [Token])
forall st. AParser st ([Symb], [Token])
symbs
       ([Symb], [Token]) -> AParser st ([Symb], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (Symb
s Symb -> [Symb] -> [Symb]
forall a. a -> [a] -> [a]
: [Symb]
is, Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
      AParser st ([Symb], [Token])
-> AParser st ([Symb], [Token]) -> AParser st ([Symb], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Symb], [Token]) -> AParser st ([Symb], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symb
s], [])

-- | parse symbol mappings
symbMapItems :: AParser st SymbMapItems
symbMapItems :: AParser st SymbMapItems
symbMapItems = do
    SymbOrMap
s <- AParser st SymbOrMap
forall st. AParser st SymbOrMap
symbMap
    SymbMapItems -> AParser st SymbMapItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbMapItems -> AParser st SymbMapItems)
-> SymbMapItems -> AParser st SymbMapItems
forall a b. (a -> b) -> a -> b
$ SymbKind -> [SymbOrMap] -> [Annotation] -> Range -> SymbMapItems
SymbMapItems SymbKind
Implicit [SymbOrMap
s] [] Range
nullRange
  AParser st SymbMapItems
-> AParser st SymbMapItems -> AParser st SymbMapItems
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (k :: SymbKind
k, p :: Token
p) <- AParser st (SymbKind, Token)
forall st. AParser st (SymbKind, Token)
symbKind
    (is :: [SymbOrMap]
is, ps :: [Token]
ps) <- AParser st ([SymbOrMap], [Token])
forall st. AParser st ([SymbOrMap], [Token])
symbMaps
    SymbMapItems -> AParser st SymbMapItems
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbMapItems -> AParser st SymbMapItems)
-> SymbMapItems -> AParser st SymbMapItems
forall a b. (a -> b) -> a -> b
$ SymbKind -> [SymbOrMap] -> [Annotation] -> Range -> SymbMapItems
SymbMapItems SymbKind
k [SymbOrMap]
is [] (Range -> SymbMapItems) -> Range -> SymbMapItems
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
p Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

symbMaps :: AParser st ([SymbOrMap], [Token])
symbMaps :: AParser st ([SymbOrMap], [Token])
symbMaps = do
    SymbOrMap
s <- AParser st SymbOrMap
forall st. AParser st SymbOrMap
symbMap
    do Token
c <- AParser st Token
forall st. AParser st Token
anComma AParser st Token
-> GenParser Char (AnnoState st) Symb -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`followedWith` GenParser Char (AnnoState st) Symb
forall st. AParser st Symb
symb
       (is :: [SymbOrMap]
is, ps :: [Token]
ps) <- AParser st ([SymbOrMap], [Token])
forall st. AParser st ([SymbOrMap], [Token])
symbMaps
       ([SymbOrMap], [Token]) -> AParser st ([SymbOrMap], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return (SymbOrMap
s SymbOrMap -> [SymbOrMap] -> [SymbOrMap]
forall a. a -> [a] -> [a]
: [SymbOrMap]
is, Token
c Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps)
      AParser st ([SymbOrMap], [Token])
-> AParser st ([SymbOrMap], [Token])
-> AParser st ([SymbOrMap], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([SymbOrMap], [Token]) -> AParser st ([SymbOrMap], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([SymbOrMap
s], [])