AS_CoCASL.der.hs revision e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2004
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : hausmann@tzi.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederPortability : portable
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederAbstract syntax for CoCASL, the coalgebraic extension of CASL
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder Only the added syntax is specified
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maedermodule CoCASL.AS_CoCASL where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Id
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.AS_Annotation
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport CASL.AS_Basic_CASL
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder-- DrIFT command
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder{-! global: UpPos !-}
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype C_BASIC_SPEC = BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedertype AnModFORM = Annoted (FORMULA C_FORMULA)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata C_BASIC_ITEM = CoFree_datatype [Annoted CODATATYPE_DECL] Range
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos: free, type, semi colons
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder | CoSort_gen [Annoted (SIG_ITEMS C_SIG_ITEM C_FORMULA)] Range
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos: generated, opt. braces
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving Show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederdata C_SIG_ITEM = CoDatatype_items [Annoted CODATATYPE_DECL] Range
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- type, semi colons
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder deriving Show
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata CODATATYPE_DECL = CoDatatype_decl SORT [Annoted COALTERNATIVE] Range
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- pos: "::=", "|"s
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder deriving Show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata COALTERNATIVE = Co_construct FunKind (Maybe OP_NAME) [COCOMPONENTS] Range
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- True if Total, pos: "(", semi colons, ")"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder | CoSubsorts [SORT] Range
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder -- pos: sort, commas
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving Show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maederdata COCOMPONENTS = CoSelect [OP_NAME] OP_TYPE Range
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder -- pos: commas, colon
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder deriving Show
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM C_FORMULA)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Eq, Ord, Show)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
76647324ed70f33b95a881b536d883daccf9568dChristian Maederdata C_FORMULA = BoxOrDiamond Bool MODALITY (FORMULA C_FORMULA) Range
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- The identifier and the term specify the kind of the modality
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder -- pos: "[]" or "<>", True if Box, False if Diamond
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder | CoSort_gen_ax [SORT] [OP_SYMB] Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- flag: belongs to a cofree type and hence is cofreeness axiom?
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder deriving (Eq, Ord, Show)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdiamondS, greaterS :: String
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdiamondS = "<>"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergreaterS = ">"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedercocasl_reserved_words :: [String]
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedercocasl_reserved_words = [diamondS]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder