content: {- |
  Module      :  ./Omega/DataTypes.hs
  Description :  The Omega Data Types
  Copyright   :  (c) Ewaryst Schulz, DFKI 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Ewaryst.Schulz@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Datatypes for an intermediate Omega Representation.
  -}
  module Omega.DataTypes where
  
  justWhen :: Bool -> a -> Maybe a
  justWhen b x = if b then Just x else Nothing
  
  -- | Top level element with libname and a list of theories
  data Library = Library String [Theory] deriving (Show, Eq, Ord)
  
  {- | Contains a theoryname a list of imports, signature elements and
  sentences (axioms or theorems) -}
  data Theory = Theory String [String] [TCElement]
                   deriving (Show, Eq, Ord)
  
  -- | Theory constitutive elements
  data TCElement =
      -- | An axiom or theorem element
      TCAxiomOrTheorem Bool String Term
      -- | Symbol to represent sorts, constants, predicate symbols, etc.
    | TCSymbol String
      -- | A comment, only for development purposes
    | TCComment String
      deriving (Show, Eq, Ord)
  
  
  -- | Term structure
  data Term =
      -- | Symbol
      Symbol String
      -- | Simple variable
    | Var String
      -- | Application of a function to a list of arguments
    | App Term [Term]
      -- | Bindersymbol, bound vars, body
    | Bind String [Term] Term
    deriving (Show, Eq, Ord)
  