{- |
Module      :  ./ConstraintCASL/Formula.hs
Copyright   :  (c) Florian Mossakowski, Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

parse terms and formulae
-}

module ConstraintCASL.Formula where

import Common.AnnoState
import Common.Id
import Common.Lexer
import Common.Token
import ConstraintCASL.AS_ConstraintCASL
import Text.ParserCombinators.Parsec
import CASL.AS_Basic_CASL

{- ------------------------------------------------------------------------
formula
------------------------------------------------------------------------ -}

cformula :: [String] -> AParser st ConstraintFORMULA
cformula :: [String] -> AParser st ConstraintFORMULA
cformula k :: [String]
k =
    AParser st ConstraintFORMULA -> AParser st ConstraintFORMULA
forall tok st a. GenParser tok st a -> GenParser tok st a
try (
    do ATOMCONJUNCTION
c1 <- [String] -> AParser st ATOMCONJUNCTION
forall st. [String] -> AParser st ATOMCONJUNCTION
conjunction [String]
k
       GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
impliesT
       ATOMCONJUNCTION
c2 <- [String] -> AParser st ATOMCONJUNCTION
forall st. [String] -> AParser st ATOMCONJUNCTION
conjunction [String]
k
       ConstraintFORMULA -> AParser st ConstraintFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOMCONJUNCTION -> ATOMCONJUNCTION -> ConstraintFORMULA
Implication_ConstraintFormula ATOMCONJUNCTION
c1 ATOMCONJUNCTION
c2))
  AParser st ConstraintFORMULA
-> AParser st ConstraintFORMULA -> AParser st ConstraintFORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    AParser st ConstraintFORMULA -> AParser st ConstraintFORMULA
forall tok st a. GenParser tok st a -> GenParser tok st a
try (
    do ATOMCONJUNCTION
c1 <- [String] -> AParser st ATOMCONJUNCTION
forall st. [String] -> AParser st ATOMCONJUNCTION
conjunction [String]
k
       GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
equivalentT
       ATOMCONJUNCTION
c2 <- [String] -> AParser st ATOMCONJUNCTION
forall st. [String] -> AParser st ATOMCONJUNCTION
conjunction [String]
k
       ConstraintFORMULA -> AParser st ConstraintFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOMCONJUNCTION -> ATOMCONJUNCTION -> ConstraintFORMULA
Equivalence_ConstraintFormula ATOMCONJUNCTION
c1 ATOMCONJUNCTION
c2))
  AParser st ConstraintFORMULA
-> AParser st ConstraintFORMULA -> AParser st ConstraintFORMULA
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
impliesT
       ATOMCONJUNCTION
c <- [String] -> AParser st ATOMCONJUNCTION
forall st. [String] -> AParser st ATOMCONJUNCTION
conjunction [String]
k
       ConstraintFORMULA -> AParser st ConstraintFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ATOMCONJUNCTION -> ConstraintFORMULA
Axiom_ConstraintFormula ATOMCONJUNCTION
c)

