a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterDescription : The Omega Data Types
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterCopyright : (c) Ewaryst Schulz, DFKI 2008
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterLicense : GPLv2 or higher, see LICENSE.txt
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterMaintainer : Ewaryst.Schulz@dfki.de
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterStability : provisional
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterPortability : portable
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterDatatypes for an intermediate Omega Representation.
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterjustWhen :: Bool -> a -> Maybe a
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterjustWhen b x = if b then Just x else Nothing
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | Top level element with libname and a list of theories
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Library = Library String [Theory] deriving (Show, Eq, Ord)
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | Contains a theoryname a list of imports, signature elements and
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fostersentences (axioms or theorems) -}
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Theory = Theory String [String] [TCElement]
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | Theory constitutive elements
449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbingsdata TCElement =
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | An axiom or theorem element
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster TCAxiomOrTheorem Bool String Term
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | Symbol to represent sorts, constants, predicate symbols, etc.
449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings | TCSymbol String
449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings -- | A comment, only for development purposes
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | TCComment String
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | Term structure
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Symbol String
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | Simple variable
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Var String
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | Application of a function to a list of arguments
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | App Term [Term]
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | Bindersymbol, bound vars, body
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Bind String [Term] Term
a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)