{- |

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)