Changeset 11215 for trunk/CspCASL/AS_CspCASL.der.hs

Timestamp:

05.01.2009 15:46:06 (11 months ago)

Author:

csliam

Message:

Large commit - improved static analysis of cspcasl and translation of cspcasl to isabelle

Files:

• trunk/CspCASL/AS_CspCASL.der.hs (modified) (3 diffs)

trunk/CspCASL/AS_CspCASL.der.hs

@@ -14 +14 @@
 module CspCASL.AS_CspCASL where
 
+import Common.Doc
+import Common.DocUtils
 import Common.Id
 
-import CASL.AS_Basic_CASL (SORT, VAR)
+import CASL.AS_Basic_CASL (SORT, VAR, FORMULA)
 
 import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, COMM_TYPE, PROCESS(..),
                                    PROCESS_NAME)
-
-import Common.Id
 
 -- DrIFT command
@@ -34 +34 @@
                     deriving Show
 
+data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range
+                     deriving (Show,Ord, Eq)
+
 data PROC_ITEM = Proc_Decl PROCESS_NAME PROC_ARGS PROC_ALPHABET
                | Proc_Eq PARM_PROCNAME PROCESS
@@ -42 +45 @@
 data PARM_PROCNAME = ParmProcname PROCESS_NAME [VAR]
                      deriving Show
-
-data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range
-                     deriving Show
-
--- Sentences
-
-data CspCASLSentence = CspCASLSentence PROCESS_NAME [VAR] PROCESS
-               deriving (Show, Eq, Ord)
-
-emptyProcName :: PROCESS_NAME
-emptyProcName = mkSimpleId "empty"
-
-emptyCCSentence :: CspCASLSentence
-emptyCCSentence = CspCASLSentence emptyProcName []
-                      (NamedProcess emptyProcName [] nullRange)