content: {- |
  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 k =
      try (
      do c1 <- conjunction k
         impliesT
         c2 <- conjunction k
         return (Implication_ConstraintFormula c1 c2))
    <|>
      try (
      do c1 <- conjunction k
         equivalentT
         c2 <- conjunction k
         return (Equivalence_ConstraintFormula c1 c2))
    <|>
      do impliesT
         c <- conjunction k
         return (Axiom_ConstraintFormula c)
  
  conjunction :: [String] -> AParser st ATOMCONJUNCTION
  conjunction k =
      do (atoms, _) <- atom k `separatedBy` anComma
         return (Atom_Conjunction atoms)
  
  atom :: [String] -> AParser st ATOM
  atom k =
      try (do r <- relation k
              oParenT
              (terms, _) <- constraintterm k `separatedBy` anComma
              cParenT `notFollowedWith` relation k
              return (Prefix_Atom r terms))
    <|>
      do t1 <- constraintterm k
         r <- relation k
         t2 <- constraintterm k
         return (Infix_Atom t1 r t2)
  
  simplerelation :: [String] -> AParser st RELATION
  simplerelation k =
      do emptyRelationT
         return Empty_Relation
     <|>
      do equalityRelationT
         return Equal_Relation
     <|>
      do oParenT
         r <- relation k
         cParenT
         return r
     <|>
      do ide <- parseId k
         return (Id_Relation ide)
     <|>
      do inverseT
         r <- relation k
         return (Inverse_Relation r)
  
  relation :: [String] -> AParser st RELATION
  relation k =
      try ( do (rels, _) <- simplerelation k `separatedBy` anComma
               return (Relation_Disjunction rels))
     <|> simplerelation k
  
  constraintterm :: [String] -> AParser st ConstraintTERM
  constraintterm k =
      try (do ide <- parseId k
              return (Atomar_Term ide))
     <|>
      do ide <- parseId k
         oParenT
         (terms, _) <- constraintterm k `separatedBy` anComma
         cParenT
         return (Composite_Term ide terms)
  
  formula :: [String] -> AParser st ConstraintCASLFORMULA
  formula k =  do x <- cformula k
                  return (ExtFORMULA x)
  
  emptyRelation :: String
  emptyRelation = "{}"
  
  emptyRelationT :: GenParser Char st Token
  emptyRelationT = pToken $ toKey emptyRelation
  
  equalityRelation :: String
  equalityRelation = "="
  
  equalityRelationT :: GenParser Char st Token
  equalityRelationT = pToken $ toKey equalityRelation
  
  inverse :: String
  inverse = "~"
  
  inverseT :: GenParser Char st Token
  inverseT = pToken $ toKey inverse
  
  implies :: String
  implies = "|-"
  
  impliesT :: GenParser Char st Token
  impliesT = pToken $ toKey implies
  
  equivalent :: String
  equivalent = "-||-"
  
  equivalentT :: GenParser Char st Token
  equivalentT = pToken $ toKey equivalent
  
  constraintKeywords :: [String]
  constraintKeywords = [equivalent, implies]
  
  instance TermParser ConstraintFORMULA where
    termParser = aToTermParser $ cformula []
  