{- |
Module      :  ./CoCASL/Parse_AS.hs
Description :  Parser for CoCASL
Copyright   :  (c) Christian Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  hausmann@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Parser for CoCASL
-}

module CoCASL.Parse_AS where

import Common.AnnoState
import Common.AS_Annotation
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Token
import CoCASL.AS_CoCASL
import Text.ParserCombinators.Parsec
import CASL.Formula
import CASL.Parse_AS_Basic (sigItems)
import CASL.AS_Basic_CASL

cocasl_reserved_words :: [String]
cocasl_reserved_words :: [String]
cocasl_reserved_words = [String
diamondS]

parseSen :: AParser st (FORMULA C_FORMULA)
parseSen :: AParser st (FORMULA C_FORMULA)
parseSen = [String] -> AParser st (FORMULA C_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
cocasl_reserved_words

cocaslFormula :: AParser st C_FORMULA
cocaslFormula :: AParser st C_FORMULA
cocaslFormula = do
    Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
    MODALITY
m <- [String] -> AParser st MODALITY
forall st. [String] -> AParser st MODALITY
modality []
    Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
    FORMULA C_FORMULA
f <- [String] -> AParser st (FORMULA C_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
cocasl_reserved_words
    C_FORMULA -> AParser st C_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
True MODALITY
m FORMULA C_FORMULA
f (Range -> C_FORMULA) -> Range -> C_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)
  AParser st C_FORMULA
-> AParser st C_FORMULA -> AParser st C_FORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
o <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
lessS
    MODALITY
m <- [String] -> AParser st MODALITY
forall st. [String] -> AParser st MODALITY
modality [String
greaterS] -- do not consume matching ">"!
    Token
c <- String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
greaterS
    FORMULA C_FORMULA
f <- [String] -> AParser st (FORMULA C_FORMULA)
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula [String]
cocasl_reserved_words
    C_FORMULA -> AParser st C_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MODALITY -> FORMULA C_FORMULA -> Range -> C_FORMULA
BoxOrDiamond Bool
False MODALITY
m FORMULA C_FORMULA
f (Range -> C_FORMULA) -> Range -> C_FORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
o [] Token
c)

modality :: [String] -> AParser st MODALITY
modality :: [String] -> AParser st MODALITY
modality ks :: [String]
ks = do
    TERM C_FORMULA
t <- [String] -> AParser st (TERM C_FORMULA)
forall f st. TermParser f => [String] -> AParser st (TERM f)
term (String
prodS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ks [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
cocasl_reserved_words)
            -- put the term in parens if you need to use "*"
    ()
-> ParsecT String (AnnoState st) Identity ()
-> ParsecT String (AnnoState st) Identity ()
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option () (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
prodS AParser st Token
-> ParsecT String (AnnoState st) Identity ()
-> ParsecT String (AnnoState st) Identity ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> ParsecT String (AnnoState st) Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
       -- presence of "*" is not stored yet!
    MODALITY -> AParser st MODALITY
forall (m :: * -> *) a. Monad m => a -> m a
return (MODALITY -> AParser st MODALITY)
-> MODALITY -> AParser st MODALITY
forall a b. (a -> b) -> a -> b
$ case TERM C_FORMULA
t of
      Mixfix_token tok :: Token
tok -> Token -> MODALITY
Simple_mod Token
tok
      _ -> TERM C_FORMULA -> MODALITY
Term_mod TERM C_FORMULA
t

instance TermParser C_FORMULA where
  termParser :: Bool -> AParser st C_FORMULA
termParser = AParser st C_FORMULA -> Bool -> AParser st C_FORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser AParser st C_FORMULA
forall st. AParser st C_FORMULA
cocaslFormula

cBasic :: AParser st C_BASIC_ITEM
cBasic :: AParser st C_BASIC_ITEM
cBasic = do
    Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
cofreeS
    C_SIG_ITEM
ti <- AParser st C_SIG_ITEM
forall st. AParser st C_SIG_ITEM
coSigItems
    C_BASIC_ITEM -> AParser st C_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (C_SIG_ITEM -> Range -> C_BASIC_ITEM
codatatypeToCofreetype C_SIG_ITEM
ti (Token -> Range
tokPos Token
f))
  AParser st C_BASIC_ITEM
-> AParser st C_BASIC_ITEM -> AParser st C_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
g <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
cogeneratedS
    do SIG_ITEMS C_SIG_ITEM C_FORMULA
t <- [String] -> AParser st (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
sigItems [String]
cocasl_reserved_words
       C_BASIC_ITEM -> AParser st C_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> Range -> C_BASIC_ITEM
CoSort_gen [SIG_ITEMS C_SIG_ITEM C_FORMULA
-> Range
-> [Annotation]
-> [Annotation]
-> Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted SIG_ITEMS C_SIG_ITEM C_FORMULA
t Range
nullRange [] []] (Range -> C_BASIC_ITEM) -> Range -> C_BASIC_ITEM
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
g)
      AParser st C_BASIC_ITEM
-> AParser st C_BASIC_ITEM -> AParser st C_BASIC_ITEM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
        Token
o <- AParser st Token
forall st. CharParser st Token
oBraceT
        [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
is <- AParser st (SIG_ITEMS C_SIG_ITEM C_FORMULA)
-> AParser st [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
forall st a. AParser st a -> AParser st [Annoted a]
annosParser ([String] -> AParser st (SIG_ITEMS C_SIG_ITEM C_FORMULA)
forall s f st.
(AParsable s, TermParser f) =>
[String] -> AParser st (SIG_ITEMS s f)
sigItems [String]
cocasl_reserved_words)
        Token
c <- AParser st Token
forall st. CharParser st Token
cBraceT
        C_BASIC_ITEM -> AParser st C_BASIC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] -> Range -> C_BASIC_ITEM
CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)]
is (Token -> [Token] -> Token -> Range
toRange Token
g [Token
o] Token
c))

