Changeset 11228

Show
Ignore:
Timestamp:
07.01.2009 14:10:29 (11 months ago)
Author:
csliam
Message:

Added simplification of CspCASL sentences, currently this is turned off while I develop

Location:
trunk
Files:
5 modified

Legend:

Unmodified
Added
Removed

  • trunk/CspCASL/AS_CspCASL_Process.der.hs

    r11215 r11228  
    4040    deriving (Show,Ord, Eq) 
    4141 
    42  
    4342-- |Event sets are sets of communication types. 
    4443 
    4544data EVENT_SET = EventSet [COMM_TYPE] Range 
    4645    deriving (Show,Ord, Eq) 
    47  
    4846 
    4947-- |CSP renamings are predicate names or op names. 

  • trunk/CspCASL/Print_CspCASL.hs

    r11227 r11228  
    149149            prettyComms cs = sepByCommas (map pretty cs) 
    150150        in brackets(pretty p) <> text "_" <> braces (prettyComms commAlphaList) 
    151           -- (pretty p) 
     151           -- pretty p 
    152152 
    153153instance Pretty CommType where 

  • trunk/CspCASL/SignCSP.hs

    r11226 r11228  
    4444-- alphabet. 
    4545data ProcProfile = ProcProfile [SORT] CommAlpha 
    46                    deriving (Eq, Show) 
     46                   deriving (Eq, Show)              
    4747 
    4848type ChanNameMap = Map.Map CHANNEL_NAME SORT 

  • trunk/CspCASL/SimplifySen.hs

    r11227 r11228  
    1515module CspCASL.SimplifySen(simplifySen) where 
    1616 
    17 import qualified CASL.SimplifySen as CASL_SimplifySen 
     17import CASL.SimplifySen (simplifyCASLSen) 
    1818 
     19import CspCASL.AS_CspCASL_Process 
    1920import CspCASL.SignCSP 
    2021 
     22-- | Simplify a CspCASL sentence for before pretty printing, e.g. for 
     23-- | "show theory". typically this replaces fully quallified CASL by 
     24-- | non fully qualified CASL so that it is readable. 
    2125simplifySen :: CspCASLSign -> CspCASLSen -> CspCASLSen 
    2226simplifySen sigma sen = 
    … …  
    2428      CASLSen f -> 
    2529          let caslSign = ccSig2CASLSign sigma 
    26           in CASLSen $ CASL_SimplifySen.simplifyCASLSen caslSign f 
    27       ProcessEq pn var alpha p -> ProcessEq pn var alpha p 
     30          in CASLSen $ simplifyCASLSen caslSign f 
     31      ProcessEq pn var alpha p -> ProcessEq pn var alpha ( p) -- (simplifyProc sigma p) 
     32 
     33simplifyProc :: CspCASLSign -> PROCESS -> PROCESS 
     34simplifyProc sigma proc = 
     35    let caslSign = ccSig2CASLSign sigma 
     36    in case proc of 
     37      Skip range -> 
     38          Skip range 
     39      Stop range -> 
     40          Stop range 
     41      Div range -> 
     42          Div range 
     43      Run es range -> 
     44          Run es range 
     45      Chaos es range -> 
     46          Chaos es range 
     47      PrefixProcess e p range -> 
     48          PrefixProcess e (simplifyProc sigma p) range 
     49      ExternalPrefixProcess v s p range -> 
     50          ExternalPrefixProcess v s (simplifyProc sigma p) range 
     51      InternalPrefixProcess v s p range -> 
     52          InternalPrefixProcess v s (simplifyProc sigma p) range 
     53      Sequential p q range -> 
     54          Sequential (simplifyProc sigma p) (simplifyProc sigma q) range 
     55      ExternalChoice p q range -> 
     56          ExternalChoice (simplifyProc sigma p) (simplifyProc sigma q) range 
     57      InternalChoice p q range -> 
     58          InternalChoice (simplifyProc sigma p) (simplifyProc sigma q) range 
     59      Interleaving p q range -> 
     60          Interleaving (simplifyProc sigma p) (simplifyProc sigma q) range 
     61      SynchronousParallel p q range -> 
     62          SynchronousParallel (simplifyProc sigma p) (simplifyProc sigma q) range 
     63      GeneralisedParallel p es q range -> 
     64          GeneralisedParallel (simplifyProc sigma p) es (simplifyProc sigma q) range 
     65      AlphabetisedParallel p esp esq q range -> 
     66          AlphabetisedParallel (simplifyProc sigma p) esp esq (simplifyProc sigma q) range 
     67      Hiding p es range -> 
     68          Hiding (simplifyProc sigma p) es range 
     69      RenamingProcess p r range -> 
     70          RenamingProcess (simplifyProc sigma p) r range 
     71      ConditionalProcess f p q range -> 
     72          ConditionalProcess (simplifyCASLSen caslSign f) 
     73                                 (simplifyProc sigma p) (simplifyProc sigma q) range 
     74      NamedProcess name args range -> 
     75          NamedProcess name args range 
     76      FQProcess p alpha range -> 
     77          FQProcess (simplifyProc sigma p) alpha range 
     78 

  • trunk/Makefile

    r11226 r11228  
    282282 
    283283CspCASL_files = CspCASL/AS_CspCASL.hs CspCASL/AS_CspCASL_Process.hs \ 
    284     CspCASL/SignCSP.hs CspCASL/Morphism.hs CspCASL/SimplifySen.hs 
     284    CspCASL/SignCSP.hs 
    285285 
    286286CASL_DL_files = CASL_DL/AS_CASL_DL.hs CASL_DL/Sign.hs CASL_DL/Sublogics.hs