hets/CspCASL/AS_CSP_CASL.hs

	AS_CSP_CASL.hs revision 268193ecba082551560bb4d9f61e49e558e41834
1f80c0ba14aa3bf4526d68767c26116eb30ecaa8Christian Maeder{- |
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederModule      :  $Header$
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederCopyright   :  (c)  Daniel Pratsch and Uni Bremen 2002-2003
06a671f19b2f76097ca4997268954721a831c527Christian MaederLicence     :  All rights reserved.
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer  :  hets@tzi.de
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederStability   :  provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability :  portable
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederabstract syntax of CSP-CASL
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-}
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
f1c6047a6f86f75e1effd7dfa833e0f5bbd16330Christian Maedermodule CspCASL.AS_CSP_CASL where
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport CASL.AS_Basic_CASL
705d04a6d3b01afd249f53397e5cbfa76fc0e179Christian Maederimport Common.Id
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder----------------------------------------------------------------------------
1f80c0ba14aa3bf4526d68767c26116eb30ecaa8Christian Maeder-- Specifications
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder----------------------------------------------------------------------------
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederdata C3PO = Named_c3po NAMED_CSP_CASL_C_SPEC
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder          | C3po CSP_CASL_C_SPEC
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder		   deriving (Show,Eq)
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maederdata NAMED_CSP_CASL_C_SPEC =  Named_csp_casl_spec SPEC_NAME CSP_CASL_C_SPEC
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder		   deriving (Show,Eq)
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder
1f80c0ba14aa3bf4526d68767c26116eb30ecaa8Christian Maedertype SPEC_NAME = SIMPLE_ID
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder
1f80c0ba14aa3bf4526d68767c26116eb30ecaa8Christian Maederdata CSP_CASL_C_SPEC = Csp_casl_c_spec DATA_DEFN CHANNEL_DECL PROCESS_DEFN
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder		   deriving (Show,Eq)
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maederdata Basic_CSP_CASL_C_SPEC = Basic_csp_casl_c_spec CHANNEL_DECL PROCESS_DEFN
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder		   deriving (Show,Eq)
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder
64f2afbaadbbc9ffc4d10eb413325777f7e7fef8Christian Maeder----------------------------------------------------------------------------
-- DATA, CHANNEL & PROCESS Def.
----------------------------------------------------------------------------

type DATA_DEFN = BASIC_SPEC           -- will become a structured spec later

data CHANNEL_DECL = Channel_items [CHANNEL_ITEM]
		   deriving (Show,Eq)

data CHANNEL_ITEM = Channel_decl [CHANNEL_NAME] SORT
		   deriving (Show,Eq)

type CHANNEL_NAME = SIMPLE_ID

type PROCESS_NAME = SIMPLE_ID

data PROCESS_DEFN = Basic PROCESS
                  | Recursive [PROCESS_EQUATION] NAMED_PROCESS
                  | Generic_recursive [PROCESS_EQUATION] GEN_NAMED_PROCESS
		   deriving (Show,Eq)


data NAMED_PROCESS = Named PROCESS_NAME
		   deriving (Show,Eq)

data GEN_NAMED_PROCESS = Generic_named PROCESS_NAME TERM
		   deriving (Show,Eq)

data GENERIC_EQUATION = Generic PROCESS_NAME VAR EVENT_SET
		   deriving (Show,Eq)

data PROCESS_EQUATION = Equation NAMED_PROCESS PROCESS
                      | Generic_equation GENERIC_EQUATION PROCESS
		   deriving (Show,Eq)


data PROCESS = Named_process NAMED_PROCESS
             | Generic_named_process GEN_NAMED_PROCESS
             | Skip
             | Stop
             | Prefix EVENT PROCESS
             | Multiple_prefix VAR EVENT_SET PROCESS
             | Sequential [PROCESS]
             | External_choice [PROCESS]
             | Internal_choice [PROCESS]
             | Alphabet_parallel PROCESS EVENT_SET PROCESS
             | General_parallel PROCESS EVENT_SET EVENT_SET PROCESS
             | Synchronous_parallel [PROCESS]
             | Interleaving_parallel [PROCESS]
             | Hiding PROCESS EVENT_SET
             | Csp_sort_renaming PROCESS SORT_RENAMING
             | Csp_channel_renaming PROCESS CHANNEL_RENAMING
             | Conditional_process FORMULA PROCESS
             | Conditional_choice FORMULA PROCESS PROCESS
		         | Guarded_command FORMULA PROCESS
             | Channel_parallel PROCESS CHANNEL_NAME CHANNEL_NAME PROCESS
		   deriving (Show,Eq)


data EVENT_SET = Event_set SORT
		   deriving (Show,Eq)

data SORT_RENAMING = Op_list [OP_NAME]
		   deriving (Show,Eq)

data CHANNEL_RENAMING = Channel_renaming CHANNEL_NAME CHANNEL_NAME
		   deriving (Show,Eq)

data EVENT        = Term TERM
                  | Send CHANNEL_NAME TERM
                  | Receive CHANNEL_NAME VAR SORT
		   deriving (Show,Eq)


--data CSP_RENAMING = PRED_NAME

--data CSP_RENAMING = SORT_RENAMING
--                  | CHANNEL_RENAMING
--		   deriving (Show,Eq)