content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./ConstraintCASL/AS_ConstraintCASL.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
  
  Abstract syntax for ConstraintCASL
    Only the formula syntax is specified
  -}
  
  module ConstraintCASL.AS_ConstraintCASL where
  
  import Data.Data
  
  import Common.Id
  
  import CASL.AS_Basic_CASL
  
  type ConstraintCASLBasicSpec = BASIC_SPEC () () ConstraintFORMULA
  
  type ConstraintCASLFORMULA = FORMULA ConstraintFORMULA
  
  data ConstraintFORMULA = Implication_ConstraintFormula
                           ATOMCONJUNCTION ATOMCONJUNCTION
                         | Equivalence_ConstraintFormula
                           ATOMCONJUNCTION ATOMCONJUNCTION
                         | Axiom_ConstraintFormula ATOMCONJUNCTION
                           deriving (Show, Eq, Ord, Typeable, Data)
  
  data RELATION = Empty_Relation | Equal_Relation | Id_Relation Id
                | Relation_Disjunction [RELATION] | Inverse_Relation RELATION
                  deriving (Show, Eq, Ord, Typeable, Data)
  
  
  data ATOMCONJUNCTION = Atom_Conjunction [ATOM]
                     deriving (Show, Eq, Ord, Typeable, Data)
  
  
  data ATOM = Prefix_Atom RELATION [ConstraintTERM]
            | Infix_Atom ConstraintTERM RELATION ConstraintTERM
              deriving (Show, Eq, Ord, Typeable, Data)
  
  data ConstraintTERM = Atomar_Term Id | Composite_Term Id [ConstraintTERM]
                        deriving (Show, Eq, Ord, Typeable, Data)
  
  instance GetRange ConstraintFORMULA -- default is nullRange
  