PredefinedCASLAxioms.hs revision 200047c6bcc532759c37274b5c663388d3dd54a6
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : PredefinedSign.hs
967e5f3c25249c779575864692935627004d3f9eChristian MaederDescription : with inlined axioms
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Uni and DFKI Bremen 2005-2007
967e5f3c25249c779575864692935627004d3f9eChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : Christian.Maeder@dfki.de
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional
967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability : portable
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule CASL_DL.PredefinedCASLAxioms
967e5f3c25249c779575864692935627004d3f9eChristian Maeder ( predefSign
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , predefinedSign
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , thing
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder , nothing
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , conceptPred
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder , dataPred
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , dataS
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder , predefinedAxioms
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , mkNName
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , mkDigit
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder , joinDigits
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , negateInt
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski , integer
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski , float
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , negateFloat
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder , posInt
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , nonPosInt
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , decimal
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , double
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , upcast
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , mkDecimal
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , mkFloat
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , consChar
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , emptyStringTerm
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , trueT
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , falseT
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , nonNegInt
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , negIntS
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , stringS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ) where
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport CASL.AS_Basic_CASL
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport CASL.Sign
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport OWL2.Keywords
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport Common.AS_Annotation
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport Common.Id
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport Common.GlobalAnnotations
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport qualified Common.Lib.Rel as Rel
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport qualified Common.Lib.MapSet as MapSet
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederimport Data.Char
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederhetsPrefix :: String
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederhetsPrefix = ""
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder-- | OWL topsort Thing
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederthing :: SORT
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederthing = stringToId thingS
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedern :: Range
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedern = nullRange
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedernothing :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedernothing = stringToId nothingS
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder-- | OWL Data topSort DATA
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederdataS :: SORT
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederdataS = stringToId dATAS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinteger :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederinteger = stringToId integerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederfloat :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederfloat = stringToId floatS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederdecimal :: SORT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederdecimal = stringToId decimalS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdouble :: SORT
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdouble = stringToId doubleS
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederposInt :: SORT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederposInt = stringToId positiveIntegerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegIntS :: SORT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegIntS = stringToId negativeIntegerS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedernonPosInt :: SORT
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedernonPosInt = stringToId nonPositiveIntegerS
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedernonNegInt :: SORT
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedernonNegInt = stringToId nonNegativeIntegerS
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederclassPredType :: PRED_TYPE
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederclassPredType = Pred_type [thing] n
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederconceptPred :: PredType
967e5f3c25249c779575864692935627004d3f9eChristian MaederconceptPred = toPredType classPredType
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaederdataPred :: PredType
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederdataPred = PredType [dataS, dataS]
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederboolS :: SORT
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederboolS = stringToId "boolean"
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederboolT :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederboolT = mkTotOpType [] boolS
20e16bdd7481741d0b6b14f952aea42ee7a65efbChristian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedertrueS :: Id
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedertrueS = stringToId "True"
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederfalseS :: Id
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederfalseS = stringToId "False"
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermkConst :: Id -> OpType -> TERM ()
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermkConst i o = mkAppl (mkQualOp i $ toOP_TYPE o) []
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedertrueT :: TERM ()
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedertrueT = mkConst trueS boolT
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederfalseT :: TERM ()
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederfalseT = mkConst falseS boolT
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedernatT :: OpType
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskinatT = mkTotOpType [] nonNegInt
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder-- | create a term of type nonNegativeInteger
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermkDigit :: Int -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermkDigit i = mkConst (stringToId $ show i) natT
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederunMinus :: Id
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederunMinus = mkId [mkSimpleId "-", placeTok]
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusTy :: OpType
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusTy = mkTotOpType [integer] integer
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder
842eedc62639561781b6c33533d1949693ef6cc5Christian MaederminusFloat :: OpType
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiminusFloat = mkTotOpType [float] float
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaedernegateTy :: OpType -> TERM () -> TERM ()
967e5f3c25249c779575864692935627004d3f9eChristian MaedernegateTy o t = mkAppl (mkQualOp unMinus $ toOP_TYPE o) [t]
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | negate a term of type integer
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateInt :: TERM () -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateInt = negateTy minusTy
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder-- | negate a term of type float
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateFloat :: TERM () -> TERM ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernegateFloat = negateTy minusFloat
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederatAt :: Id
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederatAt = mkInfix "@@"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederatAtTy :: OpType
967e5f3c25249c779575864692935627004d3f9eChristian MaederatAtTy = mkTotOpType [nonNegInt, nonNegInt] nonNegInt
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermkBinOp :: Id -> OpType -> TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkBinOp i o t1 t2 = mkAppl (mkQualOp i $ toOP_TYPE o) [t1, t2]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | join two terms of type nonNegativeInteger
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederjoinDigits :: TERM () -> TERM () -> TERM ()
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederjoinDigits = mkBinOp atAt atAtTy
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederdec :: Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederdec = mkInfix ":::"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdecTy :: OpType
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederdecTy = mkTotOpType [nonNegInt, nonNegInt] float
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
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 Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedereId :: Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedereId = mkInfix "E"
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederexpTy :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederexpTy = mkTotOpType [float, integer] float
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
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
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | upcast a term to a matching sort
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederupcast :: TERM () -> SORT -> TERM ()
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederupcast t ty = Sorted_term t ty nullRange
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedercharS :: Id
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharS = stringToId "Char"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharT :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercharT = mkTotOpType [] charS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederstringS :: Id
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederstringS = stringToId "string"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedercons :: Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maedercons = mkInfix ":@:"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederemptyString :: Id
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederemptyString = stringToId "emptyString"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederemptyStringTerm :: TERM ()
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederemptyStringTerm = mkAppl (mkQualOp emptyString $ toOP_TYPE emptyStringTy) []
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercharToId :: Char -> Id
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedercharToId c = let s = show (ord c) in
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder stringToId $ "'\\" ++ replicate (3 - length s) '0' ++ show (ord c) ++ "'"
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedermkChar :: Char -> TERM ()
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedermkChar c = mkAppl (mkQualOp (charToId c) $ toOP_TYPE charT) []
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsChar :: Char -> TERM () -> TERM ()
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsChar c t = mkAppl (mkQualOp cons $ toOP_TYPE consTy) [mkChar c, t]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederemptyStringTy :: OpType
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederemptyStringTy = mkTotOpType [] stringS
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederconsTy :: OpType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederconsTy = mkTotOpType [charS, stringS] stringS
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- | OWL bottom
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernoThing :: PRED_SYMB
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernoThing = Qual_pred_name nothing classPredType n
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaederintTypes :: [PredType]
intTypes = map (\ t -> PredType [t]) [integer, nonNegInt]
predefinedSign :: e -> Sign f e
predefinedSign e = (emptySign e)
{ sortRel = Rel.insertKey (stringToId "Char")
$ Rel.insertKey thing
$ Rel.transClosure $ Rel.fromList
[(boolS, dataS),
(integer, float),
(float, dataS),
(negIntS, nonPosInt),
(nonNegInt, integer),
(nonPosInt, integer),
(posInt, nonNegInt),
(stringS, dataS) ]
, predMap =
MapSet.fromList
$ (nothing, [conceptPred])
: map ((\ o -> (mkInfix o, [dataPred])) .
showFacet) facetList
++ map ( \ o -> (stringToId o, intTypes))
["even", "odd"]
, opMap = MapSet.fromList
$ map (\ i -> (stringToId $ show i, [natT]))
[0 .. 9 :: Int]
++ map (\ c -> (charToId c, [charT]))
[chr 0 .. chr 127]
++
[ (trueS, [boolT])
, (falseS, [boolT])
, (atAt, [atAtTy])
, (unMinus, [minusTy, minusFloat])
, (dec, [decTy])
, (eId, [expTy])
, (cons, [consTy])
, (emptyString, [emptyStringTy])
]
, globAnnos = emptyGlobalAnnos
{ literal_annos = emptyLiteralAnnos
{ number_lit = Just atAt
, float_lit = Just (dec, eId)
, string_lit = Just (emptyString, cons) }}
}
predefSign :: CASLSign
predefSign = predefinedSign ()
predefinedAxioms :: [Named (FORMULA ())]
predefinedAxioms = let
v1 = mkVarDecl (mkNName 1) thing
t1 = toQualVar v1
in [makeNamed "nothing in Nothing" $ mkForall [v1] $ Negation
(Predication noThing [t1] n) n,
makeNamed "thing in Thing" $ mkForall [v1] $ Predication
(Qual_pred_name thing classPredType n) [t1] n]
mkNNameAux :: Int -> String
mkNNameAux k = genNamePrefix ++ "x" ++ show k
-- | Build a name
mkNName :: Int -> Token
mkNName i = mkSimpleId $ hetsPrefix ++ mkNNameAux i