PredefinedCASLAxioms.hs revision 200047c6bcc532759c37274b5c663388d3dd54a6
967e5f3c25249c779575864692935627004d3f9eChristian MaederDescription : with inlined axioms
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Uni and DFKI Bremen 2005-2007
967e5f3c25249c779575864692935627004d3f9eChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : Christian.Maeder@dfki.de
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional
967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability : portable
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , predefinedSign
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , conceptPred
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder , predefinedAxioms
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , negateFloat
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , emptyStringTerm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport qualified Common.Lib.Rel as Rel
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport qualified Common.Lib.MapSet as MapSet
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederhetsPrefix :: String
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederhetsPrefix = ""
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- | OWL topsort Thing
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederthing = stringToId thingS
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedernothing :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedernothing = stringToId nothingS
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- | OWL Data topSort DATA
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederdataS = stringToId dATAS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinteger :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederinteger = stringToId integerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederfloat = stringToId floatS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederdecimal :: SORT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederdecimal = stringToId decimalS
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdouble :: SORT
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdouble = stringToId doubleS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederposInt :: SORT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederposInt = stringToId positiveIntegerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegIntS :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegIntS = stringToId negativeIntegerS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedernonPosInt :: SORT
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedernonPosInt = stringToId nonPositiveIntegerS
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedernonNegInt :: SORT
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedernonNegInt = stringToId nonNegativeIntegerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederclassPredType :: PRED_TYPE
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederclassPredType = Pred_type [thing] n
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederconceptPred :: PredType
967e5f3c25249c779575864692935627004d3f9eChristian MaederconceptPred = toPredType classPredType
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaederdataPred :: PredType
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederdataPred = PredType [dataS, dataS]
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederboolS = stringToId "boolean"
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederboolT :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederboolT = mkTotOpType [] boolS
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedertrueS = stringToId "True"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederfalseS = stringToId "False"
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermkConst :: Id -> OpType -> TERM ()
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermkConst i o = mkAppl (mkQualOp i $ toOP_TYPE o) []
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedertrueT :: TERM ()
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedertrueT = mkConst trueS boolT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederfalseT :: TERM ()
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederfalseT = mkConst falseS boolT
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedernatT :: OpType
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskinatT = mkTotOpType [] nonNegInt
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder-- | create a term of type nonNegativeInteger
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermkDigit :: Int -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermkDigit i = mkConst (stringToId $ show i) natT
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederunMinus = mkId [mkSimpleId "-", placeTok]
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusTy :: OpType
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusTy = mkTotOpType [integer] integer
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusFloat :: OpType
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiminusFloat = mkTotOpType [float] float
967e5f3c25249c779575864692935627004d3f9eChristian MaedernegateTy :: OpType -> TERM () -> TERM ()
967e5f3c25249c779575864692935627004d3f9eChristian MaedernegateTy o t = mkAppl (mkQualOp unMinus $ toOP_TYPE o) [t]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | negate a term of type integer
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateInt :: TERM () -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateInt = negateTy minusTy
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | negate a term of type float
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateFloat :: TERM () -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateFloat = negateTy minusFloat
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederatAt = mkInfix "@@"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederatAtTy :: OpType
967e5f3c25249c779575864692935627004d3f9eChristian MaederatAtTy = mkTotOpType [nonNegInt, nonNegInt] nonNegInt
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermkBinOp :: Id -> OpType -> TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkBinOp i o t1 t2 = mkAppl (mkQualOp i $ toOP_TYPE o) [t1, t2]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | join two terms of type nonNegativeInteger
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederjoinDigits :: TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederjoinDigits = mkBinOp atAt atAtTy
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederdec = mkInfix ":::"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdecTy :: OpType
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdecTy = mkTotOpType [nonNegInt, nonNegInt] float
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder{- | create the float given by two non-negative integers separated by the
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederdecimal point -}
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkDecimal :: TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkDecimal = mkBinOp dec decTy
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedereId = mkInfix "E"
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederexpTy :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederexpTy = mkTotOpType [float, integer] float
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | construct the E float, where the second argument is of type integer
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermkFloat :: TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkFloat = mkBinOp eId expTy
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | upcast a term to a matching sort
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederupcast :: TERM () -> SORT -> TERM ()
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederupcast t ty = Sorted_term t ty nullRange
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharS = stringToId "Char"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharT :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharT = mkTotOpType [] charS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederstringS = stringToId "string"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maedercons = mkInfix ":@:"
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederemptyString :: Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederemptyString = stringToId "emptyString"
967e5f3c25249c779575864692935627004d3f9eChristian MaederemptyStringTerm :: TERM ()
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederemptyStringTerm = mkAppl (mkQualOp emptyString $ toOP_TYPE emptyStringTy) []
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercharToId :: Char -> Id
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercharToId c = let s = show (ord c) in
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder stringToId $ "'\\" ++ replicate (3 - length s) '0' ++ show (ord c) ++ "'"
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedermkChar :: Char -> TERM ()
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedermkChar c = mkAppl (mkQualOp (charToId c) $ toOP_TYPE charT) []
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsChar :: Char -> TERM () -> TERM ()
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsChar c t = mkAppl (mkQualOp cons $ toOP_TYPE consTy) [mkChar c, t]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederemptyStringTy :: OpType
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederemptyStringTy = mkTotOpType [] stringS
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsTy :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederconsTy = mkTotOpType [charS, stringS] stringS
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- | OWL bottom
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernoThing :: PRED_SYMB
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernoThing = Qual_pred_name nothing classPredType n
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederintTypes :: [PredType]
{ sortRel = Rel.insertKey (stringToId "Char")
$ Rel.insertKey thing
, opMap = MapSet.fromList