conjunction :: [String] -> AParser st ATOMCONJUNCTION
conjunction :: [String] -> AParser st ATOMCONJUNCTION
conjunction k :: [String]
k =
    do (atoms :: [ATOM]
atoms, _) <- [String] -> AParser st ATOM
forall st. [String] -> AParser st ATOM
atom [String]
k AParser st ATOM
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([ATOM], [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
       ATOMCONJUNCTION -> AParser st ATOMCONJUNCTION
forall (m :: * -> *) a. Monad m => a -> m a
return ([ATOM] -> ATOMCONJUNCTION
Atom_Conjunction [ATOM]
atoms)

atom :: [String] -> AParser st ATOM
atom :: [String] -> AParser st ATOM
atom k :: [String]
k =
    AParser st ATOM -> AParser st ATOM
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do RELATION
r <- [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
relation [String]
k
            CharParser (AnnoState st) Token
forall st. GenParser Char st Token
oParenT
            (terms :: [ConstraintTERM]
terms, _) <- [String] -> AParser st ConstraintTERM
forall st. [String] -> AParser st ConstraintTERM
constraintterm [String]
k AParser st ConstraintTERM
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([ConstraintTERM], [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
            CharParser (AnnoState st) Token
forall st. GenParser Char st Token
cParenT CharParser (AnnoState st) Token
-> AParser st RELATION -> CharParser (AnnoState st) Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`notFollowedWith` [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
relation [String]
k
            ATOM -> AParser st ATOM
forall (m :: * -> *) a. Monad m => a -> m a
return (RELATION -> [ConstraintTERM] -> ATOM
Prefix_Atom RELATION
r [ConstraintTERM]
terms))
  AParser st ATOM -> AParser st ATOM -> AParser st ATOM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do ConstraintTERM
t1 <- [String] -> AParser st ConstraintTERM
forall st. [String] -> AParser st ConstraintTERM
constraintterm [String]
k
       RELATION
r <- [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
relation [String]
k
       ConstraintTERM
t2 <- [String] -> AParser st ConstraintTERM
forall st. [String] -> AParser st ConstraintTERM
constraintterm [String]
k
       ATOM -> AParser st ATOM
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintTERM -> RELATION -> ConstraintTERM -> ATOM
Infix_Atom ConstraintTERM
t1 RELATION
r ConstraintTERM
t2)

simplerelation :: [String] -> AParser st RELATION
simplerelation :: [String] -> AParser st RELATION
simplerelation k :: [String]
k =
    do GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
emptyRelationT
       RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION
Empty_Relation
   AParser st RELATION -> AParser st RELATION -> AParser st RELATION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
equalityRelationT
       RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION
Equal_Relation
   AParser st RELATION -> AParser st RELATION -> AParser st RELATION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
oParenT
       RELATION
r <- [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
relation [String]
k
       GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
cParenT
       RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return RELATION
r
   AParser st RELATION -> AParser st RELATION -> AParser st RELATION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Id
ide <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
k
       RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> RELATION
Id_Relation Id
ide)
   AParser st RELATION -> AParser st RELATION -> AParser st RELATION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do GenParser Char (AnnoState st) Token
forall st. GenParser Char st Token
inverseT
       RELATION
r <- [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
relation [String]
k
       RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return (RELATION -> RELATION
Inverse_Relation RELATION
r)

relation :: [String] -> AParser st RELATION
relation :: [String] -> AParser st RELATION
relation k :: [String]
k =
    AParser st RELATION -> AParser st RELATION
forall tok st a. GenParser tok st a -> GenParser tok st a
try ( do (rels :: [RELATION]
rels, _) <- [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
simplerelation [String]
k AParser st RELATION
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) ([RELATION], [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
             RELATION -> AParser st RELATION
forall (m :: * -> *) a. Monad m => a -> m a
return ([RELATION] -> RELATION
Relation_Disjunction [RELATION]
rels))
   AParser st RELATION -> AParser st RELATION -> AParser st RELATION
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st RELATION
forall st. [String] -> AParser st RELATION
simplerelation [String]
k

constraintterm :: [String] -> AParser st ConstraintTERM
constraintterm :: [String] -> AParser st ConstraintTERM
constraintterm k :: [String]
k =
    AParser st ConstraintTERM -> AParser st ConstraintTERM
forall tok st a. GenParser tok st a -> GenParser tok st a
try (do Id
ide <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
k
            ConstraintTERM -> AParser st ConstraintTERM
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> ConstraintTERM
Atomar_Term Id
ide))
   AParser st ConstraintTERM
-> AParser st ConstraintTERM -> AParser st ConstraintTERM
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
    do Id
ide <- [String] -> GenParser Char (AnnoState st) Id
forall st. [String] -> GenParser Char st Id
parseId [String]
k
       CharParser (AnnoState st) Token
forall st. GenParser Char st Token
oParenT
       (terms :: [ConstraintTERM]
terms, _) <- [String] -> AParser st ConstraintTERM
forall st. [String] -> AParser st ConstraintTERM
constraintterm [String]
k AParser st ConstraintTERM
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([ConstraintTERM], [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
       CharParser (AnnoState st) Token
forall st. GenParser Char st Token
cParenT
       ConstraintTERM -> AParser st ConstraintTERM
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> [ConstraintTERM] -> ConstraintTERM
Composite_Term Id
ide [ConstraintTERM]
terms)

formula :: [String] -> AParser st ConstraintCASLFORMULA
formula :: [String] -> AParser st ConstraintCASLFORMULA
formula k :: [String]
k =  do ConstraintFORMULA
x <- [String] -> AParser st ConstraintFORMULA
forall st. [String] -> AParser st ConstraintFORMULA
cformula [String]
k
                ConstraintCASLFORMULA -> AParser st ConstraintCASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintFORMULA -> ConstraintCASLFORMULA
forall f. f -> FORMULA f
ExtFORMULA ConstraintFORMULA
x)

emptyRelation :: String
emptyRelation :: String
emptyRelation = "{}"

emptyRelationT :: GenParser Char st Token
emptyRelationT :: GenParser Char st Token
emptyRelationT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
emptyRelation

equalityRelation :: String
equalityRelation :: String
equalityRelation = "="

equalityRelationT :: GenParser Char st Token
equalityRelationT :: GenParser Char st Token
equalityRelationT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
equalityRelation

inverse :: String
inverse :: String
inverse = "~"

inverseT :: GenParser Char st Token
inverseT :: GenParser Char st Token
inverseT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
inverse

implies :: String
implies :: String
implies = "|-"

impliesT :: GenParser Char st Token
impliesT :: GenParser Char st Token
impliesT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
implies

equivalent :: String
equivalent :: String
equivalent = "-||-"

equivalentT :: GenParser Char st Token
equivalentT :: GenParser Char st Token
equivalentT = CharParser st String -> GenParser Char st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser st String -> GenParser Char st Token)
-> CharParser st String -> GenParser Char st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser st String
forall st. String -> CharParser st String
toKey String
equivalent

constraintKeywords :: [String]
constraintKeywords :: [String]
constraintKeywords = [String
equivalent, String
implies]

instance TermParser ConstraintFORMULA where
  termParser :: Bool -> AParser st ConstraintFORMULA
termParser = AParser st ConstraintFORMULA
-> Bool -> AParser st ConstraintFORMULA
forall st a. AParser st a -> Bool -> AParser st a
aToTermParser (AParser st ConstraintFORMULA
 -> Bool -> AParser st ConstraintFORMULA)
-> AParser st ConstraintFORMULA
-> Bool
-> AParser st ConstraintFORMULA
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st ConstraintFORMULA
forall st. [String] -> AParser st ConstraintFORMULA
cformula []