coSigItems :: AParser st C_SIG_ITEM
coSigItems :: AParser st C_SIG_ITEM
coSigItems =
  [String]
-> String
-> ([String] -> AParser st CODATATYPE_DECL)
-> ([Annoted CODATATYPE_DECL] -> Range -> C_SIG_ITEM)
-> AParser st C_SIG_ITEM
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
cocasl_reserved_words String
cotypeS [String] -> AParser st CODATATYPE_DECL
forall st. [String] -> AParser st CODATATYPE_DECL
codatatype [Annoted CODATATYPE_DECL] -> Range -> C_SIG_ITEM
CoDatatype_items

codatatype :: [String] -> AParser st CODATATYPE_DECL
codatatype :: [String] -> AParser st CODATATYPE_DECL
codatatype ks :: [String]
ks = do
    Id
s <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks
    AParser st ()
forall st. AParser st ()
addAnnos
    Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
defnS
    AParser st ()
forall st. AParser st ()
addAnnos
    [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
getAnnos
    (Annoted v :: COALTERNATIVE
v _ _ b :: [Annotation]
b : as :: [Annoted COALTERNATIVE]
as, ps :: [Token]
ps) <- [String] -> AParser st (Annoted COALTERNATIVE)
forall st. [String] -> AParser st (Annoted COALTERNATIVE)
acoAlternative [String]
ks AParser st (Annoted COALTERNATIVE)
-> AParser st Token
-> GenParser Char (AnnoState st) ([Annoted COALTERNATIVE], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` AParser st Token
forall st. AParser st Token
barT
    CODATATYPE_DECL -> AParser st CODATATYPE_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return (CODATATYPE_DECL -> AParser st CODATATYPE_DECL)
-> CODATATYPE_DECL -> AParser st CODATATYPE_DECL
forall a b. (a -> b) -> a -> b
$ Id -> [Annoted COALTERNATIVE] -> Range -> CODATATYPE_DECL
CoDatatype_decl Id
s (COALTERNATIVE
-> Range -> [Annotation] -> [Annotation] -> Annoted COALTERNATIVE
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted COALTERNATIVE
v Range
nullRange [Annotation]
a [Annotation]
b Annoted COALTERNATIVE
-> [Annoted COALTERNATIVE] -> [Annoted COALTERNATIVE]
forall a. a -> [a] -> [a]
: [Annoted COALTERNATIVE]
as)
      (Range -> CODATATYPE_DECL) -> Range -> CODATATYPE_DECL
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
e Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ps

acoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
acoAlternative :: [String] -> AParser st (Annoted COALTERNATIVE)
acoAlternative ks :: [String]
ks = do
    COALTERNATIVE
a <- [String] -> AParser st COALTERNATIVE
forall st. [String] -> AParser st COALTERNATIVE
coalternative [String]
ks
    [Annotation]
an <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
    Annoted COALTERNATIVE -> AParser st (Annoted COALTERNATIVE)
forall (m :: * -> *) a. Monad m => a -> m a
return (COALTERNATIVE
-> Range -> [Annotation] -> [Annotation] -> Annoted COALTERNATIVE
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted COALTERNATIVE
a Range
nullRange [] [Annotation]
an)

coalternative :: [String] -> AParser st COALTERNATIVE
coalternative :: [String] -> AParser st COALTERNATIVE
coalternative ks :: [String]
ks = do
    Token
s <- String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
sortS
    (ts :: [Id]
ts, cs :: [Token]
cs) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
sortId [String]
ks GenParser Char (AnnoState st) Id
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. AParser st Token
anComma
    COALTERNATIVE -> AParser st COALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> Range -> COALTERNATIVE
CoSubsorts [Id]
ts (Range -> COALTERNATIVE) -> Range -> COALTERNATIVE
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ Token
s Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
cs)
  AParser st COALTERNATIVE
-> AParser st COALTERNATIVE -> AParser st COALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Id
i <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
consId [String]
ks
    [String] -> Maybe Id -> AParser st COALTERNATIVE
forall st. [String] -> Maybe Id -> AParser st COALTERNATIVE
cocomp [String]
ks (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i)
  AParser st COALTERNATIVE
-> AParser st COALTERNATIVE -> AParser st COALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> Maybe Id -> AParser st COALTERNATIVE
forall st. [String] -> Maybe Id -> AParser st COALTERNATIVE
cocomp [String]
ks Maybe Id
forall a. Maybe a
Nothing

cocomp :: [String] -> Maybe OP_NAME -> AParser st COALTERNATIVE
cocomp :: [String] -> Maybe Id -> AParser st COALTERNATIVE
cocomp ks :: [String]
ks i :: Maybe Id
i = do
    Token
o <- CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT
    (cs :: [COCOMPONENTS]
cs, ps :: [Token]
ps) <- [String] -> AParser st COCOMPONENTS
forall st. [String] -> AParser st COCOMPONENTS
cocomponent [String]
ks AParser st COCOMPONENTS
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([COCOMPONENTS], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. AParser st Token
anSemi
    Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT
    let qs :: Range
qs = Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c
    do Token
q <- CharParser (AnnoState st) Token
forall st. CharParser st Token
quMarkT
       COALTERNATIVE -> AParser st COALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Maybe Id -> [COCOMPONENTS] -> Range -> COALTERNATIVE
Co_construct OpKind
Partial Maybe Id
i [COCOMPONENTS]
cs (Range
qs Range -> Range -> Range
`appRange` Token -> Range
tokPos Token
q))
      AParser st COALTERNATIVE
-> AParser st COALTERNATIVE -> AParser st COALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> COALTERNATIVE -> AParser st COALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Maybe Id -> [COCOMPONENTS] -> Range -> COALTERNATIVE
Co_construct OpKind
Total Maybe Id
i [COCOMPONENTS]
cs Range
qs)
  AParser st COALTERNATIVE
-> AParser st COALTERNATIVE -> AParser st COALTERNATIVE
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> COALTERNATIVE -> AParser st COALTERNATIVE
forall (m :: * -> *) a. Monad m => a -> m a
return (OpKind -> Maybe Id -> [COCOMPONENTS] -> Range -> COALTERNATIVE
Co_construct OpKind
Total Maybe Id
i [] Range
nullRange)

cocomponent :: [String] -> AParser st COCOMPONENTS
cocomponent :: [String] -> AParser st COCOMPONENTS
cocomponent ks :: [String]
ks = do
    (is :: [Id]
is, cs :: [Token]
cs) <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
ks GenParser Char (AnnoState st) Id
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([Id], [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
    Token
c <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
colonST
    OP_TYPE
t <- [String] -> AParser st OP_TYPE
forall st. [String] -> AParser st OP_TYPE
opType [String]
ks
    COCOMPONENTS -> AParser st COCOMPONENTS
forall (m :: * -> *) a. Monad m => a -> m a
return (COCOMPONENTS -> AParser st COCOMPONENTS)
-> COCOMPONENTS -> AParser st COCOMPONENTS
forall a b. (a -> b) -> a -> b
$ [Id] -> OP_TYPE -> Range -> COCOMPONENTS
CoSelect [Id]
is OP_TYPE
t (Range -> COCOMPONENTS) -> Range -> COCOMPONENTS
forall a b. (a -> b) -> a -> b
$ [Token] -> Range
catRange ([Token] -> Range) -> [Token] -> Range
forall a b. (a -> b) -> a -> b
$ [Token]
cs [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
c]

instance AParsable C_SIG_ITEM where
  aparser :: AParser st C_SIG_ITEM
aparser = AParser st C_SIG_ITEM
forall st. AParser st C_SIG_ITEM
coSigItems

instance AParsable C_BASIC_ITEM where
  aparser :: AParser st C_BASIC_ITEM
aparser = AParser st C_BASIC_ITEM
forall st. AParser st C_BASIC_ITEM
cBasic

codatatypeToCofreetype :: C_SIG_ITEM -> Range -> C_BASIC_ITEM
codatatypeToCofreetype :: C_SIG_ITEM -> Range -> C_BASIC_ITEM
codatatypeToCofreetype d :: C_SIG_ITEM
d pos :: Range
pos = case C_SIG_ITEM
d of
    CoDatatype_items ts :: [Annoted CODATATYPE_DECL]
ts ps :: Range
ps -> [Annoted CODATATYPE_DECL] -> Range -> C_BASIC_ITEM
CoFree_datatype [Annoted CODATATYPE_DECL]
ts (Range
pos Range -> Range -> Range
`appRange` Range
ps)